Inducing syntactic cut-elimination for indexed nested sequents
本文通过建立标记相继式与索引嵌套相继式的对应关系，为索引嵌套相继式演算引入句法切割消去证明，并首次为中间逻辑构造了无切割的索引嵌套相继式演算。
2018-11-23 cs.LO
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
我们定义了PDL的无穷标号代数演算G3 PDL ^{ \infty }.然后给出了一个有限可表示的循环系统G3 PDL ^ω。我们表明，这两个是健全的和完整的PDL的标准模型，并进一步，G3 PDL ^{ \infty }是无割完全的。此外，我们还研究了证明搜索策略的循环系统的片段PDL没有测试。
2019-05-16 cs.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.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
Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics
研究了Burgess提出的优先条件逻辑PCL及其扩展.首先，一个自然语义的基础上的邻域模型，推广刘易斯的球模型的反事实逻辑，提出。直接证明了PCL及其推广的可靠性和完备性。然后介绍了该家族所有逻辑的标号微积分。该演算是模块化的，并具有标准的证明理论性质，其中最重要的是容许切割，这需要一个完整的演算的语法证明。通过采用一种通用的策略，根优先证明搜索终止，从而为PCL及其扩展提供了一个决策过程。最后，建立演算的语义完备性：从一个失败的证明尝试中的有限分支中，有可能提取出根节点的有限反模型。后一个结果给出了所有考虑的逻辑的有限模型性质的构造性证明。
2020-02-14 cs.LO
Sequent and Hypersequent Calculi for Abelian and Lukasiewicz Logics
本文给出了无限值Lukasiewicz逻辑L到Meyer和Slaney的阿贝尔逻辑A（格序阿贝尔群的逻辑）的两个嵌入。我们给出了A的新的解析证明系统，并利用嵌入导出了L的相应系统。其中包括：A和L的超代数演算以及这些演算的终止版本;复杂性co-NP的A和L的标记单代数演算; A和L的未标记单代数演算。
2002-11-18 cs.LO
Labelled calculi for quantified modal logics with definite descriptions
本文引入了具有确定描述的量化模态逻辑的标号演算。我们证明了这些演算具有G3型演算的良好结构性质。特别地，所有规则都是保高可逆的，弱化和收缩是保高容许的，割是容许的。最后，我们表明，每个演算给出了相应的模型类的有效性的证明理论表征。
2020-02-12 cs.LO math.LO
Uniform interpolation via nested sequents and hypersequents
最近开发了一个模块化证明理论框架，以证明Craig插值的正常模态逻辑的基础上推广的微积分（例如，嵌套序列、超序列和标记序列）。在本文中，我们转向一致插值，这是强于克雷格插值。给出了一种构造性的嵌套序列一致插值证明方法，并应用该方法重新证明了正规模态逻辑$\mathsf{K}$，$\mathsf{D}$和$\mathsf{T}$的一致插值性质.然后，我们使用的诀窍开发的嵌套序列应用相同的方法超序列，并获得了第一个直接证明的均匀插值$\mathsf{S5}$通过一个无割序列的演算。虽然我们的方法是证明理论的，但嵌套序列和超序列的均匀插值的定义也使用了语义概念，包括互模拟模原子命题。
2021-05-23 cs.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
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL cs.LO
A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
本文为直觉主义模态逻辑 IK 提出无标签双嵌套矢列演算，支持判定、由失败证明直接构造有限反模型，并可模拟现有嵌套与标签演算。
2025-05-13 cs.LO
Classical Transitions
我们介绍了演算的经典过渡（CT），它扩展了线性逻辑和过程之间的关系的研究线标记的过渡。从以前的工作中的关键转折是注册并行打字判断，通过概括线性逻辑判断从一个序列到许多（hypersequents）。这使我们能够弥合以前工作中用作证明项的算子结构与标准π演算（特别是并行算子和限制）之间的差距。CT的证明理论允许新的证明变换，我们显示对应于过程的标记转换系统（LTS）。我们证明了CT的学科减少和进步。
2018-03-02 cs.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
Graduate School of Information Sciences, Tohoku University（东北大学信息科学研究院）
本文研究了命题动态逻辑中非标记循环证明系统的消去问题，提出了序数演算和循环证明系统，并证明了其正确性和完备性，同时展示了消去失败及限制后的消去性质。
2026-03-02 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
Nested Sequents
我们看到如何嵌套序列，超序列的自然概括，使我们能够开发一个系统的模态逻辑证明理论。与其他突出的形式主义，如显示演算和标记序列相反，嵌套序列留在模态语言中，并允许在字面意义上享受子公式属性的证明系统。在第一部分中，我们研究了一套系统的嵌套系统的所有正常模态逻辑形成的一些组合的公理的序列性，自反性，对称性，传递性和欧几里德。我们建立健全性和完整性和他们的一些良好的性质，如可逆的所有规则，结构规则的可接受性，终止证明搜索，以及句法切割消除。在第二部分中，我们研究了常识逻辑，一种具有不动点模态的模态逻辑。我们期待在两个无穷证明系统，这种逻辑：现有的一个普通序列的基础上，没有语法切割消除程序是已知的，和一个新的嵌套序列的基础上。我们看到如何嵌套的序列，在普通的序列相比，允许句法削减消除，从而使我们能够获得一个序数上限的长度证明。
2010-04-11 cs.LO math.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
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
Unravelling Cyclic First-Order Arithmetic
本文提出将 Heyting 与 Peano 算术循环证明直接嵌入纯归纳证明的方法，扩展 Springer–Dam 翻译以恢复 Das 的 CΠ_n⊆IΠ_{n+1}，并给出标号矢列演算表示。
2025-07-28 cs.LO math.LO
