Sequent Calculi for Semi-De Morgan and De Morgan Algebras
给出了半De Morgan代数的无压缩无割的代数演算$\msf{G3SDM}$和De Morgan代数的无结构规则的单后继代数演算$\msf{G3DM}$.截规则在两种结石中均成立。这两种演算都具有可判定性和Craig插值。利用该演算证明了一些嵌入定理：$\msf{G3DM}$通过Gödel-Gentzen变换嵌入到$\msf{G3SDM}$中. $\msf{G3DM}$嵌入到经典命题逻辑的微积分中。将$\msf{G3SDM}$嵌入到直觉命题逻辑的微积分$\msf{G3ip}$中。
2016-11-16 math.LO
A sequent calculus demonstration of Herbrand's theorem
赫布兰德定理通常被认为是根岑在经典微积分中的Hauptstern定理的一个推论。然而，Middle定理仅对前束范式公式直接给出Herbrand定理。在手册的证明论，巴斯声称要证明的充分声明的定理，使用微积分的方法来显示完整性的演算的Herbrand证明，但我们证明有一个缺陷的证明。本文给出了Herbrand定理的完全一般性的正确证明，作为LK的全割消元定理的推论。主要的困难是要表明，如果有一个Herbrand证明的前提下，一个压缩规则，有一个Herbrand证明其结论。我们通过证明一个深度压缩规则的可容许性来解决这个问题。
2010-07-20 math.LO
Epsilon Calculus Provides Shorter Cut-Free Proofs
本文证明一阶语言中epsilon格式矢列演算的无切割推导相比通常矢列演算的无切割证明具有非初等加速优势。
2024-01-17 math.LO
A Cut-Free Sequent Calculus for Defeasible Erotetic Inferences
近年来，形式化性爱推理的努力-即，对问题的推论和从问题中的推论-已经成为那些从事色情逻辑工作的人关注的中心问题。然而，很少有人试图为这些推论制定一个证明论。为了填补这一空白，我们构建了一个演算（类）的序列，是健全的和完整的两种研究推理的色情逻辑（IEL）：色情唤起和色情的影响。虽然已经作出努力，公理化前者在一个系统中，目前没有证明论为后者。此外，现存的公理化的色情唤起未能捕捉其可废止的字符，并提供任何规则，引入或消除问题形成的运营商。相比之下，我们的演算编码序列的可撤销性条件，并提供了规则的引进和消除的色情公式。我们证明了一个消除定理的版本的截规则，适用于声明和erotetic公式，并在IEL的问题唤起的公理化帐户的规则在我们的系统中是允许的。
2018-11-16 math.LO
A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)
本文为包含分裂析取与探究析取的基础命题团队逻辑引入了一种深度推理矢列演算，证明了其保高度弱化、切消除等性质，并导出了新的Lyndon插值定理。
2025-08-10 math.LO
Proof nets for the Lambek calculus with one division and a negative-polarity modality for weakening
在本文中，我们介绍了一个变种的Lambek演算允许空的前件。这个变体使用两个连接词：左分裂和一元模态，只在负极性时出现，并允许弱化后继词的先行词。我们定义了这个演算的证明网的概念，这是类似于普通的Lambek演算和乘法线性逻辑。我们证明了一个图在所考虑的演算中是可导的当且仅当它存在一个证明网，从而我们建立了一个基于图的可导性准则.图的大小由图的长度限定。
2019-12-08 math.LO
Cut--free sequent calculus and natural deduction for the tetravalent modal logic
{ \em四价模态逻辑}（$\cal TML$）是Font和Rius（\cite{FR2}）定义的两种逻辑之一（另一种是{ \em正常四价模态逻辑} ${\cal TML}^N$），与蒙泰罗的四价模态代数有关。这些逻辑是众所周知的{ \em-邓恩的四值逻辑}的扩展，它结合了多值字符（四价）与模态字符。事实上，$\cal TML$是关于四价模态代数保持真度的逻辑。正如丰特和里乌斯所观察到的，逻辑$\cal TML$和代数之间的联系不如${\cal TML}^N$那么好，但是作为补偿，它具有更好的证明理论行为，因为它具有强充分的根岑演算（参见\cite{FR2}）。本文证明了Font和Rius给出的非线性微积分不具有割消性质。然后，利用Avron，Ben-Naim和Konikowska提出的一般方法（\cite{Avron02}），我们给出了具有割消性质的$\cal TML$的一个代数演算.最后，受后者的启发，我们提出了一个{ \em自然演绎}系统，相对于四价模态逻辑是可靠的和完备的。
2021-01-24 math.LO
Undefinability of Standard sequent calculi for Paraconsistent three-valued logics
本文研究一类三值次协调逻辑的演绎性质。我们定义了一个标准微积分的概念，并证明了这些逻辑没有健全的和完整的标准微积分。此外，我们还利用三边序列为次协调弱Kleene逻辑提供了非标准的可靠的、完全的和无割的代数演算。
2017-09-28 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
Sequent calculi for first-order ST
Università di Cagliari（卡利亚里大学）；Universitat de Barcelona（巴塞罗那大学）
本文提出两种一阶ST的sequent演算，旨在恢复其与局部元推理有效性之间的完整对应关系。
2026-02-27 math.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 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 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
A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)
本文基于序贯演算而非自然演绎定义基扩展语义，利用多重结论序贯演算构建适合经典语义的框架，支持 Sandqvist 式完备性证明，并探讨了原子切割规则对语义的影响。
2025-07-13 cs.LO math.LO
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
2014-11-05 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
Integrating a Global Induction Mechanism into a Sequent Calculus
数学中大多数有趣的证明都包含一个归纳论证，这需要扩展LK-演算来形式化。最常用的演算归纳包含一个单独的规则或公理，减少了有效的证明理论性质的演算。据我们所知，没有这样的演算允许割消法成为具有子公式性质的标准形式，即证明中出现的每个公式都是最终公式的子公式。证明图式是LK-证明的变体，能够通过将证明链接在一起来模拟归纳。存在一个模式范式，它与具有子公式性质的范式具有可比的证明理论行为。然而，一个演算的证明图式的建设并不存在。在本文中，我们介绍了一个演算证明图式和证明的可靠性和完整性方面的一个片段的归纳论点形式化的皮亚诺算术。
2017-05-12 cs.LO math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
Propositional Calculus in Coq
我正式的经典命题逻辑在证明辅助Coq的重要定理。主要证明了（1）自然演绎演算的可靠性和完备性，（2）自然演绎演算与Hilbert系统和Hilbert演算的等价性，（3）Hilbert演算的割消元。
2015-03-31 cs.LO math.LO
Admissibility of the Structural Rules in the Sequent Calculus with Equality
本研究基于结构规则可容许性一般定理，分析带等词的G3[mic]矢列演算扩展系统，证明无函数符号语言下Fitting语义表列方法可同时施加严格性与等词替换定向性，并探讨相关推广及Orevkov性质的适用性。
2024-03-11 math.LO
Uniform Interpolation in provability logics
本文利用模态可证逻辑GL和Grz的解析演算和终止演算，用证明理论的方法证明了这两类逻辑的一致内插定理. Gödel-Löb的逻辑GL的演算是标准循环演算的一个变体，在Grzegorczyk的逻辑Grz的情况下，演算实现了一个显式的循环防止机制，灵感来自Heuerding的工作。
2022-11-04 math.LO
Canonical Proof nets for Classical Logic
证明网为模规则排列的证明提供了抽象的对应物;其思想是，如果两个证明具有相同的底层证明网，则它们本质上是相同的证明。因此，提供一个令人信服的证明网络对应于经典的微积分证明是理解经典微积分证明的重要一步。通过令人信服，我们的意思是：（a）应该有一个典范函数从证明网络的证明，（b）应该有可能检查网络的正确性在多项式时间，（c）每个正确的网络应该是可获得的从一个微积分证明，（d）应该有一个削减消除程序，保持正确性。以前的尝试给证明网类对象的命题经典逻辑已经失败了至少一个上述条件。在[23]中，作者给出了满足（a）和（b）的证明网（扩展网）的演算;文章定义了与扩展网对应的证明演算，但没有给出（c）的显式证明。该演算称为LK \ast，是一种新的具有加法和乘法析取规则的单边演算.本文（[23]的一个自包含的扩展版本）给出了关于LK \ast的扩展网的（c）的一个充分证明，并且另外给出了扩展网内部的一个割消元过程--这使得扩展网成为满足所有四个准则的经典逻辑的第一个证明网概念。
2012-03-19 cs.LO math.LO
Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
任何一组真值函数连接词都有微积分规则，这些规则可以从连接词的真假值表中系统地生成。这样一个逻辑演算产生了一个多结论的自然演绎系统和帕里戈自由演绎的一个版本。排除规则是“一般性的”，但可以系统地简化。削减消除和正常化保持不变。限制到一个单一的公式，在随后产生这些系统的直观版本。这些规则还产生了广义lambda演算，为Curry-Howard同构中的自然演绎证明提供了证明条件。添加一个间接证明规则产生经典的单结论版本的这些系统。根岑的标准系统是作为特例出现的。
2021-05-31 math.LO
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
Cirquent calculus in a nutshell
本文是一个简短的和非正式的介绍cirquent演算，一个新的证明系统的资源意识逻辑。因此，它是一种改进的微积分与机制，允许显式地考虑不同的表达式/资源之间共享子表达式/子资源的可能性。这是通过处理循环风格的结构来实现的，称为循环，而不是公式，序列或其他树状结构。该方法具有更大的表现力，灵活性和效率相比，更传统的证明理论的方法。
2021-08-28 cs.LO math.LO
Introduction to Cirquent Calculus and Abstract Resource Semantics
本文介绍了一种改进的微积分的方法，称为cirquent演算。而在Gentzen风格的证明树兄弟姐妹（或堂兄弟姐妹等）序列是不相交的公式序列，在圆微积分中，它们可以共享元素。明确地允许或禁止共享资源，从而将子结构逻辑的资源感知直觉带到一个更微妙的层次，cirquent演算提供了比cirquent演算更大的灵活性和功能。随着可计算性逻辑的诞生，对新的演绎工具的需求也随之而来（见http：//www.cis.upenn.edu/linggiorgi/cl.html）--这是一种语义构建的计算资源形式理论，它顽固地抵制了传统句法方法框架内的任何公理化尝试。循环微积分打破了僵局。从其规则的全部集合中去除收缩，产生了可计算性逻辑的基本片段CL 5的健全和完整的系统。另一方面，在微积分中做同样的事情，会把婴儿和洗澡水一起扔掉，导致严格较弱的仿射逻辑。可计算性逻辑的一个隐含的主张是，它是CL 5，而不是仿射逻辑，充分体现了传统上与后者相关的资源哲学。为了加强这一主张，本文进一步引入了一个抽象的资源语义，并显示了CL 5的可靠性和完整性。
2005-12-23 cs.LO math.LO
On structural proof theory of the modal logic K+ extended with infinitary derivations
本文研究模态逻辑K+在加入无穷推导后的结构证明论，提出允许非良基证明的矢列演算，并利用连续切割消去方法证明切割消去定理，同时说明K+的普通证明可视为循环无切割证明。
2023-10-16 math.LO
A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic
针对$\textsf{iK}_d$和$\textsf{iK}_{d*}$这两个动态拓扑逻辑系统，本文提出无切割的G3风格相继式演算，补充了其证明论分析，并证明了析取性质、Visser规则推广及插值性质等关键结果。
2025-02-13 cs.LO math.LO
A sequent calculus for a semi-associative law
本文提出一个通过限制Lambek乘积规则精确刻画Tamari序的矢列演算，证明其聚焦性质与相干性定理，并应用于格性质及Tutte-Chapoton公式的新证明。
2019-02-03 cs.LO math.CO math.LO
Sequent calculi for a unity of logic
我们提出了一个新的统一的逻辑，即，一个单一的微积分，体现了经典，直觉和线性逻辑。具体地说，我们定义了经典线性逻辑否定（CLL $^-$），它是一种新的逻辑，它是经典的、线性的，但摒弃了经典线性逻辑中的极性和严格的德摩根定律。然后，我们定义了非线性化和经典化的微积分，使得非线性化映射CLL $^-$（分别为）。直觉线性逻辑（ILL））到经典逻辑（CL）（分别直觉主义逻辑（IL）），和经典化地图IL（分别。ILL）至CL（分别为CLL $^-$）模保守扩张。通过这两个映射，只有ILL的保守扩张的微积分才能满足ILL，IL，CLL $^-$和CL。这一结果实现了一个简单的，高度系统化的逻辑统一，通过丢弃极性和严格的德摩根定律，其中（可以说）只有CLL，并包括统一的经典化和非线性化，其中交换。以前的方法不能满足这些要求。我们的统一也澄清了直觉性和经典性之间的二分法，以及逻辑的线性和非线性之间的二分法，它们是对称的。
2021-01-06 math.LO
Locality for Classical Logic
在本文中，我们将看到演绎系统的经典命题和谓词逻辑的演算结构。像随机系统一样，它们有一个可接受的截规则。此外，它们具有自顶向下的对称性和一些在微积分中不可用的导子的标准形式。同一性公理、切割、弱化和收缩都可以被简化为原子形式。这导致规则是局部的：它们不需要检查无限大小的表达式。
2003-01-27 math.LO
The approximate strong completeness of the hypersequent calculus $\text{GŁ}\forall$
School of Mathematical Sciences, Beihang University（北京航空航天大学数学科学学院）；Beijing Institute of Mathematical Sciences and Applications（北京国际数学研究中心）
本文通过标记表方法证明了一阶Łukasiewicz逻辑的超序贯演算 $ ext{GŁ} orall$ 的近似强完备性，并作为应用证明了Gentzen中序定理的变体和近似Herbrand定理，同时引入了新的切割规则 $( ext{s-Cut})$ 并展示了 $ ext{GŁ} orall+( ext{s-Cut})$ 的近似强完备性。
2026-07-15 math.LO
Gentzen-Mints-Zucker duality
Curry-Howard对应通常被描述为将证明（在直觉自然演绎中）与程序（在简单类型lambda演算中的术语）相关联。然而，这种叙述并不是完美的，因为割消的计算内容和lambda演算的逻辑起源。我们重新审视霍华德的工作，并解释它作为一个同构的一类证明在直观的λ演算和一类简单类型的lambda演算的条款。在我们讲述这个故事时，基本的二重性不是证明和程序之间的二重性，而是在一个共同的逻辑计算数学结构上的局部（λ演算）和全局（λ演算或自然演绎）观点之间的二重性。
2020-08-23 cs.LO math.LO
Focus-style proofs for the two-way alternation-free $μ$-calculus
本文为双向无交替模态μ-演算提出了一种循环证明系统，通过迹原子处理反向模态并利用多聚焦注释转化为基于路径的系统，证明了系统的可靠性与相对完备性。
2023-07-04 cs.LO math.LO
Problems and Consequences of Bilateral Notions of (Meta-)Derivability
Ruhr University Bochum（波鸿鲁尔大学）
本文探讨双边主义下相继式演算中两种可推导性对偶化的问题，揭示证明与反驳概念的不平衡，并提出保持双边平衡的解决方案。
2025-10-16 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
An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文为 FO(ID) 逻辑中的非单调归纳定义形式化了无限下降原理，通过扩展 LKID{\omega} 和 CLKID{\omega} 得到相继式演算 SCFO(ID)-inf 和 SCFO(ID)-cyc，并证明了可靠性、完备性、消割及与 SCFO(ID) 的关系。
2026-09-23 cs.LO math.LO
On noncommutative extensions of linear logic
本文受语义学启发定义半交换乘法线性逻辑，扩展两个非交换连接词，并引入装饰相继式演算，证明其无切割、可靠且完全，从而为 Pomset 逻辑提供了相继式演算表述。
2019-09-19 cs.LO math.LO
On the Recognizing Power of the Lambek Calculus with Brackets
每一种由带括号的Lambek演算识别的语言都是上下文无关的。这一点可以通过结合耶格尔的观察和对彭图斯用于原始兰贝克演算的方法的完全直接的改编来证明。允许有空前件的序列的微积分变体的情况稍微复杂一些，需要限制乘法单元的使用。
2018-04-15 cs.LO math.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
Provability in BI's Sequent Calculus is Decidable
本文针对束蕴涵逻辑（BI）自问世以来缺乏有效证明搜索过程的问题，通过推广根岑的可判定性论证并结合戴克霍夫缩并消除论证的关键特征，证明可将任意相继式的证明搜索空间规约为原始递归集，从而得出BI相继式演算的可证明性是可判定的，但文中存在错误导致主定理证明无效。
2024-04-12 cs.LO cs.SC 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
A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems
University of Urbino Carlo Bo（乌尔比诺卡洛博大学）
本文提出了一种无切割的序数演算LMC，用于分析并发系统中有限迹性质，通过闭包ℓ-单形的代数抽象实现逻辑系统的正确性和完备性。
2025-12-05 cs.LO math.LO
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 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
On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics
我们引入了一个非交换子结构逻辑的演算FL'。它最多有一个公式在右项，并排除了三个结构推理规则，即收缩，弱化和交换。(FL是基于我们对非交换子结构逻辑的根森式自然演绎的研究。FL'具有与标准演算FL（Full Lambek）相同的证明强度，标准演算FL是所有其他子结构逻辑的基本演算。对于标准FL，我们使用Ono的公式。虽然FL'和标准FL是等价的，但在左蕴涵规则上有细微的差别。在标准FL中，两个参数分别为$Γ_1$和$Γ_2$，其中每一个只是任意公式的有限序列，分别出现在左侧和右侧。位于左规则$\imply$（对应于FL '中的$\imply'$）左上方的左括号左侧的公式。另一方面，在FL '的$\imply'$的左侧规则中，在左上侧的箭头的左侧没有这样的参数。在FL '中，$Γ_1$始终为空，并且在$\imply'$的左侧规则中只允许出现$Γ_2$。（类似的区别也出现在乘法连词和加法连词以及加法析取中。）FL'和FL之间的这种区别关系很大，因为我们在FL'中构造了一个证明图，它表明乘法合取的结合性和乘法合取在加法析取上的分配性是如何涉及到这些证明图中的截规则的消除的。我们说明了结合性和分配性如何与FL '的证明图中的截规则的应用的不可消除性相关。
2009-02-02 math.LO
Computational interpretation of classical logic with explicit structural rules
我们提出了一个演算提供了一个Curry-Howard对应的经典逻辑中所表示的显式的结构规则，即弱化和收缩演算。这些结构规则分别引入了明确的删除和重复的条款。我们提出了一个类型系统，我们证明了类型保持下减少。详细研究了它与经典微积分之间的一种相互关系，这种关系具有隐含的结构规则。从这个分析中，我们得到强归一化性质。
2012-03-21 cs.DC cs.LO math.LO
Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation
Université Paris Cité, INRIA, CNRS, IRIF（巴黎西岱大学、法国国家信息与自动化研究所、法国国家科学研究中心、IRIF）
本文通过双向类型原理重新审视并形式化了Craig-Čubrić插值定理，扩展了其在λ演算和序贯演算中的应用。
2026-07-17 cs.LO cs.PL math.LO
Modelling Multiplicative Linear Logic via Deep Inference
本文研究乘法线性逻辑中深推理系统与标准矢列演算之间的翻译关系，提出简化翻译并证明标准建模方法对翻译保持不变，同时给出一个文献中缺失的关于 par 与 tensor 数量的可证性必要条件。
2024-04-01 cs.LO math.LO
Semi-Substructural Logics à la Lambek
本文以非结合 Lambek 演算为视角，构造了左斜幺半闭范畴与斜幺半双闭范畴的无切割矢列演算，证明其与既有演算等价、对关系模型可靠完备，并建立框架条件与结构律的对应关系。
2024-12-31 cs.LO math.LO
Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
本文提出半解析矢列演算的通用框架，证明足够强的多模态子结构逻辑若具有此类演算则必满足 Craig 插值性质，并据此统一证明多类逻辑的 CIP，同时形式化证实几乎所有常见逻辑都缺乏“好的”矢列演算。
2024-09-03 cs.LO math.LO
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL cs.LO
Unsound Inferences Make Proofs Shorter
我们给出的例子演算，延长根岑的微积分LK不健全的量词推理，这样的方式，（一）推导只导致真正的序列，（二）证明在其中是非elementarily短于LK证明。
2019-05-06 cs.LO math.LO
Deducibility in the full Lambek calculus with weakening is HAck-complete
该研究证明带弱化的完全Lambek演算的后承关系判定问题（含乘法片段）为HAck完全，通过有损通道系统可达性归约证下界，结合结构证明论与良拟序理论得上界。
2024-06-21 cs.CC cs.LO math.LO
