Twist Sequent Calculi for S4 and its Neighbors
本文提出两种Gentzen风格扭转矢列演算用于正规模态逻辑S4，通过扭转否定推理规则为含大量否定的可证模态公式生成简短证明，并证明切割消去与子公式性质，同时推广至S5等邻近逻辑。
2024-12-31 cs.LO
Terminating Calculi for Propositional Dummett Logic with Subformula Property
本文给出了两个满足子公式性质的命题Dummett逻辑的终止表演算。我们演算的思想依赖于Dummett逻辑的线性有序Kripke语义。第一个演算在两个语义层面上工作：现在和下一个可能世界。第二个演算采用通常的对象语言的Tableau系统，并利用一个属性的建设的完整性定理，引入一个检查，这是一种替代循环检查机制。
2012-06-20 cs.LO
Local Intuitionistic Modal Logics and Their Calculi
本研究聚焦带局部模态算子的直觉主义模态逻辑，明确基础逻辑LIK与WK、IK的强弱关系，给出其公理化与双嵌套演算，同时提供判定及有穷反模型提取方法。
2024-03-11 cs.LO
Streamlining Input/Output Logics with Sequent Calculi
本研究通过面向证明搜索的序列演算简化Bochman的因果输入/输出（I/O）逻辑，建立其与原始I/O逻辑可推导性的句法语义联系，获得新语义、复杂度界等成果，统一解决相关未决问题。
2023-06-15 cs.LO
On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
我们考虑两种风格的证明演算紧张的逻辑，在嵌套序列的基础上提出的形式主义的家庭。一个嵌套的序列可以看作是一个传统的单边序列树。我们的第一种演算风格被称为“浅演算”，其中推理规则仅应用于嵌套的根节点中的根结点。我们的浅层演算是鹿岛演算的时态逻辑的扩展，并与显示演算共享一个基本特征，即存在被称为“显示公设”的结构规则。浅层结石有一个简单的切割消除程序，但由于存在显示假设和其他结构规则，不适合进行证据搜索。第二种类型的演算使用深度推理，推理规则可以应用于嵌套的递归中的任何节点。我们表明，对于一系列的扩展时态逻辑，这两种风格的演算是等价的，并且有一个自然的证明理论之间的对应关系显示公设和深推理。深度推理演算具有子公式性质，没有显示公设或其他结构规则，这使得它们成为一个更好的证明搜索框架。
2011-05-14 cs.LO
Expressiveness Results for Timed Modal Mu-Calculi
本文证明了定时模态μ演算$L^{rel}_{ν,μ}$严格强于其他μ演算及TCTL，而其他μ演算与TCTL在一般定时自动机上不可比较。
2023-10-06 cs.LO
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
我们提出了简单的新的霍尔逻辑和精化演算的混合系统的风格的微分动态逻辑。（细化）Kleene代数与测试用于推理程序结构和生成验证条件在这一级。透镜以通用代数方式捕获混合程序存储。该方法已正式与伊莎贝尔/霍尔证明助手。一些示例解释了工作流程和最终的验证组件。
2019-10-29 cs.LO
Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics
研究了Burgess提出的优先条件逻辑PCL及其扩展.首先，一个自然语义的基础上的邻域模型，推广刘易斯的球模型的反事实逻辑，提出。直接证明了PCL及其推广的可靠性和完备性。然后介绍了该家族所有逻辑的标号微积分。该演算是模块化的，并具有标准的证明理论性质，其中最重要的是容许切割，这需要一个完整的演算的语法证明。通过采用一种通用的策略，根优先证明搜索终止，从而为PCL及其扩展提供了一个决策过程。最后，建立演算的语义完备性：从一个失败的证明尝试中的有限分支中，有可能提取出根节点的有限反模型。后一个结果给出了所有考虑的逻辑的有限模型性质的构造性证明。
2020-02-14 cs.LO
Games for Hybrid Logic -- From Semantic Games to Analytic Calculi
博弈语义学和获胜策略为语义学和逻辑证明系统之间提供了一个潜在的概念桥梁。我们说明了这种联系的混合逻辑-模态逻辑的扩展，允许显式引用的语言中的世界。主要的结果是，系统的搜索所有模型的获胜策略可以被有限化，从而重新制定为一个证明系统。
2022-06-01 cs.LO
Psi-calculi: a framework for mobile processes with nominal data and logic
psi演算的框架扩展了pi演算的数据结构和逻辑断言和条件的名义数据表。它们可以在进程之间传输，并且它们的名称可以像标准pi演算中那样静态地作用域。Psi演算可以捕获与其他提出的pi演算扩展相同的现象，例如应用pi演算，spi演算，融合演算，并发约束pi演算，以及具有多元通信信道或模式匹配的演算。PSI演算甚至可以更通用，例如允许结构化通道，高阶形式主义，如用于数据结构的λ演算，以及用于断言的谓词逻辑。我们提供了充分的比较，相关的结石，并讨论了一些重要的应用。我们标记的操作语义和互模拟的定义是直接的，没有结构一致性。我们建立最低要求的名义数据和逻辑，以证明一般代数性质的PSI演算，所有这些都已检查的互动定理证明伊莎贝尔。PSI演算的表达性明显超过其他形式主义，而语义的纯度与原始的PI演算相当。
2011-03-31 cs.LO
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
Fitch-Style Modal Lambda Calculi
Fitch风格的模态演绎，其中模态通过打开一个从属证明来消除，并通过关闭一个来引入，在20世纪90年代被研究作为lambda演算的基础。我们表明，这样的演算有良好的计算性能的各种直觉模态逻辑。语义是在配备了一个endofunctors的附加词的carnival封闭范畴中给出的，必要性模态由右伴随词解释。这个函子是一个幂等的comonad，语义上的一致性结果使我们能够提出一个演算的直觉S4比其他文献中的简单。我们证明了演算可以用必然性的左伴随扩展为时态逻辑，并且对于范畴语义是完备的。
2018-01-19 cs.LO
Internal Calculi for Separation Logics
我们提出了一个一般的方法来公理化分离逻辑与heaplet语义没有外部功能，如名词/标签。首先，我们为无量词分离逻辑设计了第一个（内部）希尔伯特式公理化。我们实例化的方法，通过引入一个新的分离逻辑的基本特征：它配备了分离合取，谓词LS，和一个自然的保护形式的一阶量化。我们应用我们的方法，其公理化。作为我们的方法的副产品，我们还建立了这个新的逻辑的确切的表达能力，我们显示其可满足性问题的P空间完备性。
2019-10-11 cs.LO
Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
在每一个变式中，因式分解和标准化是两个关键属性，它们显示了结果是如何计算的。我们没有分别证明按名称调用（CbN）和按值调用（CbV）变体的因式分解/规范化，而是只证明一次bang演算（受线性逻辑启发并包含CbN和CbV的扩展），然后我们通过翻译转移结果，获得CbN和CbV的因式分解/规范化。该方法是鲁棒的：它仍然适用于扩展演算与运营商和额外的规则，以模拟一些额外的计算功能。
2021-01-20 cs.LO
Binary Sequent Calculi for Truth-invariance Entailment of Finite Many-valued Logics
在本文中，我们考虑具有有限真值集的真值函数多值逻辑类。本文的主要结果是发展了一个新的\emph{binary}演算（每个演算是一对公式）的多值逻辑与一个有限集的真值，和Kripke的似语义，它是既健全和完整的。我们没有使用基于矩阵的逻辑蕴涵与指定的真值的一个严格的子集，但不同的一种新的语义的基础上推广的经典的2值真值不变蕴涵。为了定义这种基于非矩阵的多模态演算，我们利用经典的合取、析取和模态连接词的有限集合，将多值逻辑转化为正2值多模态逻辑。在这个代数框架中，我们定义了一个唯一确定的公理系统，通过扩展经典的2-值分配格逻辑（DLL）的一组新的公理多值逻辑连接。对偶地，在自指Kripke式框架中，我们得到一个唯一确定的框架，其中每个可能世界也是多值逻辑的Lindenbaum代数的等价类，由真值表示。
2011-03-07 cs.LO
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
本文研究了命题直觉主义逻辑、一阶非常数论域直觉主义逻辑和一阶常数论域直觉主义逻辑的标号演算和套演算之间的关系。它示出，拟合的嵌套结石自然产生于其相应的标记结石-为上述每一个逻辑-通过消除标记派生的结构规则。这两种类型的系统之间的平移对应关系被用来表明嵌套演算从其相关的标记演算中继承了证明理论属性，例如规则的完整性，可逆性和切割容许性。由于标记的演算很容易通过逻辑的语义，本文提出的方法可以被看作是一个，从而细化版本的标记演算（包含嵌套的演算片段）具有良好的性能直接从逻辑的语义。
2021-04-19 cs.LO math.LO
Sequent Calculi for Data-Aware Modal Logics
本文为数据感知模态逻辑HXPathD提出Gentzen式矢列演算，并给出可靠性、完备性、可逆性及切消的完整证明，作为形式结果的参考。
2025-05-22 cs.LO
Bisequent Calculi for Neutral Free Logic with Definite Descriptions
本文在中性自由逻辑中为带等词与限定摹状词的极小理论构建双矢列式演算，并证明扩展系统中切分规则可容许。
2024-12-02 cs.LO
Labelled Sequent Calculi for Propositional Team Logics
University of Helsinki（赫尔辛基大学）；University of Amsterdam, University of Southern Denmark（阿姆斯特丹大学，南丹麦大学）；University of Bern（伯尔尼大学）；Utrecht University（乌得勒支大学）
为基于团队语义的四种逻辑（基本探究逻辑、命题直觉主义依赖逻辑及其张量析取扩展）提供了可靠且完备的带标签矢列演算，并证明了弱化、收缩和切割规则的可容许性，最后给出了带简化标签的终止证明搜索过程。
2026-07-01 cs.LO
Refutation calculi for lattice-based logics: from display to tableaux
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Johannesburg（约翰内斯堡大学）；Scuola Normale Superiore di Pisa（比萨高等师范学院）
本文引入基本LE-逻辑的反驳显示演算，通过可推导矢列的分析证明其可靠性和完全性，并从中得到终止的表格演算。
2026-05-23 cs.LO math.LO
Bounded Inquisitive Logics: Sequent Calculi and Schematic Validity
本文为 n-有界探究逻辑 InqBQ_n 构造了无切割带标签矢列演算，并通过 Casari 公式揭示了原子有效性与模式有效性在有界与无界谓词探究逻辑中的微妙差异。
2025-07-18 cs.LO
Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning
我们提出了一些逻辑的非单调推理，由克劳斯，莱曼和Magidor定义的表演算。我们给出了所有KLM逻辑，即优先，循环累积，累积和理性逻辑的一个Tableau证明过程。我们的演算是通过引入合适的模态来解释条件断言而获得的。我们提供了一个决策程序的逻辑考虑，我们研究它们的复杂性。
2006-11-10 cs.AI cs.LO
Labelled calculi for quantified modal logics with definite descriptions
本文引入了具有确定描述的量化模态逻辑的标号演算。我们证明了这些演算具有G3型演算的良好结构性质。特别地，所有规则都是保高可逆的，弱化和收缩是保高容许的，割是容许的。最后，我们表明，每个演算给出了相应的模型类的有效性的证明理论表征。
2020-02-12 cs.LO math.LO
Comparative plausibility in neighbourhood models: axiom systems and sequent calculi
我们介绍了一个家庭的比较可扩展性逻辑的邻域模型，推广刘易斯的比较可扩展性运营商的球模型。我们提供了公理系统的逻辑，并证明其可靠性和完备性方面的语义。然后，我们介绍了该家族中几种逻辑的两种分析证明系统：Lellmann和Pattinson风格的多前提相继式演算，我们证明了其截可接受性，以及Girlando等人基于条件逻辑结构化演算的超相继式演算。，专门为反模型构建而设计，而不是失败的证据搜索。我们的研究结果构成的第一步，在定义一个统一的证明理论框架的逻辑配备了一个比较可验证性运营商。
2022-10-19 cs.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Uniform Cut-free Bisequent Calculi for Three-valued Logics
本文利用双矢列演算BSC统一形式化多种三值逻辑，并构造性证明所得系统无切、具子公式性质且常可推出插值定理。
2024-12-02 cs.LO
Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic -- Extended Version
全直觉线性逻辑（FILL）是用PAR扩展的乘法直觉线性逻辑。它的证明理论是出了名的难以得到正确的，现有的微积分都涉及带有复杂注释的推理规则，以保证可靠性和切割消除。我们给出了一个简单的和无注释的显示演算的填充，满足贝尔纳普的通用削减消除定理。要做到这一点，我们的显示演算实际上处理了FILL的扩展，称为双直觉线性逻辑（BiILL），通过一个带有par的附加词定义了一个“排除”连接词。我们完善我们的显示演算为BIILL到一个切自由嵌套的嵌套式演算与深推理，其中显式的结构规则的显示演算成为可接受的。分离性保证了在深度推理演算中FILL公式的证明不包含任何排除的痕迹。每个这样的规则对于FILL的语义来说都是合理的，因此我们的深度推理演算和显示演算相对于FILL是保守的。深度推理演算还具有子公式性质和终止反向证明搜索，这给出了BiILL和FILL的NP-完全性。
2013-07-18 cs.LO
Modularisation of Sequent Calculi for Normal and Non-normal Modalities
在这项工作中，我们探讨之间的连接（线性）嵌套的微积分和普通的微积分正常和非正常模态逻辑。通过提出本地版本的普通的正则化规则，我们得到线性嵌套正则化演算的一些逻辑，包括我们所知的第一个嵌套正则化演算的一个大类的简单依赖的多模态逻辑，和许多标准的非正常模态逻辑。由此产生的系统是模块化的，并有单独的左，右介绍规则的方式，这使得他们服从规范的双极条款。虽然这种颗粒的的证明搜索规则引入了更多的选择，我们展示了如何线性嵌套的证明演算可以限制到阻塞的推导，直接对应于普通的证明推导。
2017-11-16 cs.LO math.LO
Calculi for Intuitionistic Normal Modal Logic
本文给出了一个按名称调用和一个按值调用的项演算，它们都与直觉模态逻辑IK的盒片段有Curry-Howard对应关系。显示了结石的强归一化性和汇合性。此外，我们还定义了一个从按值调用演算到按名称调用演算的CPS转换，并证明了它的可靠性和完备性。
2016-06-10 cs.LO cs.PL
Normalization for Fitch-Style Modal Calculi
Fitch风格的模态lambda演算通过使用由锁表示的定界运算符扩展类型上下文，使编程能够在类型化λ演算中使用必要模态。锁的加入简化了包含不同模态公理的演算类型规则的制定，但每个变体都需要不同的，繁琐的和看似特别的语法引理来证明规范化。在这项工作中，我们采取了一种语义方法来规范化，称为评估规范化（NbE），通过利用Fitch风格演算的可能世界语义来产生一种更加模块化的规范化方法。我们表明，NBE模型可以构建为演算，将K，T和4公理的模态逻辑，作为合适的实例化的可能世界语义。除了现有的结果，处理β-等价，我们的归一化结果也考虑这些结石的η-等价。我们的关键成果已在证明助手阿格达机械化。最后，我们展示了几个后果的规范化证明元理论性质的Fitch式演算以及编程语言应用程序的基础上不同的解释的必要性模态。
2022-07-26 cs.LO cs.PL
Filtration and canonical completeness for continuous modal mu-calculi
连续模态μ演算是模态μ演算的一个片段，其中不动点算子的应用仅限于其函数解释是斯科特连续的公式，而不仅仅是单调的。通过博弈论的手段，我们表明，这个相对表现力的片段仍然允许基本模态逻辑，这是出了名的失败的充分模态μ演算：过滤和规范模型的两个重要技术。特别是，我们证明了过滤定理的公式在语言中的连续模态μ演算。因此，我们得到了有限的模型属性在广泛的模型类。此外，我们证明了，如果一个基本模态逻辑L是标准的和类的L-框架允许过滤，那么通过添加连续不动点算子L得到的逻辑是健全的和完整的关于类的L-框架。这概括了最近的结果严格较弱的片段的模态μ演算，即PDL。
2021-09-17 cs.LO
Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics
Technische Universität Wien（维也纳技术大学）
次协调逻辑是一类重要的形式主义，它处理来自不协调逻辑的非平凡推理。在本文中，我们引入了一致公理化的非单调次协调逻辑族的最小不一致的序列型证明系统。后者是演算的突出和广泛使用的形式，非常适合分析证明搜索。特别是，我们提供了序列型演算牧师的三值最小不一致逻辑的悖论，并为四值次协调推理关系，由于Arieli和Avron。我们的演算遵循Bonatti和Olivetti在非单调推理的背景下首次引入的方法，其显着特点是使用所谓的拒绝演算公理化无效公式。事实上，我们提出了一个通用的方法来获得任何多值逻辑的最小不一致的基础上的演算系统，产生的演算的逻辑的牧师和Arieli和Avron作为特殊情况。
2020-09-22 cs.AI cs.LO
Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics
Technische Universität Wien（维也纳技术大学）
本文是Berkel和Lyon于2019年发表的论文“时态STIT逻辑的免切演算和关系语义”的附录。给出了基本STIT逻辑Ldm（相对于非自反的时态Kripke STIT框架）的完备性证明，并推导了逻辑Xstit的主体独立性公理.
2019-02-18 cs.AI cs.LO
Hypersequent calculi for non-normal modal and deontic logics: Countermodels and optimal complexity
我们提出了一些超代数演算的所有系统的经典立方体和它们的公理$T$，$P$，$D$的扩展，并为每个$n\geq 1$，规则$RD^+_n$。演算是内部的，因为它们只使用逻辑语言，加上额外的结构连接词。我们表明，结石是完整的，相对于相应的axiomatisation的句法证明削减消除。然后，我们定义了一个终止根优先证明搜索策略的基础上的超演算，并证明它是最佳的coNP完全逻辑。此外，我们得到，从每一个饱和的叶失败的证明，有可能定义一个反模型的根hyperprandem的双邻域语义，并定期逻辑也在关系语义。最后，我们给出了一个翻译之间的hyperprinciple的应用程序和推导的标记系统的经典立方体。
2020-06-09 cs.LO math.LO
Cut-free Calculi and Relational Semantics for Temporal STIT Logics
Technische Universität Wien（维也纳工业大学）
我们提出了一个中央形式主义的代理逻辑：STIT逻辑与时间运营商的切割自由标记的微积分。其中包括用于Ldm、Tstit和Xstit的嵌入式系统。所有的结石都具有基本的结构特性，如收缩和切容许性。标记的结石G3Ldm和G3TSTIT相对于非自反的时间框架显示出健全和完整。此外，我们扩展目前的结果表明，也XSTIT可以通过关系框架，省略使用BT+AC框架的特点。
2019-04-22 cs.AI cs.LO math.LO
Extended Lambek calculi and first-order linear logic
CNRS（法国国家科学研究中心）；LaBRI（波尔多计算机科学实验室）
一阶乘法直觉线性逻辑（MILL 1）可以看作是Lambek演算的一个扩展。除了MILL 1的片段对应于Lambek演算（Moot & Piazza 2001），我将展示MILL 1的片段，它们生成多种上下文无关语言，并对应于Morrilll等人的位移演算。
2013-05-27 cs.CL cs.LO
Infinitary $λ$-Calculi from a Linear Perspective (Long Version)
我们介绍了一个线性无穷$λ$ -演算，称为$\ellΛ_{\infty}$，其中两个指数模态是可用的，第一个是通常的，有限的一个，另一个是唯一的构造解释共归纳。所得到的演算嵌入了无穷应用$λ$ -演算，并且对无穷字符串上的计算是通用的.关于$\ellΛ_{\infty}$特别有趣的是，由线性逻辑引起的细化允许限制两种模态，以便得到归纳终止和共归纳产生的结石。我们通过分析围绕$\mathsf{SLL}$和$\mathsf{4LL}$原则构建的$\ellΛ$片段来验证这一想法。有趣的是，它喜欢融合，相反，在普通的无穷$λ$ -结石发生的事情。
2016-04-27 cs.LO
Functions as proofs as processes
本文提出了一种将函数演算转换为并发进程演算的逻辑方法。出发点是与线性逻辑密切相关的π-演算的一个类型系统。将直觉逻辑和经典逻辑分解到这个系统中提供了λ演算和λμ演算的类型保持翻译，无论是按名称调用还是按值调用求值策略。先前已知的编码的\lam演算示出对应于这种逻辑嵌入的特定情况。π演算中类型的可实现性解释为这些翻译提供了系统的可靠性论证，并允许定义函数演算的类型安全扩展。
2011-07-21 cs.LO
Lax Modal Lambda Calculi
本文提出了一种基于Lax逻辑的类型lambda计算，为强functor提供了模态逻辑基础，并通过形式化验证证明了归约和等价完备性等结果。
2025-12-11 cs.LO cs.PL
Unified Gentzen Approach to Connexive Logics over Wansing's C
本文针对 Wansing 基本连接逻辑 C 之上由 Peirce 律、排中律及广义排中律扩展得到的 C-族逻辑，提出统一的 Gentzen 矢列演算与自然演绎系统，并证明两者等价以及切割消去与规范化定理。
2024-12-31 cs.LO
Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
本文提出二元混合逻辑的完备表记演算，同时构建了依赖维度的混合依赖积逻辑演算，并证明其完备性，但所有系统均不具终止性。
2023-11-14 cs.LO math.LO
Sequent Calculi for Data-Aware Modal Logics
本文从证明论视角研究数据感知混合模态逻辑HXpathD，提出了可靠完备的Gentzen式相继式演算，证明其规则可逆且满足切割消除，为数据感知模态逻辑及更广泛模态系统的证明论研究奠定基础。
2025-10-02 cs.LO
Disjunctive Axioms and Concurrent $λ$-Calculi: a Curry-Howard Approach
我们添加到直觉主义逻辑无穷多个经典的析取重言式，并使用库里-霍华德对应，以获得类型并发$λ$演算，他们每个人都具有特定的通信机制，包括广播和循环消息交换，并增强表达能力方面的$λ$演算。此外，它们都实现了代码移动性的形式。我们的结果提供了第一个并发计算解释许多命题中间逻辑，包括经典逻辑。
2018-02-13 cs.LO math.LO
Modular Labelled Sequent Calculi for Abstract Separation Logics
抽象分离逻辑是霍尔逻辑的一系列扩展，用于推理操纵诸如存储器位置之类的资源的程序。这些逻辑是“抽象的”，因为它们独立于任何特定的具体资源模型。他们的断言语言，称为命题抽象分离逻辑（PASL），以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。特别地，这些逻辑包含连接词$*$和$-\!*$，分别表示资源的组成和扩展。这种额外的表达能力是有代价的，因为所产生的逻辑都是不可判定的。鉴于其广泛的适用性，甚至半决策程序，这些逻辑是可取的。虽然在文献中讨论了几个PASL和它们与BBI的关系，但这些逻辑的证明理论和自动推理是本文的会议版本解决的开放问题，该版本使用无割标记演算为各种PASL开发了模块化证明理论。本文非平凡地改进了以前的工作，给出了一个一般框架的演算上的任何新的公理在逻辑满足一定的形式对应的推理规则在我们的框架，和完整性证明一般考虑这样的公理。我们的基础演算处理Calcagno等人。的原始逻辑的分离代数，增加了健全的规则，部分确定性和cancellativity，同时保持削减消除。然后，我们证明了分离逻辑中的许多重要性质，如不可分单元、不相交性、可分裂性和交叉分裂性，都可以用我们的一般公理形式表示。因此，我们的框架免费提供了这些属性的推理规则和完整性。最后，我们展示了我们的演算如何减少到具有全局标签替换的演算，从而实现更高效的实现。
2018-03-26 cs.LO cs.PL
Inducing syntactic cut-elimination for indexed nested sequents
本文通过建立标记相继式与索引嵌套相继式的对应关系，为索引嵌套相继式演算引入句法切割消去证明，并首次为中间逻辑构造了无切割的索引嵌套相继式演算。
2018-11-23 cs.LO
Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics
本文通过提出PTIME翻译和严格标签证明概念，建立了时态逻辑解析展示演算与标签相继式演算之间的多项式等价关系，证明标签形式体系包含并扩展了展示形式体系。
2024-06-28 cs.LO math.LO
Comparing Call-by-Name and Call-by-Value Reduction and Reduction Strategies in Calculi for Classical Logic
Imperial College London（帝国理工学院）
该研究对比了slmu、lmmt、Xs三种经典逻辑演算的CBN、CBV归约及策略，定义了演算间的映射与解释，明确了不同演算间归约概念的对应关系及编码的局限性。
2026-08-13 cs.LO
Forcing, Transition Algebras, and Calculi
提出转移代数逻辑系统，通过引入动态逻辑特性增强多类一阶逻辑，并推广力迫方法至标记范畴，证明了具有可数无限前提证明规则的完备性。
2024-04-24 cs.LO
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
语法逻辑是指多模态逻辑K的扩展，其中模态公理从形式语法生成。我们考虑一个证明理论，在嵌套微积分，与逆，即，语法逻辑，每个模态算子[a]都有一个逆。扩展以前的作品嵌套的tense逻辑系统，我们表明所有的语法逻辑（有或没有逆）可以在嵌套的tense演算，其中的公理是内在的演算作为结构规则的形式化。这些结石的语法切割消除证明使用类似的程序显示逻辑。如果文法是上下文无关的，那么可以摆脱所有的结构规则，支持深度推理和额外的传播规则。我们给出了一个新的半决策过程的上下文无关文法逻辑，使用嵌套的深度推理演算，并表明，在给定的上下文无关文法是正规的情况下，这个过程终止。与文献中所有其他现有的决策程序的规则文法逻辑，我们的程序不假设一个有限状态自动机编码的公理。
2012-04-11 cs.LO
An expressive completeness theorem for coalgebraic modal mu-calculi
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。然后，我们考虑下的行为等价的MSO公式的不变性。更具体地说，我们调查是否coalgebraic μ演算是一元二阶语言的一个给定的函子的bisimulation不变的片段。使用automatatattheoretic技术和建设最近的结果由第三作者，我们表明，为了提供这样的表征结果，它足以找到我们所谓的一个足够的一致建设的coalgebraic型函子。作为这个结果的直接应用，我们获得了部分新的证明的Janin-Walukiewicz定理的模态μ演算，避免使用语法范式，和互模拟不变的结果袋函子（分级模态逻辑）和所有指数多项式函子（包括"游戏函子"）。作为一个更复杂的应用程序，涉及额外的非平凡的想法，我们还得到了一个单调模态μ演算的特征定理，相对于自然的一元二阶语言单调邻域模型。
2017-06-30 cs.LO
Cut-free Completeness for Modular Hypersequent Calculi for Modal Logics K, T, and D
我们调查了最近的建议，模态hyperlipidic结石。关系超序列的解释包括沿超序列的可及性关系。这些系统给出了与Lellman的线性嵌套序列相同的超序列解释，但由Restall独立开发用于S5，并由Parisi扩展到其他正常模态逻辑。由此产生的系统遵循Dosen原则：模态规则在不同的模态逻辑中是相同的。不同的模态系统只在外部结构规则的存在或不存在方面有所不同。除了S5之外，这些系统都是模块化的，因为不同的结构规则捕获了可访问性关系的不同属性。我们提供了第一个直接的语义无割完备性证明K，T，和D，并展示了这种方法是如何失败的情况下B和S4。
2021-11-05 cs.LO math.LO
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
Technische Universität Wien（维也纳技术大学）
这项工作提供了证明搜索算法和自动反模型提取一类STIT逻辑。有了这个，我们回答了一个公开的问题，关于STIT逻辑的句法决策程序和无切演算。对至多n个选择的多智能体STIT问题，引入了一类新的无割完全标号演算G3LdmL^m_n.我们通过使用传播规则来精化演算G3LdmL^m_n，并证明其结构规则的可接受性，从而得到辅助演算Ldm^m_nL。在单代理的情况下，我们表明，精炼演算Ldm^m_nL推导定理在一个有限的类（森林状）序列，使我们能够提供证明搜索算法，决定单代理STIT逻辑。我们证明了证明搜索算法的正确性和终止性。
2020-02-15 cs.AI cs.LO cs.MA
Syntactic completeness of proper display calculi
最近的一系列结构证明理论的研究旨在探索分析演算的概念（即那些支持通用和模块化证明策略的演算），并确定可以根据这些演算捕获的逻辑类。在这种情况下，Wansing引入了适当显示演算的概念，作为证明演算的一个可能的设计框架，其中以特别透明的方式实现了分析性需求。最近，可适当显示逻辑（即那些可以用适当显示演算等价表示的逻辑）的理论已经与广义Sahlqvist理论（又名统一对应）联系起来发展。具体地说，可恰当显示逻辑在句法上被刻画为那些由解析归纳公理化的逻辑，这些公理可以等价地和算法地转化为解析结构规则，从而得到的恰当显示演算具有一组基本性质：可靠性、完备性、保守性、割消和子公式性质。在这种情况下，证明给定的演算是完整的w.r.t.原始逻辑通常在语法上执行，即，通过示出在基本系统中存在逻辑的每个给定公理的（无割）推导，其中从给定公理算法生成的分析结构规则已经被添加到该基本系统中。然而，到目前为止，这种证明策略的语法完整性已经实现了个案的基础上，而不是一般。在本文中，我们解决这个差距，证明在任何正常的（分配）格扩展签名正确显示逻辑的语法完备性。具体来说，我们表明，对于每一个分析归纳公理的切割自由推导可以有效地产生具有特定的形状，被称为前范式。
2021-02-23 cs.LO math.LO
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
本文探讨了基于序列的证明形式化方法的层级结构，分析了内部与外部演算的区别及其翻译难度。
2025-05-07 cs.LO math.LO
