Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
任何一组真值函数连接词都有微积分规则，这些规则可以从连接词的真假值表中系统地生成。这样一个逻辑演算产生了一个多结论的自然演绎系统和帕里戈自由演绎的一个版本。排除规则是“一般性的”，但可以系统地简化。削减消除和正常化保持不变。限制到一个单一的公式，在随后产生这些系统的直观版本。这些规则还产生了广义lambda演算，为Curry-Howard同构中的自然演绎证明提供了证明条件。添加一个间接证明规则产生经典的单结论版本的这些系统。根岑的标准系统是作为特例出现的。
2021-05-31 math.LO
Multi-type Sequent Calculi
显示演算是广义的递归演算，它享有一种“规范”的切割消除策略。也就是说，它们的割消是通过验证元定理的假设一致获得的，并且通过添加或删除结构规则来保持。在本文中，我们讨论了一个证明理论的设置，灵感都贝尔纳普的显示逻辑和Sambin的基本逻辑，概括这些演算在两个方向：明确允许不同的类型，并通过削弱所谓的显示和可见性属性。推广到多类型的环境使得有可能引入特定的工具，提高表现力，这已被证明是有用的，例如，一个顺利的证明理论治疗的多模态和动态逻辑。概括到一个设置，其中充分显示属性是不需要的，使得有可能考虑到逻辑承认连接既不是伴随也不是残差，或逻辑是不封闭的统一替代。在本文中，我们给出了一个一般性的概述，我们称之为多型演算，我们讨论了它们的典型削减消除元定理。
2016-09-17 math.LO
Modularisation of Sequent Calculi for Normal and Non-normal Modalities
在这项工作中，我们探讨之间的连接（线性）嵌套的微积分和普通的微积分正常和非正常模态逻辑。通过提出本地版本的普通的正则化规则，我们得到线性嵌套正则化演算的一些逻辑，包括我们所知的第一个嵌套正则化演算的一个大类的简单依赖的多模态逻辑，和许多标准的非正常模态逻辑。由此产生的系统是模块化的，并有单独的左，右介绍规则的方式，这使得他们服从规范的双极条款。虽然这种颗粒的的证明搜索规则引入了更多的选择，我们展示了如何线性嵌套的证明演算可以限制到阻塞的推导，直接对应于普通的证明推导。
2017-11-16 cs.LO math.LO
Sequent calculi for first-order ST
Università di Cagliari（卡利亚里大学）；Universitat de Barcelona（巴塞罗那大学）
本文提出两种一阶ST的sequent演算，旨在恢复其与局部元推理有效性之间的完整对应关系。
2026-02-27 math.LO
Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics
本文通过提出PTIME翻译和严格标签证明概念，建立了时态逻辑解析展示演算与标签相继式演算之间的多项式等价关系，证明标签形式体系包含并扩展了展示形式体系。
2024-06-28 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
Labelled calculi for the logics of rough concepts
本文针对非分配正规模态逻辑 L 及其扩张，利用丰富化形式背景的一阶原子公式作标签，构建可靠完备的加标矢列演算，并扩展得到粗糙形式背景逻辑的证明系统。
2024-01-18 math.LO
Cut-free sequent calculi for the provability logic D
本文为介于可证性逻辑GL和S之间的非正规模态逻辑D建立了两个无切矢列演算并证明了切消定理，同时引入了新的希尔伯特型系统，并推广了基于极限序列的模型定义及一般公理化结果。
2025-01-14 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
Labelled calculi for lattice-based modal logics
本文为基本正规非分配模态逻辑L及其31个公理化扩张提出了带标签矢列演算，并证明了其可靠性、完备性、保守性、切割消去与子公式性质，展示了为LE-逻辑类系统引入带标签演算的统一方法。
2024-01-18 math.LO
Labelled calculi for quantified modal logics with definite descriptions
本文引入了具有确定描述的量化模态逻辑的标号演算。我们证明了这些演算具有G3型演算的良好结构性质。特别地，所有规则都是保高可逆的，弱化和收缩是保高容许的，割是容许的。最后，我们表明，每个演算给出了相应的模型类的有效性的证明理论表征。
2020-02-12 cs.LO math.LO
Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization
University of Calabria（卡拉布里亚大学）
该研究基于经典命题逻辑的块演算与无切矢列式演算的对应关系，构建了G0T、G3T矢列式演算及NgT自然演绎系统，证明了系统等价性、切消定理与NgT的完全正规化定理。
2026-08-24 math.LO
Proof Theory for Bimodal Provability Logics
University of Bern（伯尔尼大学）
本文首次为双模可证逻辑设计非标记的序列表演算，涵盖CS、CSM和ER逻辑，并通过非非Wellfounded版本建立切消过程，证明了这些逻辑具有统一的Lyndon插值性质。
2026-05-14 math.LO
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
本文探讨了基于序列的证明形式化方法的层级结构，分析了内部与外部演算的区别及其翻译难度。
2025-05-07 cs.LO math.LO
Admissibility of the Structural Rules in the Sequent Calculus with Equality
本研究基于结构规则可容许性一般定理，分析带等词的G3[mic]矢列演算扩展系统，证明无函数符号语言下Fitting语义表列方法可同时施加严格性与等词替换定向性，并探讨相关推广及Orevkov性质的适用性。
2024-03-11 math.LO
Inception Display Calculi
IMDEA Software Institute（IMDEA软件研究所）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；Department of Mathematics and Applied Mathematics, U. of Johannesburg（约翰内斯堡大学数学与应用数学系）
本文提出了一种扩展的显现演算框架，用于涵盖更广泛的逻辑系统，包括非分析归纳公理的公理扩展，并通过统一对应理论和ALBA算法生成分析规则。
2026-05-16 math.LO
Unified Correspondence and Proof Theory for Strict Implication
分配格扩展逻辑（DLE-逻辑）的统一对应理论是严格蕴涵逻辑的专门理论。作为一般语义守恒性结果的结果，广泛的严格蕴涵逻辑可以保守地扩展到有界分配全非结合Lambek演算（BDFNL）上的Lambek演算。许多严格的蕴涵序列可以转化为分析规则，采用统一对应理论的主要工具之一，即（适当修改的版本）基于阿克曼引理的算法$\msf{ALBA}$。给出了BDFNL的Gentzen型无割演算及其推广，并给出了由严格蕴涵序列转化而来的解析规则。
2016-04-29 math.LO
Grafting Hypersequents onto Nested Sequents
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
2015-08-10 cs.LO math.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
Resource control and strong normalisation
我们介绍了\emph{resource control cube}，一个系统，由八个直观的lambda演算与资源的隐式或显式控制，无论是自然演绎或自然演算。本文介绍了Kesner和Renaud提出的与自然演绎对应的四种立方体演算，以及与λ演算对应的四种立方体演算。该演示文稿是参数化的一组资源（削弱或收缩），这使得一个统一的治疗的八个结石的立方体。简单类型的资源控制立方体一方面将Curry-Howard对应扩展为具有隐式或显式结构规则的直觉自然演绎和直觉推理逻辑，另一方面又与子结构逻辑相关。我们提出了一个通用的交叉型系统的资源控制立方体演算。我们的主要贡献是一个强大的归一化减少在这个立方体的特征。首先，我们证明了可类型性意味着强规范化的“自然演绎基地”的立方体，通过适应reductionmethod。然后，我们证明了可类型性意味着强规范化的“cubes基地”的立方体，通过使用一个组合良好的订单和一个合适的嵌入在“自然演绎基地”。最后，我们证明了强规范化意味着在立方体中使用头部主题扩展的可键入性。所有的证明都是通用的，并且可以通过实例化资源集来针对立方体的每个演算。
2013-05-17 cs.LO math.LO
Arithmetical proofs of strong normalization results for symmetric lambda calculi
给出了两个对称$λ$ -演算对应于经典逻辑的强正规化的算术证明。第一个是由Curien和Herbelin提出的$\barλμ\tildeμ$ -演算。它通过Curry-Howard对应从Gentzen的经典可编程演算LK导出，以便在“程序”和“上下文”之间以及在“按名称调用”和“按值调用”之间具有对称性。第二种是对称的$λμ$ -演算。它是Parigot引入的$λμ$ -演算，其中加入了约简规则$μ'$，它是$μ$的对称。这些结果是已知的，但是以前的证明使用了约简的候选者，其中类型的解释被定义为某些增算子的不动点，因此是高度非算术的。
2009-05-06 math.LO
Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Wrocław（弗罗茨瓦夫大学）
本文证明存在规则的 chase 与 Gentzen 一阶逻辑矢列演算扩展中的证明搜索本质等价，并能生成知识库通用模型，从而形式化连接证明论与知识表示中的可判定性工具。
2023-06-05 cs.AI cs.DB cs.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Proof Theory for Positive Logic with Weak Negation
对Johansson逻辑的子系统，通过用弱否定扩充直觉主义逻辑的正片段，发展了证明论方法。这些方法被用来建立逻辑系统的属性。特别是，无切完全的微积分的引入和使用提供了一个事实，即系统满足克雷格插值性质的证明。演算的替代版本稍后通过适当的循环检查历史机制获得。证明了新演算的可终止性，并由此得出所考虑的逻辑系统是PSPACE完全的结论。
2019-07-11 math.LO
Sequent-Type Proof Systems for Three-Valued Default Logic
序列型证明系统构成了一类重要且广泛使用的演算，非常适合于分析证明搜索。在我的硕士论文中，我介绍了一种缺省逻辑的变体的序列型演算，它采用\Lukasiewicz的三值逻辑作为底层的基本逻辑。这个版本的默认逻辑是由Radzikowska提出的，解决了标准默认逻辑的一些代表性缺陷。更具体地说，在我的论文中讨论的演算公理化勇敢和怀疑的推理，这个版本的默认逻辑，分别以下的非单调推理的上下文中首次介绍的Bonatti和Olivetti，采用互补演算公理化无效的公式，照顾表达的一致性条件的默认。
2019-05-12 cs.LO math.LO
Inference-Behaviour Semantics for All$^\ast$ Connectives in Two-Dimensional Sequent Calculi
Institute for Logic, Language and Computation, University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；Arché Research Centre, University of St Andrews（圣安德鲁斯大学Arché研究中心）
研究二维相继式演算中连接词语义，基于推理行为语义方法，通过应用于10816个连接词规则对，找到21个连接词语义子句，描绘其语义关系，发现直觉主义否定、析取和蕴涵各捕捉经典对应物一半意义。
2026-07-23 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
Proof Theory for Intuitionistic Strong Löb Logic
本文介绍了两种直觉强Löb逻辑的终结演算${\sf iSL}_\Box$：一种是基于直觉命题逻辑${\sf IPC}$的终结演算${\sf G4ip}$的终结演算${\sf G4iSL}_\Box$，另一种是标准无割演算${\sf G3ip}$的无结构规则的扩展${\sf G3iSL}_\Box$.主要结果之一是${\sf G3iSL}_\Box$的割消定理的句法证明。此外，还建立了${\sf iSL}_\Box$的微积分与Hilbert系统之间的等价关系.从文献中可知，${\sf iSL}_\Box$对于一类直觉模态Kripke模型是完备的，其中模态关系是传递的，相反是良基的，并且是直觉关系的子集.在这里，这一事实的建设性证明是通过使用一个反模型的基础上的一个变种的${\sf G4iSL}_\Box$建设。因此，该文件包含两个证明削减消除，语义和句法证明。
2023-03-06 math.LO
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
在本文中，我们介绍了一个一般家庭的序列式演算的模态语言及其片段，以捕捉所有建设性的可接受的系统的本质。称这些演算为\emph{constructive}，我们表明，任何足够强的建设性的微积分，满足一个温和的技术条件，可行地承认所有的Visser规则，即，有一种多项式时间算法，它读取维塞尔规则的前提的证明，并为其结论提供证明。作为一个积极的应用，我们证明了Visser规则在直觉模态逻辑的几个演算中的可行容许性，这些演算包括$\mathsf{CK}$，$\mathsf{IK}$及其由模态公理$T$，$B$，$4$，$5$，有界宽度和深度的模态公理以及命题逻辑的扩展。在消极的一面，我们表明，如果一个足够强大的直觉模态逻辑（满足一个温和的技术条件）不承认至少一个Visser的规则，那么它不能有一个建设性的逻辑演算。因此，除了$\mathsf{IPC}$之外，没有中间逻辑具有构造性的构造演算。
2022-10-16 cs.LO math.LO
Hypersequent Calculi Have Ackermannian Complexity
Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Bernoulli Institute, University of Groningen（格罗宁根大学伯努利研究所）
研究显示，超序列演算在扩展可交换全拉姆贝克算术时，其证明复杂度可被限制在阿克曼层级，而非超阿克曼层级。
2026-02-22 cs.CC 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 Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
本研究提出一种基于无切割嵌套序列演算的纯句法方法，证明含逆模态的经典时态逻辑及其扩展、双直觉主义逻辑的Craig插值性质，创新引入定义插值元对偶的正交性条件，无需语义或嵌入辅助。
2023-06-14 cs.LO math.LO
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
2014-11-05 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-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
Lambek-Grishin Calculus: Focusing, Display and Full Polarization
\emph{Focused sequent calculi}是一种改进的证明演算，其中关于推理规则的适用性的附加副条件强制实现证明搜索策略。聚焦无割证明给出了一种特殊的范式，用于定义微积分证明的恒等式。通过对\emph{multi-type calculi}理论及其代数语义的\emph{heterogenous consequence relations}推广，提出了一种新的Lambek-Grishin逻辑的聚焦显示演算fD.LG和全极化代数语义FP.LG.微积分fD.LG有\emph{strong focalization}，它是\emph{sound and complete} w.r.t.这个完备性结果在某种意义上比标准极化代数语义的完备性更强（例如参见Bastenhof对于Lambek-Grishin逻辑的相位语义或Hamano和Takemura对于线性逻辑的相位语义），因为我们不需要在同一公式上连续应用移位的证明上做商。我们计划调查之间的连接，如果有的话，这个完整性的结果和概念的\emph{full completeness}介绍Abramsky等人。我们还显示了一些额外的结果。fD.LG是健全和完整的w.r.t. LG-代数：这相当于所谓的\emph{completeness of focusing}的语义证明，假定用于Lambek-Grishin逻辑的标准（显示）微积…
2020-11-05 cs.LO math.LO
Uniform Interpolation in provability logics
本文利用模态可证逻辑GL和Grz的解析演算和终止演算，用证明理论的方法证明了这两类逻辑的一致内插定理. Gödel-Löb的逻辑GL的演算是标准循环演算的一个变体，在Grzegorczyk的逻辑Grz的情况下，演算实现了一个显式的循环防止机制，灵感来自Heuerding的工作。
2022-11-04 math.LO
A logic for default deontic reasoning
本文提出了一种基于默认逻辑的非模态证明论框架，用于解决规范冲突和动态规范问题。
2025-12-21 cs.LO math.LO
Unsound Inferences Make Proofs Shorter
我们给出的例子演算，延长根岑的微积分LK不健全的量词推理，这样的方式，（一）推导只导致真正的序列，（二）证明在其中是非elementarily短于LK证明。
2019-05-06 cs.LO math.LO
A minimal classical sequent calculus free of structural rules
Gentzen的经典微积分LK有明确的收缩和弱化的结构规则。它们可以被吸收（在右侧公式中），通过将公理P，（不是P）替换为Gamma，P，（不是P），对于任何上下文Gamma，并将原始析取规则替换为Gamma，A，B意味着Gamma，（A或B）。本文提出了一个经典的公理演算，它也是免费的收缩和削弱，但更对称：收缩和削弱都吸收到合取，保持公理规则完整。它使用混合合取规则，结合了标准的上下文共享和上下文拆分规则：Gamma，Delta，A和Gamma，Sigma，B意味着Gamma，Delta，Sigma，（A和B）。我们将这个系统M称为最小相继式演算。我们证明了一个极小定理的命题片段Mp：任何命题微积分S（在一个标准类的右侧演算）是完整的，当且仅当S包含Mp（即，每一个规则的Mp是可导的S）。因此，我们可以把M看作是根岑的LK的最小的完整核心。
2010-02-11 math.LO
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
Université Paris Cité（巴黎西岱大学）；CNRS（法国国家科学研究中心）；IRIF（信息与随机研究所）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
将 Pitts 的均匀插值证明论技术扩展到直觉主义多后承设定，为直觉主义模态逻辑 KM 设计终止的多后承相继演算并构造均匀插值，同时证明 KM-代数类的连贯性。
2026-05-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 Perspective on Base-Extension Semantics (Technical Report)
本文基于序贯演算而非自然演绎定义基扩展语义，利用多重结论序贯演算构建适合经典语义的框架，支持 Sandqvist 式完备性证明，并探讨了原子切割规则对语义的影响。
2025-07-13 cs.LO math.LO
On the Unity of Logic: a Sequential, Unpolarized Approach
目前的工作旨在通过标准的顺序，非极化游戏的逻辑统一。具体地说，我们的愿景是，必须有数学上精确的线性精化和直觉限制逻辑的概念，使经典逻辑（CL）的线性精化与（经典）线性逻辑（LL）相一致，其直觉限制与直觉主义逻辑（IL）到直觉主义LL（ILL）的线性精化相一致。然而，与名称相矛盾的是，由于其并发性和极化性，LL至少从游戏语义的角度来看不能是CL的线性细化。事实上，现有的游戏语义LL采用并发，这是相当异国情调的游戏语义的ILL，IL或CL。此外，LL中的线性否定在ILL、IL或CL（的游戏语义）中永远不为真。为了寻找CL的真正线性加细，我们从LL的双边加细演算中分割出线性逻辑否定（$LL^-$）的加细演算，并引入了一个新的分布公理$! ? A \vdash ? ! A$（用于将CL的序列$Δ\vdash Γ$转换为$LL^-$的序列$! Δ\vdash ? Γ$）。然后我们给出了$LL^-$的范畴语义，为此我们引入了为什么不是单子？，双到众所周知的当然comonad！，给出CL到$LL^-$的范畴翻译$Δ\rightarrow Γ= ? (Δ\multimap Γ) \cong ! Δ\multimap ? Γ$，它是IL到ILL的标准翻译$Δ\rightarrow Γ= ! Δ\multimap Γ$的Kleisli扩展。此外，我们实例化的范畴语义完全完成（顺序，非极化）的游戏语义的…
2019-12-16 cs.LO math.CT math.LO
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.LO
On Three-Valued Dependence-Like Logics
University of Lodz（罗兹大学）
本文探讨依赖逻辑与三值逻辑的关联，提出两种结合经典联结词与传染性联结词的三值依赖类逻辑，并给出相应的可靠完备无切割二叉相继式演算。
2026-10-07 cs.LO math.LO
Sequent-style tableaux for first-order logic: structural analysis, cut admissibility, and the correspondence with LK
University of Calabria（卡拉布里亚大学）
本文在一阶逻辑语境下，基于Smullyan的块演算，确立其结构性质与切消，证明其与Gentzen LK的对应关系，为sequent式tableaux提供了系统的结构分析。
2026-07-31 math.LO
Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
本文提出半解析矢列演算的通用框架，证明足够强的多模态子结构逻辑若具有此类演算则必满足 Craig 插值性质，并据此统一证明多类逻辑的 CIP，同时形式化证实几乎所有常见逻辑都缺乏“好的”矢列演算。
2024-09-03 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
Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Institute of Artificial Intelligence, Technische Universität Dresden（德累斯顿工业大学人工智能研究所）
本文提出基于矢列系统的构造性方法，首次证明高表达力描述逻辑RIQ具有基于概念的Beth可定义性，并可从证明中计算插值式以提取隐式概念的显式定义。
2024-10-18 cs.AI cs.DB 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 Grammar Logics via Structural Refinement
Institute of Artificial Intelligence, Technische Universität Dresden（德累斯顿工业大学人工智能研究所）
本文通过结构细化方法，为直觉语法学逻辑构建了无割嵌套序列表演系统，并证明了其保守性、不可判定性和可判定子类。
2025-12-03 cs.DM cs.LO math.LO
Intuitionistic Dynamic Logic
University of Bern（伯尔尼大学）；Ghent University（根特大学）
研究直觉主义动态逻辑的数学理论，涵盖五种该逻辑。通过开发证明论工具、进行语义研究，建立相关性质与界限。主要贡献为开发演算、获有限模型性质及可判定性、给出直觉主义线性时态逻辑完备公理系统。
2026-07-16 cs.LO math.LO
