A Calculus of Inconsistency I: Sentential Logic
我们描述了一个图论语法的自指公式以及四值逻辑，包括矛盾和独立的公式。然后，我们探讨在我们的理论中广义真假值表可以实现的程度，并继续描述微积分的模型论，其中允许模型包括矛盾（如“说谎者”）和公式，这些公式作为其结构的一个组成部分。这为我们构建包含矛盾的集合论模型的续集奠定了基础。
2004-09-02 math.LO
Parametric mixed sequent calculus
在本文中，我们提出了一个命题演算包含经典和直觉主义逻辑的不相交副本。我们证明了一个割消定理，并建立了这个系统与线性逻辑之间的关系。
2009-05-11 math.LO
Tense Logic via Truth Degrees: An Algebraic Completeness Result for Kashima's Calculus
Universidad Nacional del Sur（南方大学）；Universidad Nacional de San Juan（圣胡安国立大学）
本文从代数和证明论角度研究最小时态逻辑K_t，引入保真度逻辑及相继式演算，并通过Lindenbaum--Tarski构造改编，为Kashima演算建立了代数完备性定理，连接其嵌套相继式表述与时态布尔代数语义。
2026-10-02 math.LO
Approximate Completeness of Hypersequent Calculus for First-Order Łukasiewicz Logic
针对 Baaz 和 Metcalfe 的 GŁ∀ 近似完备性仅适用于前束公式的局限，本文将原证明推广至超矢列，证明其对任意一阶 Łukasiewicz 公式均近似完备。
2024-12-06 math.LO
The basis of Boole's logical calculus
在本论文中，我们的目标是提供一个深思熟虑的和训诂帐户的基本思想的基础上布尔的理论，与发展我们的调查严格的概念结构内最初介绍了布尔自己的目标。特别是，我们将集中在发展的方法的意义和有用性。我们还将考虑一个轻微的变化，这将使我们能够提出一个新的光的一些重要和天真的方面布尔演算审查的作者在他的工作。最后，一个大的注意力是致力于分析的“被忽视的”逻辑连接符的分工。
2017-10-04 math.LO
Uniform Interpolation in provability logics
本文利用模态可证逻辑GL和Grz的解析演算和终止演算，用证明理论的方法证明了这两类逻辑的一致内插定理. Gödel-Löb的逻辑GL的演算是标准循环演算的一个变体，在Grzegorczyk的逻辑Grz的情况下，演算实现了一个显式的循环防止机制，灵感来自Heuerding的工作。
2022-11-04 math.LO
Esakia's theorem for the amended monadic intuitionistic calculus
New Mexico State University（新墨西哥州立大学）；University of Milan（米兰大学）
该研究证明修正的单子直觉逻辑M^+IPC的Esakia定理成立，揭示了其与修正的单子Grzegorczyk逻辑之间的关系。
2025-12-19 math.LO
A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)
本文为包含分裂析取与探究析取的基础命题团队逻辑引入了一种深度推理矢列演算，证明了其保高度弱化、切消除等性质，并导出了新的Lyndon插值定理。
2025-08-10 math.LO
Epsilon Theorems in Intermediate Logics
任何中间命题逻辑（即，包括直觉主义逻辑并包含在经典逻辑中的逻辑）可以被扩展到具有π-和τ-算子以及临界公式的微积分。对于经典逻辑，这导致希尔伯特的$\varepsilon$ -演算。经典逻辑的第一和第二$\varepsilon$ -定理建立了$\varepsilon$ -演算在其经典基本逻辑上的保守性。众所周知，第二个$\varepsilon$ -定理对于直觉的$\varepsilon$ -演算是失败的，因为预解是不可能的。本文研究了添加临界$\varepsilon$ -和$τ$ -公式以及将量词翻译成$\varepsilon$ -和$τ$ -项对中间逻辑的影响。它表明，保守性的命题基础逻辑也持有这样的中间$\varepsilonτ$ -演算。“扩展的”第一$\varepsilon$ -定理在基逻辑是有限值哥德尔-达米特逻辑时成立，否则不成立，但对无限值哥德尔逻辑中的某些可证明公式成立。第二个$\varepsilon$ -定理也适用于有限值一阶哥德尔逻辑。用于证明无限值哥德尔逻辑的扩展的$\varepsilon$ -第一定理的方法建议应用于算术理论。
2021-11-30 math.LO
Undefinability of Standard sequent calculi for Paraconsistent three-valued logics
本文研究一类三值次协调逻辑的演绎性质。我们定义了一个标准微积分的概念，并证明了这些逻辑没有健全的和完整的标准微积分。此外，我们还利用三边序列为次协调弱Kleene逻辑提供了非标准的可靠的、完全的和无割的代数演算。
2017-09-28 math.LO
Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus
本文积极地解决了Seligman、Girard和Liu等人提出的友谊认知逻辑是否能提供一个希尔伯特系统的问题。为了找到一个Hilbert系统，我们首先介绍了一个健全的，完整的和无割的树（或嵌套）EFL演算，这是一个集成的组合Seligman的基本混合逻辑的树演算和模态逻辑的树演算。然后，我们将树的结构转换成一个普通的公式来指定EFL的Hilbert系统，最后证明我们的Hilbert系统对于预定的二维语义是健全和完备的。
2019-07-10 cs.LO math.LO
Truth-relevant Logic, Propositional Calculus
真值相关逻辑是比经典逻辑更好的数学基础。这是理查德·迪亚兹在1981年提出的一个系统。在某种意义上，t相关逻辑是基于Kleene强表的。这些定义了一个具有三个值的系统：true，false，unknown。证明了存在重言式具有以下性质：存在命题变元（t-相关变量）的真子集，使得对于所有真/假组合，重言式都为真，也就是说，重言式中出现的其余变量（冗余变量）可以是未知的。我们认为这样的复合句既不是真的也不是假的。提供了哲学论证。提出了基于表格的证明系统。证明了重言式L =（R1 v ~R1）&（R2 v ~R2）&. &（Rm v ~Rm），其中{R1，R2，. Rm}是t-相关命题变元的子集，并且=是Kleene强表等价的.
2023-02-12 math.LO
The G4i analogue of a G3i calculus
Utrecht University（乌得勒支大学）
本文提出一种为一大类直觉主义模态逻辑构造终止分析演算的方法，将 Dyckhoff 针对直觉主义命题逻辑的 G4ip 工作扩展至直觉主义模态逻辑，修正了早期版本的定理错误。
2026-08-24 math.LO
Propositional Calculus with Multiple Negations
本文提出带有多重否定的命题演算（CPN_n），通过在经典命题逻辑中添加有限个弱否定，结合次协调逻辑与经典逻辑的优势，以受控方式引入弱矛盾而不导致平凡性。
2025-10-12 math.LO
Is Leibnizian calculus embeddable in first order logic?
为了探索莱布尼茨微积分在一阶逻辑（FOL）和现代框架中的嵌入程度，我们建议撇开本体论问题，专注于过程问题。这将使一个帐户的莱布尼茨程序的框架内有限的FOL与少量的额外成分，如关系的无限接近。如果，正如我们在这里所说，一阶逻辑确实适合于开发现代代理的推理移动中发现莱布尼茨微积分，然后现代无穷小框架更适合于解释莱布尼茨微积分比现代魏尔斯特拉斯的。关键词：一阶逻辑;微积分;本体论;过程;莱布尼茨;维尔斯特拉斯;亚伯拉罕罗宾逊
2016-05-11 math.HO math.LO
Quantified Reflection Calculus with one modality
本文提出了QRC逻辑$_1$，它是量化模态逻辑的严格正片段.对菱形模态的预期解读是形式理论的一致性。谓词符号被解释为参数化公理化。我们证明了算术可靠的逻辑QRC $_1$关于这个算术解释。量化的可证明性逻辑是不可判定的。然而，不可判定性证明不能在我们的签名和算术阅读中进行。我们猜想逻辑QRC $_1$是算术完备的.本文采取的第一步，通过提供关系语义QRC $_1$与相应的完整性证明算术的完整性。我们还展示了有限模型的属性，这意味着可判定性。
2020-03-30 math.LO
On structural proof theory of the modal logic K+ extended with infinitary derivations
本文研究模态逻辑K+在加入无穷推导后的结构证明论，提出允许非良基证明的矢列演算，并利用连续切割消去方法证明切割消去定理，同时说明K+的普通证明可视为循环无切割证明。
2023-10-16 math.LO
A cut-free sequent calculus for the bi-intuitionistic logic 2Int
本文的目的是引入一个双直觉的代数演算，并给出其结构规则的可容许性证明。我将介绍的演算，称为SC2Int，是双直觉主义逻辑2Int的一个微积分。这种逻辑的演算代表了一种双边主义的推理，因为它们不仅内化了验证或可证明性的过程，而且内化了证伪或所谓的对偶可证明性方面的对偶过程。2Int的自然演绎演算的一个范式定理已被证明，本文想证明SC 2Int的一个割消定理，即如果成功，这将推广已有的结果.
2020-09-23 cs.LO math.LO
The calculus of names -- The legacy of Jan Łukasiewicz
本文回顾了 Jan Łukasiewicz 开创的名称演算逻辑分支，介绍了其首个公理系统的起源，并提出了扩展系统，同时从现代逻辑视角指出其三段论方法的非唯一性，肯定了其重要遗产地位。
2025-04-02 math.LO
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.LO
The taming of recurrences in computability logic through cirquent calculus, Part I
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。
2012-09-19 cs.LO math.LO
The taming of recurrences in computability logic through cirquent calculus, Part II
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。
2011-06-19 cs.LO math.LO
A Sequent Calculus for Dynamic Topological Logic
本文对动态拓扑逻辑$\textbf{DTL}$的时间-拓扑片段$\textbf{DTL}_{0}^{\circ * \slash \Box}$引入了一个新的演算，利用\cite{paper3}中给出的$\textbf{DTL}_{0}^{\circ * \slash \Box}$的公理化，从语义上证明了其可靠性，并从语法上证明了其完备性. $\textbf{DTL}_{0}^{\circ * \slash \Box}$的无割的Tumbler演算是Gentzen经典Tumbler演算的命题片段、模态扩展的两个$\Box$结构规则、以及时间扩展的九个$\circ$（下一个）和$*$（下一个）结构规则的结合。未来的研究将集中在动态拓扑$\textbf{S5}$逻辑的超代数演算的建设，以证明Kremer的下一个删除猜想几乎离散空间$\textbf{S5H}$上的同胚逻辑。
2014-08-03 cs.LO math.LO
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
2024-11-09 cs.LO math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
Justification Logic of the Lambda Calculus
Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
2026-07-28 cs.LO math.LO
Display to Labeled Proofs and Back Again for Tense Logics
我们介绍之间的翻译显示演算证明和标记演算证明的紧张逻辑的背景下。首先，我们证明了，在显示演算的最小时态逻辑Kt扩展与一般路径公理的每一个派生可以有效地转化为相应的标记演算的派生。关于逆翻译，我们表明，Kt扩展与路径公理，在相应的标记演算的每个派生可以放入一个特殊的形式，是可翻译的派生在相关的显示演算。在这个逆翻译中的一个关键见解是将显示序列规范表示为标记的多树。标记的多树，它表示等价类的显示序列模显示公设，也揭示了相关的对应结果紧张的逻辑。
2021-05-06 cs.LO math.LO
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
2014-11-05 cs.LO math.LO
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。
2023-09-01 cs.LO math.LO
Elementary-base cirquent calculus I: Parallel and choice connectives
循环演算是一个证明系统，操纵循环风格的结构，而不是公式。利用它，本文构建了可计算性逻辑命题片段（计算问题的博弈语义构想逻辑，见http://www.csc.villanova.edu/~japaridz/CL/）的一个合理而完整的公理化CL 16，其逻辑词汇由否定、平行和选择连接词组成，其原子表示基本的，即无移动的博弈。
2017-07-16 cs.LO math.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
Introduction to Cirquent Calculus and Abstract Resource Semantics
本文介绍了一种改进的微积分的方法，称为cirquent演算。而在Gentzen风格的证明树兄弟姐妹（或堂兄弟姐妹等）序列是不相交的公式序列，在圆微积分中，它们可以共享元素。明确地允许或禁止共享资源，从而将子结构逻辑的资源感知直觉带到一个更微妙的层次，cirquent演算提供了比cirquent演算更大的灵活性和功能。随着可计算性逻辑的诞生，对新的演绎工具的需求也随之而来（见http：//www.cis.upenn.edu/linggiorgi/cl.html）--这是一种语义构建的计算资源形式理论，它顽固地抵制了传统句法方法框架内的任何公理化尝试。循环微积分打破了僵局。从其规则的全部集合中去除收缩，产生了可计算性逻辑的基本片段CL 5的健全和完整的系统。另一方面，在微积分中做同样的事情，会把婴儿和洗澡水一起扔掉，导致严格较弱的仿射逻辑。可计算性逻辑的一个隐含的主张是，它是CL 5，而不是仿射逻辑，充分体现了传统上与后者相关的资源哲学。为了加强这一主张，本文进一步引入了一个抽象的资源语义，并显示了CL 5的可靠性和完整性。
2005-12-23 cs.LO math.LO
Linear logic with idempotent exponential modalities: a note
本文讨论了幂等指数模态线性逻辑的一个变体。我们提出了一个新的演算系统，并讨论了它的语义。我们还给出了这种演算的具体关系模型。
2014-07-22 cs.LO math.LO
A Uniform Substitution Calculus for Differential Dynamic Logic
本文介绍了一种新的证明演算微分动态逻辑（dL），完全基于一致替换，证明规则，取代一个谓词符号的公式无处不在。一致替换使得依赖公理而不是公理模式成为可能，大大简化了实现。而不是非平凡的模式变量和健全的临界侧条件的变量的出现模式，所得到的演算只采用了有限数量的普通dL公式作为公理。差分动态逻辑的静态语义仅在统一替换和绑定变量重命名中捕获，而不是以微妙的方式在证明器实现中传播。除了健全的统一替代，本文介绍了微分动态逻辑，使之有可能内化微分不变量，微分替代和推导的第一类公理在dL的微分形式。
2015-07-30 cs.LO cs.PL math.LO
Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
本文提出二元混合逻辑的完备表记演算，同时构建了依赖维度的混合依赖积逻辑演算，并证明其完备性，但所有系统均不具终止性。
2023-11-14 cs.LO math.LO
First-Order Modal $ξ$-Calculus: On the Aspects of Application and Bisimulation
本文提出了一阶模态$ξ$ -演算以及系谱Kripke模型。受模态$μ$ -演算的启发，一阶模态$ξ$ -演算采取了非常相似的形式，并将其归纳表达扩展到不同的维度。我们阐述了几个生动的例子，证明了这种逻辑的深刻的效用，特别是描绘家谱的并发计算机进程。互模拟概念的逻辑也得到了彻底的检查。
2023-01-17 cs.LO math.LO
Pomset logic: the other approach to non commutativity in logic
30年前，我介绍了经典线性逻辑的一个非交换变体，称为“pomset逻辑”，它是从线性逻辑的一种特殊范畴解释（称为相干空间）中产生的。除了线性逻辑中常见的交换乘法连接词外，pomset逻辑还包括一个非交换连接词“$\triangleleft$“，称为“before”，结合和自对偶：$(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$。一个pomset逻辑证明的结论是一个偏序的多集公式。Pomset逻辑具有割消和指称语义的证明网演算，忠实地嵌入了证明网演算。对pomset逻辑的研究已经重新开放，最近的结果是关于漂亮的证明网，关于它的微积分，或者关于它的后续演算，如Guglielmi和Strassburger的深度推理。因此，现在是我们发表一个完整的介绍pomset逻辑，包括出版和未出版的材料，旧的和新的结果。Pomset逻辑（1993）是线性逻辑（1987）的非交换变体，就像Lambek演算（1958！）它也可以用作语法形式主义。这两种演算是完全不同的，但我们希望我们在这里给出的代数表示，用公式作为代数项，用证明（网）正确性的语义概念，更好地匹配兰贝克关于逻辑应该是什么的观点。
2023-02-03 cs.LO math.LO
A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic
针对$\textsf{iK}_d$和$\textsf{iK}_{d*}$这两个动态拓扑逻辑系统，本文提出无切割的G3风格相继式演算，补充了其证明论分析，并证明了析取性质、Visser规则推广及插值性质等关键结果。
2025-02-13 cs.LO math.LO
Cirquent calculus deepened
循环演算是一种新的证明理论和语义框架，其主要区别特征是基于循环，而不是更传统的方法，处理树状对象，如公式或序列。其优点包括更高的效率、灵活性和表现力。本文提出了一个详细的阐述了深推理事件逻辑，这是自然和内在的资源意识。它表明，经典逻辑，无论是在句法上还是在语义上，都只是这种更一般的、在某种意义上更基本的逻辑--以循环演算形式出现的资源逻辑--的一个特殊的、保守的片段。读者会发现各种有利于切换到新框架的论点，例如显示线性逻辑或其他基于公式的方法开发资源逻辑的表达能力不足的论点，在Cirquent演算提供的表示和证明复杂性方面，传统方法的指数改进等等。本文的主要目的之一是提供一个介绍性的起点，正如作者所希望的那样，可能有机会成为证明理论研究的一个新方向-基于电路而不是公式的证明理论。
2008-04-01 cs.LO math.LO
The Distributive Full Lambek Calculus with Modal Operators
本文研究了在非交换条件下，考虑$\Box$和$\Diamond$的带有模态算子的有界分配剩余格的逻辑。我们为这样的子结构模态逻辑引入关系语义。通过离散对偶和正则扩张证明了任何正则逻辑都是Kripke完备的。也就是说，我们表明，一个模态扩展的分配充分Lambek演算是其框架的逻辑，如果它的品种是封闭的规范下的扩展。在此基础上，我们建立了剩余分配模态代数与基于Priestley空间的拓扑Kripke结构之间的Priestley式对偶。
2020-05-31 math.CT math.LO math.RA
Natural Deduction Calculus for First-Order Logic
本文的目的是给出一个易于理解的逐步解释，让感兴趣的人充分认识到自然演绎的一阶逻辑的力量。自然演绎作为一种证明系统，可以用来证明命题逻辑中的各种陈述，但我们将看到它的扩展，以涵盖量词，这使它在解决更复杂的现实世界问题时比命题逻辑更强大。我们首先回顾了逻辑连接词和量词，以商定整篇论文将使用的符号，因为有些作者使用不同的符号来指代同一事物。此外，我们展示了最常用的推理规则。此外，我们给出了一阶逻辑自然演绎的可靠性和完备性。最后，我们解决了从简单到复杂的示例，为您提供了不同的情况，您可以在其中应用证明系统来解决可能遇到的问题。希望这篇文章能有助于使这个主题更容易理解。
2021-08-13 cs.LO math.LO
Complete and Terminating Tableau Calculus for Undirected Graph
本文针对无向图构造混合逻辑的表列方法，证明其完备性与终止性，并由此得出该逻辑的可判定性。
2024-11-25 cs.LO math.LO
On noncommutative extensions of linear logic
本文受语义学启发定义半交换乘法线性逻辑，扩展两个非交换连接词，并引入装饰相继式演算，证明其无切割、可靠且完全，从而为 Pomset 逻辑提供了相继式演算表述。
2019-09-19 cs.LO math.LO
Intuitionistic Monotone Modal Logic: Proof Theory and Semantics
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Bern（伯尔尼大学）
研究直觉主义单调模态逻辑IM，通过构造性邻域模型刻画其自然扩展族，提出基于经典单调模态逻辑M的结构演算，证明IM的可判定性，揭示M与K的构造性和直觉主义变体之间的类比。
2026-07-01 cs.LO math.LO
Introduction to a Hypergraph Logic Unifying Different Variants of the Lambek Calculus
本文提出了超图Lambek演算（$\mathrm{HL}$）.这种形式主义的目的是推广Lambek演算（$\mathrm{L}$）超图作为超边替换文法扩展上下文无关文法。与Lambek演算不同，$\mathrm{HL}$处理超图类型和序列;它的公理和规则自然地推广了$\mathrm{L}$的公理和规则。因此，某些属性（例如剪切消除）可以从$\mathrm{L}$提升到$\mathrm{HL}$。结果表明，$\mathrm{L}$可以自然地嵌入在$\mathrm{HL}$中，而且，它的一些变体（$\mathrm{LP}$，$\mathrm{NL}$，$\mathrm{NLP}$，$\mathrm{L}$与模态，$\mathrm{L}^\ast(\mathbf{1})$，$\mathrm{L}^{\mathrm{R}}$）也可以通过不同的图形结构嵌入在$\mathrm{HL}$中。我们还建立了一个$\mathrm{HL}$和嵌入式含义的数据库之间的连接。证明了$\mathrm{HL}$的解析问题是NP完全的。
2021-03-01 cs.LO math.LO
A Complete Uniform Substitution Calculus for Differential Dynamic Logic
本文介绍了一个相对完整的微分动态逻辑（dL）的证明演算，它完全基于一致替换，一个证明规则，取代一个谓词符号的公式无处不在。一致替换使得使用公理而不是公理模式成为可能，从而大大简化了实现。而不是微妙的模式变量和健全的关键侧条件的逻辑变量的出现模式，以限制无限多的公理模式实例健全的，由此产生的演算只采用了有限数量的普通dL公式作为公理，统一的替代实例健全。微分动态逻辑的静态语义和它对证明步骤施加的合理性关键限制仅在统一替换和变量重命名中捕获，而不是以微妙的方式在证明器实现中传播。除了健全的一致替换，本文介绍了微分动态逻辑的微分形式，使其能够内化微分不变量，微分替换和导数作为第一类公理，以公理化地推理微分方程。由此得到的微分动态逻辑公理化被证明是合理的和相对完整的。
2016-07-27 cs.LO cs.PL math.LO
Logic for Everyone
在这本专著中，介绍了美国的结果。S.海军学院数理逻辑课程计划。命题演算和谓词演算以一种独特的方式提出。所有方面都是使用最少的数学技术严格建立的。命题演算得到了相当大的扩展，许多证明方法被用来建立谓词演算的结果。还介绍了Consequnce算子。此外，材料被认为是一个终端的经验，并针对应用，如逻辑网络，程序，以确定参数的有效性，简单的一致性的一些假设，一些具体和抽象的模型论，并通过紧性定理，产生的无穷小，超字和ultralogics。
2006-01-29 math.GM math.LO
Game semantics for the constructive $μ$-calculus
本文为构造性$μ$-演算提出博弈语义，证明其与双关系语义等价，并借此证明$μ$-演算在$\mathsf{IS5}$上坍缩为模态逻辑，同时给出扩展不动点算子的$\mathsf{IS5}$完备性。
2024-10-01 cs.LO math.LO
Computational interpretation of classical logic with explicit structural rules
我们提出了一个演算提供了一个Curry-Howard对应的经典逻辑中所表示的显式的结构规则，即弱化和收缩演算。这些结构规则分别引入了明确的删除和重复的条款。我们提出了一个类型系统，我们证明了类型保持下减少。详细研究了它与经典微积分之间的一种相互关系，这种关系具有隐含的结构规则。从这个分析中，我们得到强归一化性质。
2012-03-21 cs.DC cs.LO math.LO
Completeness for Game Logic
游戏逻辑是由Rohit Parikh在20世纪80年代引入的，作为命题动态逻辑（propositional dynamic logic，PDL）的推广，用于推理玩家在确定的2人游戏中可以强制执行的结果。从语义上讲，从程序到游戏的概括是通过从Kripke模型到单调邻域模型来反映的。Parikh提出了一个自然的PDL风格的希尔伯特系统，它很容易被证明是合理的，但它的完备性迄今为止仍然是一个开放的问题。在本文中，我们介绍了一个切免费的游戏逻辑的mu演算，和两个切免费的mu演算，操作注释公式，一个游戏逻辑和一个单调的μ演算，多模态μ演算的变体，其中的语义是由单调邻域模型，而不是Kripke结构。我们表明这些系统是健全的和完整的，帕里克的公理化的完整性如下。我们的方法建立在Afshari & Leigh（LICS 2017）最近的想法和结果的基础上，我们通过系统之间的一系列证明转换来获得完整性。一个关键的要素是从博弈逻辑到单调μ演算的有效性保持翻译。
2019-04-30 cs.LO math.LO
Aristotle' Relations: An Interpretation in Combinatory Logic
通常用类的演算来模拟器官的三段论，并不包括关系。然而，亚里士多德可能在前两卷中将它们设想为亲属的范畴，在那里他允许它们与自己组成。组合是组合逻辑中的主要运算，因此组合逻辑为一种新的建模提供了自己。由此产生的演算还包括由逻辑连接词组成的谓词。
2020-07-06 math.HO math.LO
Canonical Proof nets for Classical Logic
证明网为模规则排列的证明提供了抽象的对应物;其思想是，如果两个证明具有相同的底层证明网，则它们本质上是相同的证明。因此，提供一个令人信服的证明网络对应于经典的微积分证明是理解经典微积分证明的重要一步。通过令人信服，我们的意思是：（a）应该有一个典范函数从证明网络的证明，（b）应该有可能检查网络的正确性在多项式时间，（c）每个正确的网络应该是可获得的从一个微积分证明，（d）应该有一个削减消除程序，保持正确性。以前的尝试给证明网类对象的命题经典逻辑已经失败了至少一个上述条件。在[23]中，作者给出了满足（a）和（b）的证明网（扩展网）的演算;文章定义了与扩展网对应的证明演算，但没有给出（c）的显式证明。该演算称为LK \ast，是一种新的具有加法和乘法析取规则的单边演算.本文（[23]的一个自包含的扩展版本）给出了关于LK \ast的扩展网的（c）的一个充分证明，并且另外给出了扩展网内部的一个割消元过程--这使得扩展网成为满足所有四个准则的经典逻辑的第一个证明网概念。
2012-03-19 cs.LO math.LO
Semantical Analysis of the Logic of Bunched Implications
我们给出了一种新的方法来证明逻辑（以下简称：对象逻辑）的可靠性和完备性，该逻辑绕过模型中的真值直接与有效性一起工作。我们不是在特定的模型中使用特定的世界，而是使用特征世界（即，世界的一般代表）在任意模型中。这种推理被一个元逻辑（在这种情况下，一阶经典逻辑）的微积分捕获，它的表达足以捕获对象逻辑的语义。从本质上讲，人们对对象逻辑的有效性有一个演算。该方法通过还原逻辑的视角（与演绎逻辑的更传统范式相反）进行，使用还原空间作为媒介，以展示对象逻辑的相继演算和有效性演算中还原的行为等价性。而不是研究一般的技术，我们说明了它的逻辑集束的影响（BI），因此IPL和MILL（无否定）也治疗。直观地说，BI是直觉命题逻辑和乘法直觉线性逻辑的自由组合，这使得它的元理论相当复杂。关于BI的文献包含许多相似但最终不同的代数结构和满足关系，它们要么仅捕获逻辑的片段（尽管很大），要么具有用于某些连接词的复杂子句（例如，Beth's clause for disjunction instead of Kripke's）。正是这种复杂性促使我们使用BI作为这种语义方法的案例研究。
2022-10-11 cs.LO math.LO
A Canonical Fuzzy Logic
介绍了基本概念和操作a）的命题演算的一个变种的模糊逻辑-规范模糊逻辑，CFL -并在一个更简洁和介绍性的方式，b）理论的模糊集根据相同的逻辑。如果一个参数$w$的数值仅限于0和1这两种可能性，则二价经典逻辑和经典集合论的命题演算可以看作CFL相应理论的特例.
2021-05-25 cs.LO math.LO
