Separability and harmony in ecumenical systems
几十年来，寻求平滑地组合逻辑，使经典逻辑和直觉逻辑的连接词可以和平共存，一直是一个迷人的研究课题。在2015年，Dag Prawitz提出了一个普世一阶逻辑的自然演绎系统。我们开始这项工作，提出了一个{ \em纯}的微积分版本，在这个意义上，连接词的介绍，而不使用其他连接词。为了做到这一点，我们扩展了序列与额外的上下文，stoup，并定义了极性的普世概念。最后，我们顺利地扩展这些想法处理模态，提出纯标记和嵌套系统的普世模态逻辑。
2022-04-05 cs.LO
On Nested Sequents for Constructive Modal Logics
我们提出了各种模态逻辑的演绎系统，这些模态逻辑可以通过添加公理d，t，b，4和5的组合从正常模态逻辑CK的构造性变体中获得。这包括标准模态逻辑K4、S4和S5的构造变体。我们使用我们的演示形式主义的嵌套序列，并给出一个句法证明削减消除。
2015-09-02 cs.LO
Automating proof search when equality is a logical connective
Inria & LIX, Institut Polytechnique Paris（法国国家信息与自动化研究所与巴黎理工学院LIX实验室）
本文提出了一种扩展unification以处理量词交替和正负出现方程的证明搜索程序，为第一顺序sequent calculus提供了支持等价性作为逻辑连接词的轻量级逻辑框架。
2026-05-19 cs.LO
Conditionals and Modalities in Constructive Quantum Logics
TU Wien（维也纳工业大学）；Chapman University（查普曼大学）
研究推广直觉主义逻辑和量子逻辑的逻辑系统，提出iEx-逻辑作为直觉主义逻辑与带有Sasaki钩的orthomodular逻辑的交集，并刻画其扩展格。
2026-07-01 cs.LO math.LO
Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant
Section Theory of Computer Science, Informatics Institute（计算机科学理论系，信息学研究所）；Faculty of Science, University of Amsterdam（阿姆斯特丹大学理学院）
本文研究了在左到右评估假设下，哪些逻辑定律可以公理化短路求值，探讨了非交换性和交换性变体逻辑的差异及特性。
2018-10-04 cs.LO
Canonical calculi with (n,k)-ary quantifiers
2001年由Avron和Lev提出的命题规范Gentzen型系统，除了标准公理和结构规则外，只有逻辑规则，其中只有一个连接词被引入，而没有其他连接词被提及。定义了这类系统的非平凡性的构造性凝聚准则，并证明了这类系统允许割消当且仅当它是凝聚的。这种系统的语义是使用二值非确定性矩阵（2N矩阵）。在2005年，Zamansky和Avron将这些结果扩展到了一元量词的严格形式。在本文中，我们大大扩展的典型系统的特征（n，k）-ary量词，绑定k个不同的变量和连接n个公式，并表明，一致性标准仍然是建设性的，这样的系统。然后，我们讨论了k {0，1}的情形，证明了当正则演算G具有强特征2N矩阵时，G是相干的，这就等价于允许强割消.
2008-08-07 cs.LO
LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics
Technical University of Košice（科希策理工大学）
介绍LogicProof这一用于教育的交互式网络定理证明器，支持经典和构造性逻辑的自然演绎与相继式演算，经学生测试能提升对形式证明构建的理解，补充现有教学方法。
2026-07-07 cs.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
A constructive proof of Skolem theorem for constructive logic
本文针对构造逻辑，证明了一阶构造性自然演绎中矢列可证时引入新函数符号可构成保守扩展，从而给出 Skolem 定理的构造性证明。
2023-05-17 cs.LO
Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP
Institute for Logic, Language and Computation (ILLC) University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；Arché Research Centre University of St Andrews（圣安德鲁斯大学Arché研究中心）
本文通过案例研究将推理-行为语义（I-bS）扩展至三维相继式演算，构建K3与LP的I-bS并验证其联结词意义的保守性，为I-bS与MUltlog整合以实现多值逻辑I-bS生成的自动化奠定基础。
2026-08-05 cs.LO math.LO
A logical basis for constructive systems
这项工作致力于可计算性逻辑（CoL）-哲学/数学平台和长期项目，用于在其底层语义中用可计算性取代真理之后重新开发经典逻辑（见http：//www.cis.upenn.edu/paggiorgi/cl.html）。本文阐述了CoL框架的一些基本复杂性理论。然后证明了演绎系统CL 12关于CoL语义的可靠性和完备性，包括后者基于多项式时间可计算性而不是原则上可计算性的版本。CL 12是一个微积分系统，其中一个变量的含义直观上可以被描述为“后继变量可以在算法上还原为先行变量”，并且其中公式是由谓词字母、函数字母、变量、常数、恒等式、否定式、平行和选择连接词以及盲量词和选择量词构建的。一个案例是CL 12是一个足够的逻辑基础建设性的应用理论，包括复杂性导向的。
2011-03-14 cs.CC cs.LO 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
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
On noncommutative extensions of linear logic
本文受语义学启发定义半交换乘法线性逻辑，扩展两个非交换连接词，并引入装饰相继式演算，证明其无切割、可靠且完全，从而为 Pomset 逻辑提供了相继式演算表述。
2019-09-19 cs.LO math.LO
It ain't necessarily so: Basic sequent systems for negative modalities
我们期待在非经典的否定和相应的调整连接词从模态的观点，在完整的分配格，并应用一个非常一般的机制，以提供足够的分析证明系统的逻辑是基于它们。在通常的模态语义学中定义非经典否定自动地允许人们将等价公式视为同义的，并且对对位规则的全局版本有一个自然的理由。从这个角度来看，我们的研究提供了一个特别有用的环境中，消极模态和他们的同伴可以用来处理不一致和不确定性。在研究了基于任意框架的模态逻辑之后，我们将结果推广到了序列框架、自反框架、函数框架和对称框架。在每一种情况下，我们也调查何时以及如何经典否定可能从而被定义。
2016-06-23 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
Paraconsistent Constructive Modal Logic
该研究提出构造模态逻辑CK的次协调对应逻辑族，基于带双赋值的直觉主义框架定义语义，提供希尔伯特式公理化与模块化无切割矢列演算，用于形式化矛盾但非平凡命题态度的推理并证明可判定性。
2025-08-25 cs.LO
Sequent systems for negative modalities
非经典的否定可能在不止一个方面不能成为矛盾形成算子，而且它们经常也不能尊重基本的元逻辑性质，如替换性质。这样的缺点是由复杂的语义和证明系统，其哲学解释和计算属性被发现想要的见证。在本文中，我们调查全等非经典否定，生活在非常自然的系统中的正常模态逻辑在完全分配格，这些逻辑进一步丰富的调整连接词，可用于处理推理下不确定性所造成的不一致性或不确定性。使用这样简单的语义，我们研究的框架类的特征在于序列性，自反性，功能性，对称性，传递性，以及它们的一些组合，并讨论它们揭示了什么关于否定的亚经典属性。对于这样描述的逻辑，我们应用了一种一般机制，这种机制允许人们赋予它们分析的普通系统，其中大多数甚至是无切的。我们还研究了允许经典否定在我们的逻辑中明确定义的确切情况。
2017-07-25 cs.LO
A Proof-Theoretic View of Basic Intuitionistic Conditional Logic (Extended Version)
本文从证明论角度研究基本直觉主义条件逻辑，为IntCK引入嵌套演算、为CCKbox引入矢列演算，并在此基础上定义带might算子的保守扩张CCK，给出其模型类、公理化及若干扩张结果。
2025-07-03 cs.LO
Infinitary Classical Logic: Recursive Equations and Interactive Semantics
在本文中，我们提出了一个经典逻辑的无限扩展派生的交互语义。我们语言的公式可能是由命题变量和逻辑连接词标记的无限树。我们表明，在我们的设置每个递归公式方程有一个唯一的解决方案。至于导子，我们使用Tait演算的无穷变体来导出序列。我们在本文中介绍的派生的交互式语义被表示为测试<< T >>（派生候选者，Proponent）和环境<< not S >>（否定对象，Opponent）之间的辩论（交互树）。我们证明了一个推导的完备性定理，我们称之为交互完备性定理：<< T >>（测试）和<< not S >>（环境）之间的交互不会产生错误（即，Proponent wins）以防<< T >>来自< >的句法派生< S >。
2014-09-11 cs.LO
Realisability semantics of abstract focussing, formalised
我们提出了一个抽象的焦点，配备了证明条款的微积分：在传统的Zeilberger的工作，逻辑连接词和它们的介绍规则是作为一个参数的系统，它崩溃的同步和异步阶段的焦点作为宏观规则。我们进一步离开作为一个参数的操作，扩展了一个新的假设的背景下，这使我们能够捕捉经典和直观的聚焦微积分。然后，我们定义的可实现性语义（的证明）的系统，蒙奇-Maccagnoni的正交模型的基础上，经典的集中式微积分，但现在在更高的抽象层次上操作上述。在这个层次上，我们证明了一个引理，即如果一个项是A型的，那么在模型中它的外延是在A的（集合论）解释中。这表明了这样一个事实：取集合的正交时所涉及的全称量化在语义中反映了Zeilberger在异步阶段宏观规则中的全称量化。系统及其语义都在Coq中形式化。
2015-11-13 cs.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO math.LO
Non-commutative linear logic fragments with sub-context-free complexity
University of Illinois Springfield（伊利诺伊大学斯普林菲尔德分校）；RIKEN Center for Advanced Intelligence Project (AIP)（理化学研究所先进智能项目中心）
本文提出了Lambek演算片段对REG、LCFL和CFL类的新的描述复杂性刻画，首次将Lambek演算片段与证明复杂性REG和LCFL等同，并基于直接转换与结构归纳展示了最弱变体的CFL复杂性，确立了Cut消解定理在比较形式文法与矢列演算中的效用。
2025-11-04 cs.CC cs.FL cs.LO
A substructural logic for quantum measurements
本文构建了一种交换与弱化规则受限的矢列式子结构逻辑，通过基于正交关系并推广 Hilbert 投影的语义刻画量子测量序列，得到可靠完备且证明论优雅的量子测量逻辑。
2023-07-18 cs.LO math.LO quant-ph
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
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
A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)
本文基于序贯演算而非自然演绎定义基扩展语义，利用多重结论序贯演算构建适合经典语义的框架，支持 Sandqvist 式完备性证明，并探讨了原子切割规则对语义的影响。
2025-07-13 cs.LO math.LO
Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information
我们考虑一个简单的模态逻辑，其非模态部分有合取和析取作为连接词，其模态是伴随对，但不是一般的闭包算子。尽管没有否定和蕴涵，也没有与（例如）的特征公理相对应的公理，T，S4和S5，这样的逻辑是有用的，如Baltag，Coecke和第一作者在以前的工作中所示，用于编码和推理多智能体系统中的信息和错误信息。对于这样一个逻辑，我们提出了一个代数语义，使用格与代理索引的家庭的伴随对运营商，和一个免费的切演算。演算利用操作符的序列，在风格的“嵌套”或“树”演算;切容许性是由建设性的句法方法。逻辑的适用性说明了推理的泥泞的儿童难题，其中演算增加了额外的规则来表达事实的泥泞的儿童场景。
2009-03-23 cs.LO cs.MA
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
Projection-algebras and quantum logic
该研究提出作为布尔代数非交换非结合推广的P-代数，刻画其代数结构与性质，建立了对应可靠完备的受限交换子结构量子逻辑，明确了其与希尔伯特空间闭子空间的关联。
2024-08-15 cs.LO math.LO quant-ph
ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
School of Information Science, Beijing Language and Culture University（北京语言文化大学信息科学学院）
提出ZX-演算，通过迹索引类型、预层非单调语义和构造性AGM信念修正，保守扩展Martin-Löf依赖类型论，并给出Coq机械化证明。
2026-06-02 cs.CL cs.LO
