From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics
本文将线性套序列和2-序列的方法推广到自然演绎中。公式用空间坐标装饰，允许按照自然演绎的原始精神制定形式系统--每个连接词只有一个引入和一个消除规则，没有额外的（结构）规则，没有明确引用预期的可及性关系克里普克模型。我们给出了从K到S4的正规模态逻辑系统。对于系统的直观版本，我们定义了证明约简，并证明了证明规范化，从而获得了一致性的语法证明。对于逻辑K和K4，我们使用存在谓词（遵循Scott）来制定合理的演绎规则。
2021-04-24 cs.LO
A sequent calculus with procedure calls
在本文中，我们扩展的演算LKF到演算LK（T），允许调用一个决策过程。我们证明了LK（T）的截消元。
2012-04-23 cs.LO
Parametricity for Nested Types and GADTs
本文为嵌套数据类型设计了一个Hindley-Milner风格演算，并构建了其参数模型，证明了抽象定理，可用于推导自由定理，同时论证了该模型无法扩展到GADT。
2021-12-22 cs.LO
Proof systems: from nestings to sequents and back
在这项工作中，我们将探讨证明理论之间的联系，嵌套和标记演算。特别是，我们展示了一个通用的算法，通过线性嵌套系统转换成类嵌套系统的微积分系统。此外，我们显示了所有这些系统的直觉，多模态和非正常模态逻辑的语义特征，通过一个由情况下的翻译之间的标记嵌套到标记嵌套系统。
2018-02-14 cs.LO
On Nested Sequents for Constructive Modal Logics
我们提出了各种模态逻辑的演绎系统，这些模态逻辑可以通过添加公理d，t，b，4和5的组合从正常模态逻辑CK的构造性变体中获得。这包括标准模态逻辑K4、S4和S5的构造变体。我们使用我们的演示形式主义的嵌套序列，并给出一个句法证明削减消除。
2015-09-02 cs.LO
Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus
无收缩BI演算的发展，无论是在G3i或G4i的意义上，在文献中还没有成功。我们提出了这样一个开放的问题，提出了一个系统。事实上，我们的微积分不涉及结构规则。
2014-04-24 cs.LO
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
本文针对可证性逻辑GL切割消去终止性证明困难的问题，提出基于嵌套矢列式的语法化切割消去方法，并借鉴Kushida（2020）的思想，仅用直接归纳避免额外度量和复杂重写，从而消除Poggiolesi（2009）证明中的歧义。
2024-12-31 cs.LO
A Labelled Sequent Calculus for Public Announcement Logic
公告逻辑（PAL）是认知逻辑（EL）的扩展，具有一些归约公理。在本文中，我们提出了一个无割标记的PAL演算，这是一个扩展的EL与简化公理的调整规则。这种演算允许切割，并允许终止证明搜索。
2022-10-27 cs.LO
On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
我们考虑两种风格的证明演算紧张的逻辑，在嵌套序列的基础上提出的形式主义的家庭。一个嵌套的序列可以看作是一个传统的单边序列树。我们的第一种演算风格被称为“浅演算”，其中推理规则仅应用于嵌套的根节点中的根结点。我们的浅层演算是鹿岛演算的时态逻辑的扩展，并与显示演算共享一个基本特征，即存在被称为“显示公设”的结构规则。浅层结石有一个简单的切割消除程序，但由于存在显示假设和其他结构规则，不适合进行证据搜索。第二种类型的演算使用深度推理，推理规则可以应用于嵌套的递归中的任何节点。我们表明，对于一系列的扩展时态逻辑，这两种风格的演算是等价的，并且有一个自然的证明理论之间的对应关系显示公设和深推理。深度推理演算具有子公式性质，没有显示公设或其他结构规则，这使得它们成为一个更好的证明搜索框架。
2011-05-14 cs.LO
Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Technische Universität Dresden（德累斯顿工业大学）
本文提出一种新的嵌套序列证明搜索方法，用于直觉时序逻辑，支持有限反模型提取。通过引入基于同态的回路检查方法，限制了证明搜索中推导的高度。由于某些推理规则不可逆，算法构建的是称为'计算树'的广义结构，展示了如何从计算树中提取证明和反模型。
2026-03-31 cs.LO
A Sequent Calculus for Modelling Interferences
一个逻辑演算，这是一个保守的线性逻辑的扩展。这项工作的动机涉及懒惰评估，真正的并发性和干扰证明搜索。该演算包括两个新的连接词来处理多重结构，并具有割消性质。扩展提出了第一个结果，我们的目标。
2007-06-22 cs.LO
A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version
双直觉主义逻辑是直觉主义逻辑的推广，它具有一个与蕴涵有关的联结对偶。双直觉逻辑是由Rauszer作为具有代数和Kripke语义的Hilbert演算引入的。但她随后对BiInt的"无切“演算最近被Uustalu证明是失败的。我们提出了一个新的切割免费的BiInt演算，并证明它的声音和完整的Kripke语义。确保完整性是复杂的含义和它的对偶之间的相互作用，类似于未来和过去的时态逻辑模态。我们的演算处理这种相互作用，使用扩展序列传递信息的前提下的结论，使用实例化的变量在失败的派生树的叶子。我们简单的终止论证允许我们的演算用于自动演绎，尽管这不是它的主要目的。
2007-04-17 cs.LO
From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus
我们研究了Pi演算，丰富了配对和非阻塞输入，并定义了一个使用类型构造函数“箭头”的类型赋值概念。我们编码电路的演算X到这个变种的Pi，并表明，所有的减少（削减消除）和可分配的类型被保留。由于X享有根岑演算LK的Curry-Howard同构，这意味着LK中的所有证明都有Pi的表示。
2011-09-22 cs.LO
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Peking University（北京大学）
本文为线性时态逻辑（LTL）构建非良基与循环线性嵌套矢列演算系统，解决循环识别与展开问题，提供多矢列形式体系中循环转换的新证明论技术。
2026-10-13 cs.LO
Sequent Calculus for Intuitionistic Epistemic Logic
直觉主义认知逻辑IEL的形式系统是由S. Artemov和T.原教皇它基于直觉主义的Brouwer-Hayting-Kolmogorov语义学，为从直觉主义的角度研究知识提供了形式化的基础。我们构造了IEL的一个无割演算，证明了在多项式空间中进行证明搜索是充分的，从而证明了IEL是PSPACE-完全的。
2015-08-31 cs.LO
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
我们提出了一个标记的布尔BI演算，一个经典的变种的O'Hearn和Pym的逻辑的集束蕴涵。微积分是简单的，健全的，完整的，并享受削减消除。我们表明，在我们的证明系统中的所有结构规则，包括那些规则，操纵标签，可以本地化周围的应用程序的某些逻辑规则，从而本地化这些规则的处理证明搜索。在此基础上，我们展示了一个自由变量演算，处理结构规则懒在约束系统。最后提出了一种求解约束的探试法，并给出了实验结果。
2015-05-04 cs.LO
Sequent Calculus and Equational Programming
基于类型论的证明助手和程序设计语言通常有两种风格：一种是基于类型论的标准自然演绎表示，并涉及消除器，而另一种是提供等式风格的语法。我们在这里表明，方程的方法对应于使用一个集中的介绍类型论表示为微积分。一个类型化的函数语言，基于一个代数演算，我们涉及到的语法和内部语言的Agda。特别是，我们讨论了使用的模式和情况下分裂，以及规则实现归纳推理和相关产品和总和。
2015-07-29 cs.LO
A Proof Tree Builder for Sequent Calculus and Hoare Logic
我们已经开发了一个基于Web的教学证明助手，证明树生成器，它可以让你从最初的目标向上应用规则在微积分和霍尔逻辑的一个简单的命令式语言。我们配备了一个基本的证明自动化功能和Z3集成我们的工具。普林斯顿大学自动推理课程的学生使用了我们的工具，并发现它很直观。证明树生成器可在https://proof-tree-builder.github.io上在线获得。
2023-03-10 cs.LO
Nested Sequents
我们看到如何嵌套序列，超序列的自然概括，使我们能够开发一个系统的模态逻辑证明理论。与其他突出的形式主义，如显示演算和标记序列相反，嵌套序列留在模态语言中，并允许在字面意义上享受子公式属性的证明系统。在第一部分中，我们研究了一套系统的嵌套系统的所有正常模态逻辑形成的一些组合的公理的序列性，自反性，对称性，传递性和欧几里德。我们建立健全性和完整性和他们的一些良好的性质，如可逆的所有规则，结构规则的可接受性，终止证明搜索，以及句法切割消除。在第二部分中，我们研究了常识逻辑，一种具有不动点模态的模态逻辑。我们期待在两个无穷证明系统，这种逻辑：现有的一个普通序列的基础上，没有语法切割消除程序是已知的，和一个新的嵌套序列的基础上。我们看到如何嵌套的序列，在普通的序列相比，允许句法削减消除，从而使我们能够获得一个序数上限的长度证明。
2010-04-11 cs.LO math.LO
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
本文利用线性嵌套框架设计了一种新的直觉模糊逻辑--一阶Gödel逻辑的无割演算LNIF。线性嵌套序列-这是嵌套序列限制线性结构-证明是一个很好的证明理论的形式主义直觉模糊逻辑。我们发现，演算LNIF具有非常理想的证明理论的性质，如可逆的所有规则，结构规则的容许性，和句法切割消除。
2020-10-04 cs.LO math.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
Nested Sequents for Provability Logic GLP
本文提出了一种基于嵌套相继式的可证性逻辑GLP证明系统，证明了切消定理，并以此在语法上将GLP归约为其重要片段J。
2014-10-24 cs.LO math.LO
A simple sequent calculus for nominal logic
名词逻辑是一阶逻辑的变体，它支持抽象语法中的绑定名称的推理。名词逻辑的一个关键特征是新量词，它对新名称（迄今为止未出现在任何值中的名称）进行量化。以前的尝试已经作出了开发方便的规则推理与新的量词，但我们认为，这些尝试都是不完全令人满意的。在这篇文章中，我们开发了一个新的numerical演算的名义逻辑中的规则，新的量词是比以前的尝试简单得多。我们还证明了几个结构和元理论的性质，包括削减消除，一致性，和等价的皮茨公理化的名义逻辑。
2013-12-17 cs.LO
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
本文通过引入线性规则和可达性规则，并推广嵌套矢列以包含签名，为命题及一阶Gödel-Dummett逻辑构建了具有高度保持可逆性、可靠且无割完备的嵌套矢列系统，同时为更广泛的中间逻辑提供了无割嵌套矢列系统的构造思路。
2024-06-06 cs.LO math.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Proof Analysis of A Foundational Classical Singlesuccedent Sequent Calculus
本文论证现有经典单后件矢列演算均不足以继承 Gentzen 的 LK 系统，并提出专为满足经典证明论期望而设计的 G-Calculus 经典部分 Gc。
2025-07-06 cs.LO
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
我们描述了SeCaV，一阶逻辑在Isabelle/HOL，和SeCaV Unshortener，一个在线工具，扩展到完整的SeCaV语法简洁的推导的一阶逻辑的微积分验证。我们利用Isabelle/HOL作为SeCaV推导的证明检查器。Isabelle/HOL的交互功能使我们的系统透明。例如，用户可以简单地点击一个边条件来查看它的确切定义。我们的形式化的可靠性和完整性证明完全适用于暴露给用户的微积分，而不仅仅是我们工具的一些模型。用户还可以在SeCaV Unshortener中编写他们的派生，它提供了更轻的语法，并扩展它们以供以后验证。我们在教学中使用了这两种工具。
2022-04-08 cs.LO
A Sequent Calculus Proof Search Procedure and Counter-model Generation based on Natural Deduction Bounds
在之前发表的ENTCS论文（Santos et al.（2016））中，我们介绍了一种名为$\mathbf{LMT^{\rightarrow}}$的最小蕴涵命题逻辑（$\mathbf{LMT^{\rightarrow}}$）的微积分。该演算为$\mathbf{LMT^{\rightarrow}}$提供了一个自底向上的证明搜索过程。我们在那里证明了$\mathbf{LMT^{\rightarrow}}$是可靠和完备的。我们还提出了一个策略，以保证终止的证据搜索过程。在本文中，我们改进了这种策略，并提出了一种新的策略，$\mathbf{LMT^{\rightarrow}}$终止。考虑到这种新的策略，我们还提供了一个（新的）完整性证明的系统，这改善了以前的版本。除此之外，我们提出了明确的上限证明搜索过程中，来自这个新的策略。并对系统的可靠性进行了充分的证明。
2020-02-01 cs.LO
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
Nested Sequents for Quasi-transitive Modal Logics
本文针对带拟传递性公理的模态逻辑，基于嵌套矢列式提出构造性切割消去程序，并给出替代性的模块化证明系统表述。
2024-06-13 cs.LO math.LO
Sequent Calculus in the Topos of Trees
中野的“后来”模态，受到哥德尔-洛布可证明性逻辑的启发，已被应用于类型系统和程序逻辑中，以捕获保护递归。Birkedal等人通过树的拓扑的内部逻辑来模拟这种模态。我们证明了该逻辑的命题片段的语义可以由线性逆良基直觉Kripke框架给出，因此该逻辑是直觉模态逻辑KM和中间逻辑LC的结合。因此，我们称这种逻辑为$\mathrm{KM}_{\mathrm{lin}}$。通过将蕴涵分解为静态蕴涵和非自反蕴涵的策略，给出了$\mathrm{KM}_{\mathrm{lin}}$的一个可靠的无割完备蕴涵演算。我们的演算提供了确定性和终止向后证明搜索，产生的逻辑和其有效性问题的coNP-完全性的可判定性。我们的演算和决策过程可以被限制为降低线性，从而捕获KM。
2015-04-17 cs.LO
A Sequent Calculus For Trace Formula Implication
Technical University of Darmstadt（达姆施塔特工业大学）
针对迹公式间蕴含关系证明缺失限制现有迹规约演算应用的问题，本文提出结合不动点归纳、契约与μ-公式同步的可靠矢列演算，可证明迹公式蕴含的多类非平凡性质。
2025-11-17 cs.LO
A Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文提出SCFO(ID)演算，用于处理非单调归纳定义，通过稳定语义验证其理论性质，支持对一般归纳定义的定理形式化证明。
2026-09-23 cs.LO
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL cs.LO
Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus
我们的论文有两个目的：本文首先在Chlebowski和Leszczynska-Jasion的论文“An Investigation into Intuitionistic Logic with Identity”中提出的演算的基础上，给出了一个直觉主义非Fregean逻辑ISCI的演算（Bulletin of the Section of Logic 48（4），p. 259-283，2019），其次，我们通过所获得的系统讨论ISCI的可判定性问题。上述论文中的原始演算没有为ISCI提供可判定性结果。为了得到这个结果，有两个问题需要解决：直觉逻辑的所谓循环特性和由于身份专用规则的形式而缺乏子公式性质。我们讨论可能的路线，以克服这些问题：我们考虑一个较弱的版本的子公式属性，守卫的复杂性公式，可以包括在它里面，我们还提出了一个证明搜索过程，当它失败时，然后存在一个反模型（在Kripke语义ISCI）。
2022-04-14 cs.LO
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Curien和Herbelin的λ mu mu-演算的按名称调用版本的直观片段被隔离，并通过嵌入到简单类型的λ mu-演算中来证明其强规范化。我们的嵌入是一个延续和垃圾传递风格的翻译，灵感来自Ikeda和Nakazawa的Parigot的λ\_mu演算的翻译。嵌入严格模拟约简，而通常的连续传递式转换删除置换约简步骤。对于我们的直觉主义微积分，我们甚至只需要传递“垃圾单元”。我们将同样的方法应用于其他演算，即简单类型演算的连续扩展导致我们的直觉系统，并且已经对于我们考虑的最简单的扩展（具有广义应用的演算），这产生了通过约简保持嵌入的强规范化的第一个证明。所得到的结果扩展到第二和更高的阶结石。
2009-05-25 cs.LO
Modularisation of Sequent Calculi for Normal and Non-normal Modalities
在这项工作中，我们探讨之间的连接（线性）嵌套的微积分和普通的微积分正常和非正常模态逻辑。通过提出本地版本的普通的正则化规则，我们得到线性嵌套正则化演算的一些逻辑，包括我们所知的第一个嵌套正则化演算的一个大类的简单依赖的多模态逻辑，和许多标准的非正常模态逻辑。由此产生的系统是模块化的，并有单独的左，右介绍规则的方式，这使得他们服从规范的双极条款。虽然这种颗粒的的证明搜索规则引入了更多的选择，我们展示了如何线性嵌套的证明演算可以限制到阻塞的推导，直接对应于普通的证明推导。
2017-11-16 cs.LO math.LO
The Hidden Structural Rules of the Discontinuous Lambek Calculus
Lambek演算L（lambek 58）的Lambek演算sL没有结构规则。有趣的是，sL等价于一个多峰演算mL，它由非结合的Lambek演算和结合性的结构规则组成。本文证明了不连续Lambek演算（Morrill和Valentín）中的无结构规则的非连续演算或超连续演算hD也等价于一个Omega排序的多峰演算mD.更具体地说，我们提出了一个忠实的嵌入mD和hD之间的翻译，以这样一种方式，它可以说，hD吸收mD的结构规则。
2013-06-06 cs.LO
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Bologna（博洛尼亚大学）
本文提出了一种无割的嵌套序列系统，用于处理具有内外域的量模态逻辑，通过可达规则实现域条件的自然定义，并证明了系统的完备性和证明论性质。
2026-04-20 cs.LO 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
A sequent calculus with dependent types for classical arithmetic
在最近的一篇论文中，Herbelin开发了一种演算dPA $^ω$，其中可数和依赖选择公理的构造性证明可以通过将可数全称量化的证明编码为一个组件流来推导。然而，规范化的属性（因此也是健全性的属性）只是被证明了。规范化证明的困难在于依赖依赖类型的同时存在（对于选择的建设性部分），控制运算符（用于经典逻辑），共归纳对象（将$N\rightarrow A$类型的函数编码为流$(a_0,a_1,\ldots)$）和具有共享的惰性求值（对于这些共归纳对象）。建立在以前的作品，我们在本文中介绍了一个变种的dPA $^ω$提出的一个微积分。一方面，我们利用我们开发的Krivine经典可实现性的一个变体来证明经典按需调用的规范化。另一方面，我们受益于dL，一个经典的依赖类型的微积分，其中类型安全是确保使用定界的延续与语法限制。通过结合这些文件中开发的技术，我们设法定义一个可实现的解释我们的微积分，使我们能够证明规范化和健全的。
2018-12-20 cs.LO
Multimodality in the Hypergraph Lambek Calculus
本文将多模态兰贝克演算嵌入超图兰贝克演算 HL，证明 HL 的通用性，并通过超边替换将交换性与结合性纳入矢列结构，同时显式化模态的剩余性质。
2023-08-08 cs.LO
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.LO
The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
我们提出了序列演算训练器，一个工具，支持学生学习如何正确地构建证明的一阶逻辑与平等的微积分。它是一个证明助手，促进对构造正确证明所需遵守的所有句法原则的理解。它并没有提供任何帮助，在寻找良好的证明策略。相反，它的目的是在一个较低的句法层次上理解微积分，在考虑证明策略之前需要掌握它。其主要特点是在图形用户界面中嵌入了适当的反馈系统。我们还报告了一些实证研究结果，表明如何顺序演算训练可以提高学生的成功学习微积分的完整的一阶逻辑。
2015-07-14 cs.CY cs.LO
Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
我们考虑了双直觉逻辑与时态逻辑Kt的传统模态的扩展。从理论上证明，这种扩展是简单地通过扩展现有的双直觉逻辑的演算与显示逻辑中使用的模态的典型推理规则。事实证明，由此产生的演算LBiKt似乎比文献中考虑的大多数直觉时态或模态逻辑更基本，特别是Ewald和Simpson研究的那些，因为它没有假设菱形和盒子模态算子之间的任何先验关系。我们恢复Ewald的直觉时态逻辑和Simpson的直觉模态逻辑的模块化扩展LBiKt与额外的结构规则。演算LBiKt是以显示演算的一种变体形式来公式化的，使用一种称为嵌套序列的序列形式。切割消除证明LBiKt，使用类似的技术，在显示结石。与显示演算一样，LBiKt的推理规则是“浅”规则，也就是说它们作用于嵌套表达式中的顶级公式。演算LBiKt不适合向后证明搜索，因为存在某些称为“显示假设”的结构规则和任意结构上的压缩规则。我们表明，这些结构规则可以在另一个演算，DBiKt，它使用深度推理，允许一个应用推理规则在任意深度的嵌套的嵌套的。我们证明了LBiKt和DBiKt之间的等价性，并概述了DBiKt的证明搜索策略。我们还给出了一个Kripke语义，并证明了LBiKt是健全的语义，但完整性仍然是一个开放的问题。然后我们讨论LBiKt的各种扩展。
2010-06-29 cs.LO
The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality
我们展示了Leibnitz的不变性原理和Gentzen的原始工作是如何将微积分推广到具有等式的一阶逻辑的，并研究了割消性质。进一步讨论并改进了Lifshitz和Orevkov的不伸长性.
2017-05-01 cs.LO math.LO
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
逻辑学和类型论中的基本证明搜索策略可以被看作是规则在适当的微积分中的根优先应用，最好没有由规则置换产生的冗余。本文讨论的问题，定义这样的纯类型系统（PTS，这是最初提出的自然演绎风格），然后组织他们的规则，有效的证明搜索。我们引入纯类型序列演算与元变量（PTSCalpha）的想法，通过丰富的语法的置换自由演算的命题逻辑由于Herbelin，这是密切相关的自然演绎和已经很好地适应证明搜索。的操作语义是改编自Herbelin的，并定义了一个系统的本地重写规则，在削减消除，使用明确的替代。我们证明了这个系统的融合。限制我们的注意力PTSC，这个系统的地面条款的类型系统，我们得到的主题约简属性，并表明每个PTSC是逻辑等价于其相应的PTS，前者是强正规化的当且仅当后者是。我们展示了如何使PTSC的逻辑规则到一个语法导向的系统PS证明搜索，通过将转换规则的类型检查的PTS规则的语法导向的演示文稿。最后，我们考虑如何使用PTSCalpha的显式作用域元变量来表示部分证明项，并使用它们来分析交互式证明构造。这建立了一个框架PE，我们能够研究证明搜索策略，类型居民枚举和（高阶）统一。
2011-03-23 cs.LO
Nested Sequents for First-Order Modal Logics via Reachability Rules
本研究提出首个支持多种论域与路径条件的一阶模态逻辑无切割嵌套矢列系统，通过可达性规则与结构精化方法构建，证明了结构精化可扩展至一阶模态逻辑领域。
2023-11-08 cs.LO math.LO
Focalization and phase models for classical extensions of non-associative Lambek calculus
Lambek的非联想句法演算（NL）在其资源意识方面表现出色：通常的弱化，收缩，交换甚至结合性的结构规则都被丢弃。最近，有人提出了一些保守的扩展，以免除NL对具有单一结论的序列的直觉偏见：De Groote和Lamarche的经典非结合Lambek演算（CNL）和Moortgat及其同事的Lambek-Grishin演算（LG）。我们证明了Andreoli的聚焦属性所述的建议：一个规范化的结果，确定在很大程度上，那些不同的只是由平凡的规则排列的切免费的cirrhosis推导。在这样做的时候，我们从一个“统一的”CCN介绍，通过增加结构规则从LG派生CNL。规范化的证明收益的句法阶段模型的建设，其中每一个“真理”有一个集中的证明，类似于冈田和Herbelin和李的工作。
2011-06-02 cs.LO
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
TU Dresden（德累斯顿工业大学）；Peking University（北京大学）
本文针对线性时序逻辑（LTL），引入并研究非良基和循环线性嵌套相继式演算，通过饱和递归和规则前移技术，解决了从非良基证明中提取循环证明（循环识别）以及反向转换（展开）两个核心问题。
2026-10-06 cs.LO math.LO
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO 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
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
本文提出了一种用于CK、CK+ID、CK+MP和CK+MP+ ID等标准条件逻辑的无割演算SeqS.该演算使用标号和转移公式，可用于证明相应逻辑的可判定性和空间复杂度界.我们还提出了CondLean，这些逻辑实现SeqS演算SICStus Prolog写的定理证明。
2004-07-29 cs.AI cs.LO
Induction and Co-induction in Sequent Calculus
证明搜索已被用于指定广泛的计算系统。为了建立一个框架，这样的规范推理，我们使用了一个微积分，涉及感应和共感应。这些证明原则是基于定义的证明理论（而不是集合论）概念。定义类似于（分层的）逻辑程序，其中定义原子的左规则和右规则允许人们将理论视为“封闭的”或定义不动点。定义的使用使得对句法进行内涵推理成为可能，特别是通过统一来强制自由平等。我们以一致的方式添加规则前和后固定点，从而允许用户的原因归纳和共归纳的计算系统的属性，充分利用高阶抽象语法。一致性是保证通过削减消除，在那里，我们给第一，据我们所知，削减消除程序存在的一般归纳和共归纳的定义。
2009-09-30 cs.LO
