On an ecumenical natural deduction with stoup -- Part I: The propositional case
由Gentzen提出并由Prawitz进一步研究的自然演绎系统是最著名的证明理论框架之一。它的成功部分是基于这样一个事实，即自然演绎规则呈现了逻辑常数的简单表征，特别是在直觉主义逻辑的情况下。然而，为了处理经典逻辑而对直觉规则集进行扩展的做法受到了很多批评。事实上，大多数这样的扩展都在通常的引入和消除规则之外增加了管理否定的额外规则。因此，几个元逻辑属性，最突出的一个是和谐，失去了。Dag Prawitz提出了一个自然演绎的普世体系，其中经典逻辑和直觉主义逻辑被编入同一个体系。在这个系统中，古典主义逻辑学家和直觉主义逻辑学家将共享全称量词、合取词、否定词和荒谬的常量，但他们各自有自己的存在量词、析取词和蕴涵词，具有不同的含义。Prawitz的主要观点是，这些不同的含义是由一个双方都能接受的语义框架给出的。在本文中，我们提出了一种不同的方法适应，自然演绎框架，吉拉德的stoup机制。这将允许定义一个纯粹的和谐自然演绎系统的命题片段普拉维茨的普世逻辑。
2022-04-06 cs.LO
Normalisation and Subformula Property for a System of Classical Logic with Tarski's Rule, and a Correction
本文为采用一般引入/消去规则并含 Tarski 规则的经典逻辑系统定义极大公式与片段、给出归约过程，证明范式及子公式性质，并更正定理 2 相关错误。
2023-04-24 cs.LO math.LO
Normalisation for Negative Free Logics without and with Definite Descriptions
本文证明了带与不带限定摹状词算子的直觉主义和经典否定自由逻辑的规范化定理，通过参数限制规则解决了归约过程中高阶极大公式的引入问题，并探讨了受限子公式性质及结果的哲学意义。
2024-10-15 cs.LO math.LO
Definite Descriptions in Intuitionist Positive Free Logic
本文给出了二元量词$I$的推理规则，用于在直觉正自由逻辑中形式化含有确定描述的句子。$I$绑定一个变量并从两个公式形成一个公式。$Ix[F, G]$表示“$F$是$G$”。该系统被证明具有理想的证明理论的性质：它被证明，在它的扣除可以被带入范式。通过比较这里推荐的确定描述的形式化方法和使用术语形成算子$ι$（其中$ιxF$表示“F”）的更常用的方法，来进行讨论。
2021-08-04 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
The naturality of natural deduction (II). Some remarks on atomic polymorphism
在以前的文件（这是一个起诉），我们研究了提取的证明理论性质的自然演绎推导从他们的非谓词翻译到系统F。我们的主要思想是引入一个扩展的方程理论系统F编纂在语法层面上的一些参数模型中发现的属性。在最近的一系列论文中，提出了一种不同的方法来提取自然演绎推导的证明论性质，方法是定义通常翻译的谓词变体，将直觉命题逻辑嵌入系统F的原子片段。在本文中，我们表明，这种方法找到了一个一般的解释，在我们的方程研究的二阶自然演绎，并提供了一个明确的语义理由参数。
2021-01-04 cs.LO math.LO
Intuitionistic Propositional Logic in Lean
该研究在Lean证明助手中形式化直觉主义命题逻辑，验证其两份完备性证明，探究Kripke与代数两种语义范式的关系，还证明了大量定理及演绎规则。
2024-10-31 cs.LO
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
我们描述了一个自然演绎形式化的直觉和经典命题逻辑的伊莎贝尔/纯框架。与早期的工作相比，我们探索了使用深度嵌入方法进行逻辑建模的教学优势，在这里我们采用了逻辑框架建模。这产生了简单而自然的教学例子，我们报告了它在2020年和2021年教授我们的自动推理课程中所发挥的作用。
2022-02-08 cs.LO
Normalisation for Some Infectious Logics and Their Relatives
我们考虑某些传染性逻辑（Sfde，dSfde，K3w和PWK）和它们的几个非传染性修改，包括两个新的逻辑，重新制定以前为它们构建的自然演绎系统（或从头开始为新逻辑的情况下，这样的系统）的方式，使这些逻辑的规范化定理的证明成为可能。我们给出了这样一个证明，并建立了所讨论的逻辑的否定子公式性质。
2022-04-14 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
Gödel Logic: from Natural Deduction to Parallel Computation
命题哥德尔逻辑用线性$A\rightarrow B\ \lor\ B\rightarrow A$的非构造性原理扩展了直觉主义逻辑。我们介绍了一个Curry-Howard对应这种逻辑，并表明，一个特别简单的自然演绎演算可以用作一个类型系统。由此产生的函数式语言丰富了简单类型的λ演算与并行进程之间的同步通信机制。我们的规范化证明采用了原始的终止参数和复杂的证明转换与有意义的计算阅读。我们的结果提供了一个计算解释哥德尔逻辑作为一个逻辑的通信并行进程，从而证明了Avron的1991年猜想。
2017-06-18 cs.LO
A New Connective in Natural Deduction, and its Application to Quantum Computing
本文研究了非和谐逻辑连接词与量子计算的联系，指出其能建模量子测量中的信息擦除等现象，并引入包含sup连接词的直觉主义逻辑，证明其证明语言可作为量子编程语言的核心。
2023-03-21 cs.LO
Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic
本文建立了直觉主义非交换逻辑的自然演绎或λ演算公式的规范化--它同时涉及交换和非交换连接词。这种演算首先介绍了德格罗特，而不是经典版本的Abrusci和Ruet承认充分熵，允许为了放宽到任何suborder。我们的结果还包括，作为一个特殊的情况下，正常化的自然演绎Lambek演算的产品，这是不足为奇的，但尚未证明。对于全熵的直觉非交换逻辑，至今没有一个证明网语法;对于语言应用，与自然演绎或多或少等价的逻辑演算由于缺乏标准的Curry-Howard同构而不方便。
2014-02-03 cs.FL cs.LO
A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version
双直觉主义逻辑是直觉主义逻辑的推广，它具有一个与蕴涵有关的联结对偶。双直觉逻辑是由Rauszer作为具有代数和Kripke语义的Hilbert演算引入的。但她随后对BiInt的"无切“演算最近被Uustalu证明是失败的。我们提出了一个新的切割免费的BiInt演算，并证明它的声音和完整的Kripke语义。确保完整性是复杂的含义和它的对偶之间的相互作用，类似于未来和过去的时态逻辑模态。我们的演算处理这种相互作用，使用扩展序列传递信息的前提下的结论，使用实例化的变量在失败的派生树的叶子。我们简单的终止论证允许我们的演算用于自动演绎，尽管这不是它的主要目的。
2007-04-17 cs.LO
A simplified lower bound for implicational logic
本文针对直觉主义蕴涵逻辑，给出了一个适用于 Gordeev 与 Haeusler 的 dag 式自然演绎的简化指数证明长度下界。
2025-10-16 cs.LO math.LO
Gentzen-Mints-Zucker duality
Curry-Howard对应通常被描述为将证明（在直觉自然演绎中）与程序（在简单类型lambda演算中的术语）相关联。然而，这种叙述并不是完美的，因为割消的计算内容和lambda演算的逻辑起源。我们重新审视霍华德的工作，并解释它作为一个同构的一类证明在直观的λ演算和一类简单类型的lambda演算的条款。在我们讲述这个故事时，基本的二重性不是证明和程序之间的二重性，而是在一个共同的逻辑计算数学结构上的局部（λ演算）和全局（λ演算或自然演绎）观点之间的二重性。
2020-08-23 cs.LO math.LO
On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC
达米特逻辑LC是用达米特公理扩展的直觉主义逻辑：对于每两个陈述，第一个蕴涵第二个或第二个蕴涵第一个。本文给出了一阶和二阶Dummett逻辑的一个自然演绎和Curry-Howard对应。我们添加到λ演算的运营商表示，从编程的角度来看，一种机制，用于表示并行计算和它们之间的通信，并从逻辑的角度来看，达米特的公理。我们证明了我们的类型演算是正常化，并表明存在量化公式的证明条款减少到一个单独的条款形成一个Herbrand析取的列表。
2016-09-27 cs.LO
Normalisation for Bilateral Classical Logic with some Philosophical Remarks, and a Note on it
双边主义者认为，连接词的意义是由推理规则决定的，因为它们在具有断言和否定公式的演绎推理中使用。本文提出了两个可与Prior的tonk相媲美的双边连接词，与tonk不同的是，对于这两个连接词，有一些简化步骤来删除以这些连接词作为主要运算符引入和消除公式而产生的最大公式。将它们中的任何一个加到双边经典逻辑中都会导致不连贯的系统。解决这个问题的一个方法是把归约的结论和消去规则的大前提的公式算作最大的，并要求它们可以从演绎中移除。本文的主要部分包括双边逻辑的规范化定理的证明。最后几节讨论了哲学上的问题，即证明是否为手头的问题提供了令人满意的解决方案，并使双边主义者面临这样一个困境：双边稳定的概念与核心的双边论点格格不入。本说明纠正了论文中一个简化步骤中的错误。
2021-08-12 cs.LO math.LO
A Symmetric Lambda-Calculus Corresponding to the Negation-Free Bilateral Natural Deduction
Filinski构建了一个对称的λ演算组成的表达式和延续是对称的，和功能，具有对偶性。在他的微积分中，函数可以使用原始运算符编码为表达式和延续。也就是说，函数的对偶性不是在微积分中推导出来的，而是作为微积分的一个原理而被采用的。在本文中，我们提出了一个简单的对称的λ演算对应的否定自由自然演绎的双边证明论语义。在我们的微积分中，连续类型不是表示为公式的否定，而是表示为具有负极性的公式。函数类型在直觉逻辑和次协调逻辑中分别表示为蕴涵和非但连接词。我们的演算不仅简单，而且功能强大，因为它包括与Wadler发明的按值调用二元演算相对应的调用值演算。我们表明，表达和延续之间的相互转换是可定义的，在我们的微积分证明的对偶功能。我们还证明了每个可类型函数都有对偶类型。因此，功能的二重性来源于双边主义。
2021-01-29 cs.LO
Calculational HoTT
我们在同伦类型理论（HoTT）中发现了一种表示直觉主义逻辑（ICL）的一阶版本的方法，对于直觉主义计算逻辑），其中，代替演绎树，相应的线性计算格式被用作形式证明工具;除此之外，等式和逻辑等价比蕴涵更优越。ICL的形式主义以前曾被一位作者从Dijkstra和Scholten提出的计算逻辑的经典版本改编为直觉主义逻辑。我们在HoTT中正式定义了\textit{deductive chains}作为ICL线性格式的表示。此外，我们使用这些演绎链证明了ICL的方程式公理和规则在HoTT中具有对应的。在这样做的过程中，我们意识到HoTT中基本类型的所有归纳算子实际上都是同伦等价的，这是我们在本文中证明的事实。此外，我们提出了一个非正式的方法来寻找类型之间的规范函数。我们认为，这些结果可能会导致一个完整的重述HoTT平等和同伦等价发挥了突出的作用。有了这种方法，并通过计算方法，有效和优雅的形式证明HoTT是可能的，通过提出的正式演绎链的方式适当的格式和符号。
2019-07-30 cs.LO math.LO
Adjoint Natural Deduction (Extended Version)
本文提出伴随逻辑的自然演绎表述，明确其与相继式演算的关联，给出函数式语言形式的计算解释并证明相关计算性质，还提出了精妙的类型检查算法。
2024-02-02 cs.LO cs.PL
A system of inference based on proof search: an extended abstract
本文提出 PSF 证明搜索框架，介绍其设计与元理论，并展示其可统一规约经典、直觉主义及线性逻辑的多种证明系统。
2023-07-24 cs.LO
A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic
本文在Nelson次协调逻辑N4及其负自由变体中考察并改进了Kürbis的二元量词I，给出嵌入函数、自然演绎系统和Kripke语义，以构造性假和次协调逻辑解决Russell确定描述词解释中的悖论问题。
2024-12-31 cs.LO
Logical Inferentialism & Attacks on Classical Logic
本文探究逻辑推理主义的规范性标准，分析其对经典逻辑的挑战，并论证经典原则在意义理论框架下缺乏合法性。
2025-09-26 cs.LO
Embedding Modal Logics into Logics of Bunched Implications
Australian National University（澳大利亚国立大学）
本文给出S4嵌入BBI的全新句法证明，证明其在S4任意公理扩张下稳定，可扩展至BBI的多种语言扩张，还给出BBI演绎定理的首个完整证明。
2026-08-10 cs.LO math.LO
A new introduction rule for disjunction
本研究为直觉主义自然演绎系统新增第三条析取引入规则∨-i3，该规则可恢复强引入性质、简化终止性证明、应用于量子计算表达量子测量，还可用于归约交换切割。
2025-10-22 cs.LO
Dual-Context Calculi for Modal Logic
本文为K、T、K4、GL和S4等正规模态逻辑的必然性片段提出双上下文风格的自然演绎系统和模态lambda演算，证明其与希尔伯特系统在可证明性上等价，并给出保积函子的范畴语义。
2020-08-18 cs.LO
