Nested Sequents for Provability Logic GLP
本文提出了一种基于嵌套相继式的可证性逻辑GLP证明系统，证明了切消定理，并以此在语法上将GLP归约为其重要片段J。
2014-10-24 cs.LO math.LO
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
本文通过引入线性规则和可达性规则，并推广嵌套矢列以包含签名，为命题及一阶Gödel-Dummett逻辑构建了具有高度保持可逆性、可靠且无割完备的嵌套矢列系统，同时为更广泛的中间逻辑提供了无割嵌套矢列系统的构造思路。
2024-06-06 cs.LO math.LO
Nested Sequents for Quasi-transitive Modal Logics
本文针对带拟传递性公理的模态逻辑，基于嵌套矢列式提出构造性切割消去程序，并给出替代性的模块化证明系统表述。
2024-06-13 cs.LO math.LO
Modularisation of Sequent Calculi for Normal and Non-normal Modalities
在这项工作中，我们探讨之间的连接（线性）嵌套的微积分和普通的微积分正常和非正常模态逻辑。通过提出本地版本的普通的正则化规则，我们得到线性嵌套正则化演算的一些逻辑，包括我们所知的第一个嵌套正则化演算的一个大类的简单依赖的多模态逻辑，和许多标准的非正常模态逻辑。由此产生的系统是模块化的，并有单独的左，右介绍规则的方式，这使得他们服从规范的双极条款。虽然这种颗粒的的证明搜索规则引入了更多的选择，我们展示了如何线性嵌套的证明演算可以限制到阻塞的推导，直接对应于普通的证明推导。
2017-11-16 cs.LO math.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
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.LO
Nested Sequents for First-Order Modal Logics via Reachability Rules
本研究提出首个支持多种论域与路径条件的一阶模态逻辑无切割嵌套矢列系统，通过可达性规则与结构精化方法构建，证明了结构精化可扩展至一阶模态逻辑领域。
2023-11-08 cs.LO math.LO
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Peking University（北京大学）
本文为线性时态逻辑（LTL）构建非良基与循环线性嵌套矢列演算系统，解决循环识别与展开问题，提供多矢列形式体系中循环转换的新证明论技术。
2026-10-13 cs.LO
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
Technische Universität Dresden（德累斯顿工业大学）
研究哥德尔-勒布可证性逻辑的多个相继式形式体系间证明的互译性。通过重组树形超相继式证明及引入‘线性化技术’解决问题，获首个无切割线性嵌套相继式演算，建立各系统间证明对应关系。
2026-07-07 cs.LO math.LO
Normal Nested Answer Set Programs: Syntactics, Semantics and Logical Calculi
本文定义了正规嵌套程序（NNP）的语法、语义及嵌套逻辑演算，填补了嵌套回答集程序推理能力的空白，并证明了相关计算复杂性。
2025-04-07 cs.LO
Uniform interpolation via nested sequents and hypersequents
最近开发了一个模块化证明理论框架，以证明Craig插值的正常模态逻辑的基础上推广的微积分（例如，嵌套序列、超序列和标记序列）。在本文中，我们转向一致插值，这是强于克雷格插值。给出了一种构造性的嵌套序列一致插值证明方法，并应用该方法重新证明了正规模态逻辑$\mathsf{K}$，$\mathsf{D}$和$\mathsf{T}$的一致插值性质.然后，我们使用的诀窍开发的嵌套序列应用相同的方法超序列，并获得了第一个直接证明的均匀插值$\mathsf{S5}$通过一个无割序列的演算。虽然我们的方法是证明理论的，但嵌套序列和超序列的均匀插值的定义也使用了语义概念，包括互模拟模原子命题。
2021-05-23 cs.LO
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL cs.LO
Grafting Hypersequents onto Nested Sequents
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
2015-08-10 cs.LO math.LO
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
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
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
语法逻辑是指多模态逻辑K的扩展，其中模态公理从形式语法生成。我们考虑一个证明理论，在嵌套微积分，与逆，即，语法逻辑，每个模态算子[a]都有一个逆。扩展以前的作品嵌套的tense逻辑系统，我们表明所有的语法逻辑（有或没有逆）可以在嵌套的tense演算，其中的公理是内在的演算作为结构规则的形式化。这些结石的语法切割消除证明使用类似的程序显示逻辑。如果文法是上下文无关的，那么可以摆脱所有的结构规则，支持深度推理和额外的传播规则。我们给出了一个新的半决策过程的上下文无关文法逻辑，使用嵌套的深度推理演算，并表明，在给定的上下文无关文法是正规的情况下，这个过程终止。与文献中所有其他现有的决策程序的规则文法逻辑，我们的程序不假设一个有限状态自动机编码的公理。
2012-04-11 cs.LO
On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
我们考虑两种风格的证明演算紧张的逻辑，在嵌套序列的基础上提出的形式主义的家庭。一个嵌套的序列可以看作是一个传统的单边序列树。我们的第一种演算风格被称为“浅演算”，其中推理规则仅应用于嵌套的根节点中的根结点。我们的浅层演算是鹿岛演算的时态逻辑的扩展，并与显示演算共享一个基本特征，即存在被称为“显示公设”的结构规则。浅层结石有一个简单的切割消除程序，但由于存在显示假设和其他结构规则，不适合进行证据搜索。第二种类型的演算使用深度推理，推理规则可以应用于嵌套的递归中的任何节点。我们表明，对于一系列的扩展时态逻辑，这两种风格的演算是等价的，并且有一个自然的证明理论之间的对应关系显示公设和深推理。深度推理演算具有子公式性质，没有显示公设或其他结构规则，这使得它们成为一个更好的证明搜索框架。
2011-05-14 cs.LO
Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement
本文通过结构细化方法，为直觉语法学逻辑构建了无割嵌套序列表演系统，并证明了其保守性、不可判定性和可判定子类。
2025-12-03 cs.DM cs.LO math.LO
Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Technische Universität Dresden（德累斯顿工业大学）
本文提出一种新的嵌套序列证明搜索方法，用于直觉时序逻辑，支持有限反模型提取。通过引入基于同态的回路检查方法，限制了证明搜索中推导的高度。由于某些推理规则不可逆，算法构建的是称为'计算树'的广义结构，展示了如何从计算树中提取证明和反模型。
2026-03-31 cs.LO
Nested-sequent Calculus for Modal Logic MB
本文针对模态逻辑 MB 的完全性与可判定性未决问题，构造了其嵌套矢列演算并加以解决，同时探讨了添加新模态符号后的逻辑 MB+。
2024-12-31 cs.LO
Automating Reasoning with Standpoint Logic via Nested Sequents
TU Dresden（德累斯顿工业大学）
立场逻辑是最近提出的形式主义的背景下，知识的整合，它提倡一个多视角的方法，允许推理的选择不同的，可能相互冲突的立场，而不是强迫他们的统一。在本文中，我们介绍了嵌套的立场逻辑-证明系统，操纵树的节点是多套公式-并展示了如何自动化的立场推理的非确定性证明搜索算法。为了获得最坏情况下的复杂性最优的证明搜索，我们介绍了一种新的技术，在嵌套序列的上下文中，被称为“着色”，其中包括一个公式作为输入，猜测一定的着色其子公式，然后运行证明搜索在嵌套的递归演算上的彩色输入。我们的技术可以让我们决定的有效性，在CoNP的立场公式，因为证明搜索只产生一个部分的证明相对于每个允许的着色的输入。我们展示了如何将所有部分证明融合在一起，以构建一个完整的证明时，输入是有效的，以及如何某些部分证明可以转化为一个反模型时，输入是无效的。这些“证明”（即证明和反模型）作为输入有效性的解释。
2022-05-05 cs.AI cs.DS cs.LO
Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
本文为Fischer Servi的直觉主义模态逻辑IK及其扩展提供证明逻辑对应物，通过扩展证明项语法、公理化和无切嵌套序列系统实现语法实现。
2025-07-12 cs.LO math.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization
我们证明了语法的合理性与自由变量和飞行Skolemization的经典tableaux。合理性证明通常是从语义论证中建立起来的，据我们所知，这是第一个诉诸句法手段的证明。实际上，我们证明了可靠性的性质，关于无割微积分。这需要非常小心，因为使用Skolem术语允许新鲜度检查的额外自由。在对比语义的健全性，我们获得的可能性，以国家削减消除定理的微积分，前提条件下，该方法的完整性举行。我们相信，这种技术也可以应用于其他逻辑中的tableaux。
2015-05-23 cs.FL cs.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
The Bedwyr system for model checking over syntactic expressions
Bedwyr是逻辑编程的一种推广，它允许直接对可能包含绑定的语法表达式进行模型检验。这个系统是用OCaml编写的，是证明搜索理论中两个最新进展的直接实现。第一个是集中在这样一个事实，即有限的成功和有限的失败都可以捕获在微积分通过纳入推理规则的定义，允许不动点进行探索。因此，证明搜索在这样一个演算可以捕捉简单的模型检验问题，以及可能和必须行为的操作语义。第二个是使用术语级$λ$绑定器和$\nabla$量词直接支持高阶抽象语法。这些功能允许直接在包含绑定变量的表达式上进行推理。
2008-04-25 cs.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
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
微积分是一种证明一阶逻辑中陈述有效性的形式主义。它通常用于计算机科学数学逻辑模块。形式证明在微积分中是有限的树，通过连续地将证明规则应用于公式，从而逐步简化它们。学生们经常在诸如形式逻辑和形式证明等主题所涉及的数学形式和抽象层次上挣扎。这些困难可以归类为句法或语义。在句法层面上，学生需要理解什么是正确形式的证明，如何在不脱离微积分的数学框架的情况下应用规则（例如在纸上），等等;除此之外，在语义层面上，学生需要掌握找到正确证明的策略。序贯微积分训练器是一个工具，旨在帮助学生学习正式证明给定语句的技术。在本文中，我们描述的教学动机背后的工具和技术，用于解决问题的句法以及语义层面上。
2018-03-05 cs.CY cs.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
The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
我们提出了序列演算训练器，一个工具，支持学生学习如何正确地构建证明的一阶逻辑与平等的微积分。它是一个证明助手，促进对构造正确证明所需遵守的所有句法原则的理解。它并没有提供任何帮助，在寻找良好的证明策略。相反，它的目的是在一个较低的句法层次上理解微积分，在考虑证明策略之前需要掌握它。其主要特点是在图形用户界面中嵌入了适当的反馈系统。我们还报告了一些实证研究结果，表明如何顺序演算训练可以提高学生的成功学习微积分的完整的一阶逻辑。
2015-07-14 cs.CY cs.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
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
TU Dresden（德累斯顿工业大学）
针对 GL 逻辑在树-超矢列系统 CSGL 中的可判定性证明和 PSPACE 证明搜索算法问题，提出线性化方法，仅构建单分支推导和树矢列，实现 PSPACE 最优复杂度，并提取有限反模型验证算法正确性。
2026-08-11 cs.LO math.LO
A Kruskal Decision Procedure for Intuitionistic Modal Logic IK4
Scuola Normale Superiore（意大利高等师范学院）
该研究提出了直觉模态逻辑IK4的Kruskal判定程序，通过无切嵌套证明结合Kruskal定理等证明其可判定性，给出了统一的证明高度界。
2026-08-12 cs.LO
A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
本文为直觉主义模态逻辑 IK 提出无标签双嵌套矢列演算，支持判定、由失败证明直接构造有限反模型，并可模拟现有嵌套与标签演算。
2025-05-13 cs.LO
Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
本文将证明 Craig 与 Lyndon Interpolation 的方法扩展至标号矢列演算，提供了基于 Kripke-frame 表征的充分准则，并证明无量词 Horn 公式可定义的框架类对应具有 IPs 的逻辑，涵盖模态立方体与传递 Geach 逻辑族。
2016-01-21 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
Circular Proofs for Gödel-Löb Logic
我们提出了一个序列式证明系统的可证明性逻辑GL，承认所谓的循环证明。对于这些证明，证明的基础图不是有限树，但允许包含循环。作为应用，我们在语法上建立了GL的Lindon插值.
2014-01-16 cs.LO math.LO
Refining Labelled Systems for Modal and Constructive Logics with Applications
Australian National University（澳大利亚国立大学）；Laboratoire d’informatique de l’École polytechnique（巴黎综合理工学院计算机实验室）
本文介绍了“结构精化方法”，它作为一种手段转换的模态和/或建设性逻辑的关系语义到一个“经济”的证明系统，通过连接两个证明理论的范式：标记和嵌套演算。标记序列的形式主义已经成功地在拥有理想的证明理论的性质，可以自动生成大型类的逻辑切割免费演算。尽管有这些品质，标记系统使用了复杂的语法，明确地结合了相关逻辑的语义，这样的系统通常违反了子公式属性的高度。相比之下，嵌套微积分使用更简单的语法，并坚持严格阅读子公式属性，使这样的系统在自动推理算法的设计中非常有用。然而，嵌套演算范式的缺点是，关于这种演算的自动构造（如在标记设置中）的一般理论基本上是不存在的，这意味着嵌套系统的构造和它们的属性的确认通常是在个案的基础上完成的。细化方法连接这两种范式在一个富有成效的方式，通过转换成嵌套的（或，精制标记）系统与前保持整个转换过程中的属性标记系统。为了证明精化的方法和它的一些应用，我们考虑文法逻辑，一阶直觉逻辑和道义STIT逻辑。介绍了细化标记演算将被用来提供第一个证明搜索算法的道义STIT逻辑。此外，我们使用我们的精炼标记演算的语法逻辑，以表明在类中的每一个逻辑具有有效的林登插值属性。
2021-07-30 cs.AI cs.DM cs.FL
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
Streamlining Input/Output Logics with Sequent Calculi
本研究通过面向证明搜索的序列演算简化Bochman的因果输入/输出（I/O）逻辑，建立其与原始I/O逻辑可推导性的句法语义联系，获得新语义、复杂度界等成果，统一解决相关未决问题。
2023-06-15 cs.LO
A Decidable Class of Nested Iterated Schemata (extended version)
Grenoble University（格勒诺布尔大学）；CNRS（法国国家科学研究中心）
许多问题可以通过依赖于参数的命题公式的模式来指定，例如，电路的规格通常取决于其输入的位数。我们定义了一个逻辑的公式，称为“迭代图式”，允许表达这样的模式。图式用索引命题（如P_i，P_i+1，P_1）和广义连接词（如/i=1）扩展命题逻辑。n或i=1.. n（称为“迭代”），其中n是称为“参数”的（未绑定）整数变量。迭代模式的表达能力严格地大于命题逻辑：它甚至超出了一阶逻辑的范围。我们定义了一个证明过程，称为DPLL*，可以证明一个模式是满足至少一个值的参数，在精神的DPLL过程。然而，相反的问题，即证明模式对于参数的每个值都是不可满足的，是不可判定的，所以DPLL* 一般不会终止。尽管如此，我们证明，它终止的语法子类称为“定期嵌套”的模式。这是第一个非平凡类，DPLL* 被证明终止。此外，规则嵌套模式的类是第一个允许迭代嵌套的可判定类，即允许模式的形式/n =1.。n（/ \j =1.. n.）。
2010-01-24 cs.AI cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
The Finite Model Property of Quasi-transitive Modal Logic
建立了准传递模态逻辑$\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$的有限模型性质。这种模态逻辑被保守地扩展到时态逻辑$\mathsf{Kt}_2^3$。本文提出了一个求解$\mathsf{Kt}_2^3$的Gentzen微积分$\mathsf{G}$。该演算$\mathsf{G}$通过有限的句法结构而具有有限代数性质。因此，$\mathsf{Kt}_2^3$和$\mathsf{K}_2^3$具有有限模型性质。
2019-02-22 cs.LO
A Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文提出SCFO(ID)演算，用于处理非单调归纳定义，通过稳定语义验证其理论性质，支持对一般归纳定义的定理形式化证明。
2026-09-23 cs.LO
Inputs, Outputs, and Composition in the Logic of Information Flows
信息流逻辑（LIF）是一个通用的框架，在这个框架中，过程性的任务可以以声明性的、基于逻辑的方式进行建模。本文的第一个贡献是提出了LIF表达式的输入和输出的语义和句法定义。我们研究这两者之间的关系，并表明我们的句法定义是最佳的，在某种意义上说，是精确的。第二个贡献是一个系统的研究的表达能力的序列组成的LIF。我们的结果的组合在输入和输出的结果，并与LIF的一阶逻辑（FO）和有界变量LIF有界变量FO。
2022-09-14 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
Taming Complexity in Intuitionistic Modal Logic: The Case of FIK and Its Shallow Calculus
Institute of Computer Science Czech Academy of Sciences（捷克科学院计算机科学研究所）；LIS Aix-Marseille University, CNRS（艾克斯-马赛大学CNRS LIS实验室）
针对直觉主义模态逻辑FIK，提出浅层嵌套矢列演算，通过证明切消可容许性，将判定问题复杂度降至EXPSPACE，显著低于IK的猜想非初等复杂度。
2026-07-01 cs.CC cs.LO
