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
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
证明理论语义学（Proof-theoretical Semantics，P-tS）是一种语义学范式，其中逻辑中的意义基于证明（而不是真理）。直觉命题逻辑（IPL）的P-tS的一个特殊实例是它的基扩展语义（B-eS）。这种语义由一个称为支持的关系给出，解释逻辑常数的含义，它由称为基础的规则系统参数化，提供原子命题的语义。在本文中，我们解释的基础上收集的明确的公式，并使用统一的证明搜索-逻辑编程（LP）的证明理论的基础-提供后者的操作视图-建立完整的IPL的B-eS。这种观点允许否定，P-tS中的一个微妙的问题，被理解为在LP中的否定失败协议。具体地说，虽然对命题的否定在传统上被理解为对命题否定的断言，但在B-eS中，我们可以将对命题的否定理解为未能找到对命题的证明，这样，断言和否定都是P-tS中的基本概念。
2023-03-28 cs.LO math.LO
The model checking problem for intuitionistic propositional logic with one variable is AC1-complete
我们证明了单变量直觉命题逻辑的模型检验问题对于对数空间一致AC 1是完备的。作为基本工具，我们使用直觉主义逻辑和海廷代数之间的联系，并探讨其复杂性的理论方面。对于单变量超直觉逻辑，我们得到了模型检验问题的NC 1-完全性。
2011-09-15 cs.CC cs.LO
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
Epistemic extensions of combined classical and intuitionistic propositional logic
逻辑$L$是由Lewitzka [7]引入的，作为一个结合了直觉主义和经典逻辑的模态系统：$L$是CPC的保守扩展，它通过嵌入$φ\mapsto\squareφ$包含IPC的副本。在这篇文章中，我们考虑$L3$，即$L$增广与S3模态公理，定义基本的认知扩展和证明完全性w.r.t.代数语义学由此产生的逻辑结合了经典知识和信仰与直觉真理。阿特莫夫和普罗波佩斯库[1]所研究的直觉主义认识逻辑的一些认识规律反映在经典模态原理中。特别是，“直觉真理$\Rightarrow$知识$\Rightarrow$经典真理”的影响是由我们的逻辑$EL3$的定理$\squareφ\rightarrow Kφ$和$Kφ\rightarrowφ$表示的，在这里我们处理的是经典而不是直觉知识。最后，我们表明，修改我们的语义产生代数模型的直觉主义认知逻辑系统介绍了[1]。
2017-02-27 cs.LO
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
借助一个紧凑的Prolog为基础的定理证明直觉命题逻辑，我们合成的最小假设下，一个给定的公式公式成为一个定理。应用我们的合成算法，以涵盖基本的溯因推理机制后，我们合成的字面量，模仿行的真值表在经典或中间逻辑和我们的条件假设，把经典或中间逻辑的定理，在直觉逻辑。更进一步，我们推广我们的溯因推理机制，合成更有表现力的前置条件，使用最小的一组规范公式，在微积分中的任意公式可以减少，同时保持其可证明性。组织作为一个独立的文学Prolog程序，本文支持其内容的交互式探索，并确保我们的结果完全可复制。
2022-05-11 cs.LO
Fixed-point elimination in the intuitionistic propositional calculus
这是现有文献的一个结果，最小和最大的单调多项式的不动点Heyting代数，即直觉命题演算的代数模型总是存在的，即使这些代数是不完整的格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉逻辑的$μ$ -演算是平凡的，每个$μ$ -公式等价于一个不动点自由公式。本文给出了公式的最小不动点和最大不动点的公理化，以及计算等价于给定$μ$ -公式的无不动点公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每个单调公式都通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。我们从算法中提取出这样的n的上界，这取决于公式的大小。对于某些公式，我们证明了这些上界是多项式的和最优的。
2016-01-04 cs.LO math.CT math.LO
An analytic calculus for intuitionistic belief
直觉主义信念已经被阿特莫夫（Artemov）和普罗托波佩斯库（Protopescu）公理化为直觉主义命题逻辑的扩展，通过分配方案K和共反射$A\rightarrow\Box A$。通过这种方式，信念被解释为验证的结果，并且它适合于具有认知模态的直觉主义命题逻辑的扩展的Brouwer-Heyting-Kolmogorov解释。本文研究了直觉信念的自然演绎系统$\mathsf{IEL}^{-}$的结构性质。重点讨论了微积分的解析性，首先证明了正规化定理和子公式性质。从这些，逻辑的可判定性和一致性遵循作为推论。最后，用纯证明论的方法建立了析取性质、$\Box$ -素性和反射规则的可容许性。
2021-06-27 cs.LO math.LO
Verified completeness in Henkin-style for intuitionistic propositional logic
本文在Lean定理证明器中形式化并验证了Troelstra和van Dalen提出的直觉主义命题逻辑Henkin式完备性证明，是该方法下首个经机械验证的同类成果，源码已开源。
2023-10-03 cs.LO
Negational Fragment of Intuitionistic Control Logic
研究直觉控制逻辑一元纯否定片段的性质。该逻辑是在直觉命题逻辑（IPL）的基础上，通过增加新的伪和常数扩展IPL语言而产生的。有两个不同的假常数可以定义两种形式的否定。我们分析了负一元公式之间的蕴涵关系，并给出了ICL这一片断的非等价公式的偏序集。
2014-08-09 cs.LO math.LO
Uniform interpolation with constructive diamond
University of Amsterdam（阿姆斯特丹大学）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
本文通过构造性方法证明构造性K（CK）和Wijesekera的K（WK）具有均匀插值性质，填补了直觉主义模态逻辑中独立box和diamond算子均匀插值研究的空白。
2026-05-27 cs.LO math.LO
Propositional Logics of Dependence
本文在命题层次上研究依赖逻辑。我们证明了几个有趣的命题依赖逻辑，包括命题依赖逻辑，命题直觉依赖逻辑以及命题查询逻辑，是表达完备的，并且具有析取或合取范式.我们提供了演绎系统，并证明了这些逻辑的完备性定理。
2016-03-07 cs.LO math.LO
Semantic Incompleteness of Hilbert System for a Combination of Classical and Intuitionistic Propositional Logic
本文证明del Cerro和Herzig提出的希尔伯特系统(C+J)−因缺少经典肯定前件规则而在语义上不完备，并利用Priest的悖论逻辑给出论证。
2023-12-26 cs.LO
Ruitenburg's Theorem via Duality and Bounded Bisimulations
对于给定的直觉命题公式A和出现在其中的命题变元x，定义公式{A\_i}的无穷序列|i $\ge$ 1}，设A1为A，A1 + 1为A（A1/x）。Ruitenburg定理[8]指出序列{Ai}（模逻辑等价）最终是周期为2的周期性的，即存在N个$\ge$ 0使得A N +2 $\leftrightarrow$ A N在直觉命题演算中是可证明的。我们给出了这个定理的语义证明，使用对偶技术和有界互模拟行列。
2018-04-17 cs.LO math.LO
A note on undecidability of propositional non-associative linear logics
本文介绍了一种非结合、非交换的命题直觉线性逻辑，称为命题非结合非交换直觉线性逻辑（NACILL）。我们证明了NACILL和它的任何扩展的交换和/或压缩规则是不可判定的。此外，我们介绍了两种类型的经典版本的NACILL，即，NACILL的对合版本和NACILL的循环和对合版本。我们证明这两个逻辑也是不可判定的。
2019-09-30 cs.LO
Formula Transformers and Combinatorial Test Generators for Propositional Intuitionistic Theorem Provers
我们开发组合测试生成算法，逐步更强大的定理证明，涵盖公式语言，从直觉逻辑的隐含片段，以充分的直觉命题逻辑。我们的算法支持穷举和随机生成这些逻辑公式。为了提供已知可证明的公式，通过Curry-Howard公式作为类型的对应，我们使用生成器来生成可类型化的lambda项和组合子表达式。除了发电机的几个类的公式，我们设计的算法，限制公式生成的规范代表之间的equiprovable公式，并引入程序转换，减少公式等价公式的一个更简单的结构。同样的转换，当反向应用时，会创建更难的公式，可以捕获合理性或不完整性错误。为了测试测试框架本身的有效性，我们描述了用于导出这些逻辑中的几个的轻量级定理证明器和用于在已知定理证明器中查找错误的用例。我们的Prolog实现可在：https://github.com/ptarau/TypesAndProofs和公式生成器和定理证明器的子集，在Python中实现可在：https://github.com/ptarau/PythonProvers。保留字：术语和公式生成算法，基于Prolog的定理证明器，公式作为类型，类型推断和类型栖息，组合测试，发现定理证明器中的错误。
2019-10-04 cs.LO
Cut-free Deductive System for Continuous Intuitionistic Logic
本文提出了一种无割推理论系统，用于连续直觉逻辑，通过代数方法证明了其完备性和割可接受性。
2026-02-05 cs.LO math.LO
Simple example of weak modal logic based on intuitionistic core
在本文中，我们提出了一个简单的命题逻辑的例子，它有一个模态算子，是基于直觉的核心。这个系统在模态意义上是非常弱的-例如规则性或单调性不成立。它具有完备的语义，由具有邻域和预序关系的可能世界构成。我们讨论了对这些结构施加的某些限制。此外，我们提出的特征公理4已知的逻辑S4。
2018-06-25 cs.LO math.LO
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
本文提出共诱导证明搜索方法，扩展至偏极直觉逻辑LJP，并通过解释将该方法应用于其他直觉逻辑系统，实现了解的可判定性继承。
2025-12-04 cs.LO math.LO
From Intuitionism to Many-Valued Logics through Kripke Models
直觉命题逻辑是由Kurt Gödel（1932）证明的无限多值逻辑，它是由Stanismartaw Jaumkowski（1936）证明的可数多值逻辑。在本文中，我们使用Saul Kripke（1959）的模型为这些定理提供了另一种证明。哥德尔的证明产生了一个中间命题逻辑（介于直觉主义和经典之间），现在被称为哥德尔或哥德尔-达米特逻辑，也被模糊逻辑学家研究。我们还提供了一些结果，在此逻辑命题连接词的可定义性。
2020-08-20 cs.LO math.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Modality Definition Synthesis for Epistemic Intuitionistic Logic via a Theorem Prover
我们推导出一个Prolog定理证明器的直觉主义认知逻辑开始，我们扩展与操作符定义提供嵌入在直觉主义命题逻辑（{ \bf IPC}）的微积分{ \bf G4 IP}。借助一个候选定义公式生成器，我们发现的公理和定理的阿特莫夫和Protopescu的{ \em直觉主义认知逻辑}（{ \bf IEL}）持有和预期的非定理公式失败的认知运营商。我们比较了嵌入{ \bf IEL}在{ \bf IPC}与同样发现成功嵌入Dosen的双重否定模态，判断不足以作为一个认识算子。最后，我们讨论了失败的{ \em必要性规则}，否则成功的{ \bf S4}嵌入和分享我们的想法的直觉解释这些差异的背景下，Brouwer-Heyting-Kolmogorov语义的直觉推理和知识获取的认识和alethic模态。保留字：认知直觉逻辑，命题直觉逻辑，基于Prolog的定理证明器，逻辑系统的自动综合，定义公式生成算法，模态逻辑嵌入直觉逻辑。
2019-09-14 cs.LO
There are (other) ways to negate in propositional team semantics
本文研究命题团队语义中的否定机制，证明完全直觉主义否定不增加向下封闭逻辑的公理化复杂度，并证明同时含依赖原子与包含原子的命题逻辑具有表达完备性。
2024-10-10 cs.LO math.LO
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
IBM Research -- Tokyo（IBM研究院（东京））；Kyoto University（京都大学）
受深度神经网络（DNN）在机器学习中的最新发展的启发，我们探索了它们在PL相关主题中的应用。本文是实现这一目标的第一步;我们提出了一种无否定命题逻辑的证明合成方法，其中我们使用DNN来获得证明搜索的指南。这个想法是把证明综合问题看作是从命题到其证明的转换。我们训练seq 2seq，这是神经机器翻译中的一个流行网络，因此它生成一个编码为给定命题的$λ$ -项的证明。我们实现了整个框架，并根据经验观察到，生成的证明项在AST的树编辑距离方面接近于正确的证明。这一观察结果证明了使用经过训练的seq 2seq模型的输出作为证据搜索的指导是合理的。
2017-06-20 cs.AI cs.LO cs.PL
Intuitionistic modal logics: epistemic reasoning with distributed knowledge
本文向直觉主义信念与认知逻辑的参数化语言中添加菱形算子，并证明了所得的带分布式知识的逻辑关于其关系语义的完备性。
2025-09-16 cs.LO
Modal meet-implication logic
本文扩展命题直觉主义逻辑的 meet-implication 片段，引入保持 meet 的模态，基于半格给出语义并建立对偶性，获得完备性，识别共同模态片段，并证明其为 dialgebraic 逻辑，进而获得某处可表达性。
2022-07-13 cs.LO math.LO
Proof complexity of intuitionistic implicational formulas
本文在直觉命题逻辑（IPC）证明复杂性的背景下研究蕴涵公式。一方面，我们给出了一个有效的重言式到蕴涵重言式的转换，该转换保持了直觉扩展Frege（EF）或替换Frege（SF）证明的多项式长度。另一方面，在IPC的蕴涵片段中的EF证明多项式地模拟了蕴涵重言式的完全直觉主义逻辑。在一定条件下，这些结果也适用于其他超直觉逻辑的其他片段。特别地，Hrubeeland \cite{hru:lbint}的直觉EF证明的长度的指数下界，由Jeanábek \cite{ej:sfef}推广到无界分支的超直觉逻辑中EF和SF系统之间的指数分离，可以通过蕴涵重言式实现。
2016-09-18 cs.LO math.LO
Propositional Logics Complexity and the Sub-Formula Property
1979年，理查德·斯塔曼（Richard Statman）利用证明论证明了直觉主义逻辑的纯蕴涵部分（M-蕴涵）是PSPACE-完备的。他展示了从完整的直觉主义命题逻辑到其蕴涵片段的多项式有界翻译。通过Ladner证明的S4的PSPACE-完备性，以及从S4到直觉逻辑的Goedel变换，得出了M-隐含的PSPACE-完备性。逻辑L的演绎系统的子公式原理指出，只要F1，...，Fk证明了A，有一个证明，其中每个公式的出现要么是A的子公式，要么是Fi的某个子公式。在这项工作中，我们扩展了Statman的结果，并表明，任何命题（可能模态）结构逻辑满足一个特定的配方的子公式原则是在PSPACE。如果逻辑包含最小纯蕴涵逻辑，那么它是PSPACE-完全的。因此，EXPTIME完全命题逻辑，如PDL和至少有2个主体的常识认知逻辑满足这个特定的子公式原则，当且仅当PSPACE=EXPTIME。我们还展示了如何我们的技术可以用来证明，任何多值逻辑有它的重言式集在PSPACE。
2015-04-10 cs.LO
Intuitionistic Non-Normal Modal Logics: A general framework
我们定义了一类直觉非正规模态逻辑，它们可以被看作是经典模态逻辑的直觉对应物。我们首先考虑单峰逻辑，它只包含必然性和可能性之间的一个。然后，我们考虑更重要的情况下，双峰逻辑，其中包含两个模态算子。在这种情况下，我们定义了几个必要性和可能性之间的相互作用，尽管比对偶性弱。对于所有的逻辑，我们提供了一个希尔伯特公理化和一个切自由的代数演算，在此基础上，我们还证明了它们的可判定性。然后，我们给我们的逻辑在邻域模型的语义特征。我们的语义框架捕获模块化不仅我们的系统，但也已经知道的直觉非正常模态逻辑，如建设性K（CK）和Wijesekera的建设性并发动态逻辑的命题片段。
2019-01-28 cs.LO math.LO
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
Preferred Networks, Inc.（首选网络公司）
自动定理证明（ATP）中的问题求解可以被解释为证明者逐步构造证明树的搜索问题。本文提出了一种用于直觉命题逻辑中证明搜索的深度强化学习算法。将深度学习应用于ATP的最大挑战是缺乏大型公共定理数据库。然而，我们通过在强化学习的每次迭代中应用新的数据增强过程来克服这个问题。我们还提高了算法的效率，通过一种新的紧凑图表示公式的语法结构。使用大量的扩充数据，我们训练高度精确的图神经网络，其近似公式的语法结构的集合的价值函数。我们的方法在计算时间方面也具有成本效益。我们将展示我们的证明器优于Coq的$\texttt{tauto}$策略，这是一种基于人类工程学的证明器。在指定的时间限制内，我们的证明器解决了基准库中84%的定理，而$\texttt{tauto}$只能解决52%。
2018-11-02 cs.AI cs.LG cs.LO
On an ecumenical natural deduction with stoup -- Part I: The propositional case
由Gentzen提出并由Prawitz进一步研究的自然演绎系统是最著名的证明理论框架之一。它的成功部分是基于这样一个事实，即自然演绎规则呈现了逻辑常数的简单表征，特别是在直觉主义逻辑的情况下。然而，为了处理经典逻辑而对直觉规则集进行扩展的做法受到了很多批评。事实上，大多数这样的扩展都在通常的引入和消除规则之外增加了管理否定的额外规则。因此，几个元逻辑属性，最突出的一个是和谐，失去了。Dag Prawitz提出了一个自然演绎的普世体系，其中经典逻辑和直觉主义逻辑被编入同一个体系。在这个系统中，古典主义逻辑学家和直觉主义逻辑学家将共享全称量词、合取词、否定词和荒谬的常量，但他们各自有自己的存在量词、析取词和蕴涵词，具有不同的含义。Prawitz的主要观点是，这些不同的含义是由一个双方都能接受的语义框架给出的。在本文中，我们提出了一种不同的方法适应，自然演绎框架，吉拉德的stoup机制。这将允许定义一个纯粹的和谐自然演绎系统的命题片段普拉维茨的普世逻辑。
2022-04-06 cs.LO
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
本文研究了命题直觉主义逻辑、一阶非常数论域直觉主义逻辑和一阶常数论域直觉主义逻辑的标号演算和套演算之间的关系。它示出，拟合的嵌套结石自然产生于其相应的标记结石-为上述每一个逻辑-通过消除标记派生的结构规则。这两种类型的系统之间的平移对应关系被用来表明嵌套演算从其相关的标记演算中继承了证明理论属性，例如规则的完整性，可逆性和切割容许性。由于标记的演算很容易通过逻辑的语义，本文提出的方法可以被看作是一个，从而细化版本的标记演算（包含嵌套的演算片段）具有良好的性能直接从逻辑的语义。
2021-04-19 cs.LO math.LO
Phase Semantic Cut-elimination for Intuitionistic Linear Logic with Least and Greatest Fixed Points
Graduate School of Humanities and Human Sciences Hokkaido University（北海道大学人文科学研究院）；School of Computer Science University of Sheffield（谢菲尔德大学计算机学院）；Faculty of Humanities and Human Sciences Hokkaido University（北海道大学人文科学部）
研究具有最小和最大不动点的直觉主义命题乘加线性逻辑（$\mu$IMALL）的消去切割定理，通过定义相位语义，证明其可靠性与无切割完全性，改进前人论证方法来达成该定理的证明。
2026-07-23 cs.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
The ILLTP Library for Intuitionistic Linear Logic
使用标准化问题集对自动定理证明（ATP）系统进行基准测试是一种用于测量其性能的成熟方法。然而，这种库的非经典逻辑的可用性是非常有限的。在这项工作中，我们提出了一个库基准吉拉德的（命题）直觉线性逻辑。为了快速引导问题的集合，并讨论相关问题的选择和理解它们作为线性逻辑定理的意义，我们使用Kleene直觉定理集合在传统专著“元数学导论”中的翻译。我们分析了四种不同的翻译直觉逻辑线性逻辑和比较他们的证明使用线性逻辑为基础的证明与聚焦。为了增强我们库中的问题集，我们将这三个保持可靠性的翻译应用于ILTP库中的命题基准。最后，我们产生了一个全面的可达性问题的Petri网和编码等问题的线性逻辑序列，从而扩大了我们的问题集。
2019-04-15 cs.LO
Intuitionistic Common Knowledge
Peking University（北京大学）
本文研究了直觉逻辑中的共同知识逻辑变种ICK，扩展了直觉命题逻辑IPL，引入多层知识算子和共同知识算子，并通过birelational Kripke模型分析其语义，证明了逻辑的完备性、有限模型性质和可判定性。
2026-05-01 cs.LO math.LO
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
University of California San Diego（加利福尼亚大学圣迭戈分校）；Carnegie Mellon University（卡内基梅隆大学）
本文提出 TrialMaster，通过构建 Lean 形式化的直觉主义命题逻辑试错数据集，让模型从失败搜索路径中学习，从而在推理时以更少尝试解决更多未见定理。
2024-07-29 cs.AI cs.LO
Decision Problems for Propositional Non-associative Linear Logic and Extensions
在我们以前的工作中，我们提出了从完全非结合Lambek演算通过添加一种线性逻辑模态获得的逻辑。我们称这种逻辑为非关联非交换直觉线性逻辑（简称$\mathbf{NACILL}$）。在本文中，我们建立了可判定性和不可判定性结果的各种扩展的$\mathbf{NACILL}$。关于可判定性的结果，我们证明了$\mathbf{NACILL}$的几个推广的演绎问题与左弱化规则是可判定的。关于不可判定性结果，我们证明了非结合非交换经典线性逻辑的所有扩张的压缩和交换规则的可证明性问题是不可判定的。
2020-03-03 cs.LO math.LO
New Proofs of Weak Normalization for Propositional Logic
Chennai Mathematical Institute（钦奈数学研究所）
本文提出直觉主义自然演绎弱规范化的新证明，仅处理割，提供局部规则选择收缩或归约子证明，并在Lean中形式化，给出确定性算法。
2026-10-01 cs.LO
Uniform Lyndon interpolation for intuitionistic monotone modal logic
本文证明了直觉单调模态逻辑$\mathsf{iM}$具有一致Lyndon插值性质性质（ULIP）.逻辑$\mathsf{iM}$是一种基于直觉的非正规模态逻辑，而ULIP属性是插值的加强，其中插值只依赖于蕴涵的前提或结论，并尊重命题变元的极性。我们的方法来证明ULIP产生明确的一致插值，并利用了一个终止的微积分$\mathsf{iM}$，我们已经为此目的开发。据我们所知，$\mathsf{iM}$具有ULIP和一个终止的逻辑演算的结果是第一个直觉非正规模态逻辑的结果。然而，而不是证明这些特定的结果，我们的目的是显示的建设性证明理论方法，我们用来证明ULIP的灵活性。它在过去几年中得到了发展，并已被应用于子结构，中间，经典（非）正规模态和直觉正规模态逻辑。根据这些结果，直觉非正规模态逻辑似乎是一个自然的下一类尝试应用该方法，我们在这方面迈出了第一步。
2022-08-09 cs.LO math.LO
Intuitionistic Dynamic Logic
University of Bern（伯尔尼大学）；Ghent University（根特大学）
研究直觉主义动态逻辑的数学理论，涵盖五种该逻辑。通过开发证明论工具、进行语义研究，建立相关性质与界限。主要贡献为开发演算、获有限模型性质及可判定性、给出直觉主义线性时态逻辑完备公理系统。
2026-07-16 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
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
2025-07-09 cs.LO math.LO
Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)
证明演算是一种类型化的证明演算，它利用证明和反驳概念之间的对偶性为经典命题逻辑提供计算解释。在这项工作中，我们将扩展Euda-Euda，以包括经典的二阶逻辑，通过将参数多态性和存在类型。该系统具有良好的计算性能，如类型保持，汇合，和强规范化，这是建立在通过reductionalargument。我们确定了一个句法限制的证明，其特点正是直观的片段的二阶dupda-dupta，我们研究规范的结果。
2022-10-13 cs.LO
Higher-order Kripke models for intuitionistic and non-classical modal logics
University College London（伦敦大学学院）
本文提出推广标准Kripke模型的高阶Kripke模型，通过非经典命题模型间的可达关系定义非经典模态语义，验证其可适配直觉主义模态逻辑IK与新逻辑MK，给出通用结构定义及相关性质猜想。
2025-11-19 cs.LO
Combining First-Order Classical and Intuitionistic Logic
本文从证明论的角度研究了Humberstone（1979）和del Cerro and Herzig（1996）研究的直觉主义和经典命题逻辑组合C+J的一阶展开。C+J同时具有经典蕴涵和直觉蕴涵，而我们的一阶扩展在C+ J中增加了经典和直觉全称量词以及一个存在量词.本文为我们的一阶直觉逻辑和经典逻辑的结合提供了一个多后继的代数演算G（FOC+J）.我们的正则演算G（FOC+J）将直觉蕴涵和直觉全称量词的正确规则的上下文限制在特定形式的公式中。为了保证子公式的性质，建立了割消定理。作为推论，G（FOC+J）在一阶直觉逻辑和经典逻辑上都是保守的。通过一个典范模型论证证明了G（FOC+J）的强完备性.
2022-04-14 cs.LO
A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems
本文提出了一种基于算法的方法来证明命题系统的归纳性质，如可容许性，可逆性，割消和单位扩展。虽然一般来说是不可判定的，但这些结构属性在证明理论中是至关重要的，因为它们可以减少证明搜索工作，并进一步用作获得其他元结果（如一致性）的脚手架。算法-利用重写逻辑元逻辑框架，并使用重写和缩小为基础的推理-详细解释，并说明整个文件的例子。他们已经完全机械化的L-框架，从而提供了一个正式的规约语言和现成的机械化的证明搜索算法来证明定理和元定理的目标系统的半决策程序。本文通过实例分析说明，L-框架在单结论和多结论直觉逻辑、经典逻辑、经典线性逻辑及其二元系统、直觉线性逻辑和正规模态逻辑等命题推理系统上的应用，实现了很大程度的自动化。
2021-01-08 cs.LO math.LO
Classical and Intuitionistic Subexponential Logics are Equally Expressive
经典逻辑的直觉限制被标准地看作是增加了逻辑的表达性，因为经典逻辑可以通过双重否定在直觉逻辑中得到充分的表示，而另一个方向没有真值保持的命题编码。在这里，我们表明，次指数逻辑，这是一个家庭的子结构的经典逻辑，每个参数在一个前序的次指数连接词的改进，不遭受这种不对称性，如果前序是系统修改的编码的一部分。准确地说，我们显示了合成（即，聚焦的）对给定编码取模的部分双导数。我们的编码特定的次指数前序的特殊情况下，产生了已知的和新的充分性定理的子结构逻辑。
2010-06-16 cs.LO
A translation of Maehara's "Eine Darstellung der Intuitionistischen Logik in der Klassischen"
本文翻译了Maehara 1954年关于直觉主义逻辑嵌入经典模态逻辑的论文，该工作独立于Gödel，使用证明论方法扩展了嵌入到一阶直觉主义模态逻辑。
2026-09-24 cs.LO math.LO
Proof-theoretic Semantics for First-order Logic
本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明，并同时给出一阶直觉主义逻辑的可靠性与完备性证明。
2025-07-17 cs.LO math.LO
Defining Logical Systems via Algebraic Constraints on Proofs
本文提出利用约束代数将非经典逻辑证明系统分解为更简单逻辑（如经典逻辑）的证明系统，实现统一模块化的证明理论处理，并搭建语义与证明理论的桥梁。
2023-10-19 cs.LO math.LO
A General Glivenko-Gödel Theorem for Nuclei
格利文科定理说，在命题逻辑中，一个公式的经典可证明性包含了该公式的双重否定的直觉可证明性。我们概括Glivenko的定理从双重否定到任意核，从可证明性在微积分归纳产生的抽象后果关系，并从命题逻辑的任何一组对象。由此产生的守恒定理带有精确的有效性标准，这使我们能够立即包括Gödel的Glivenko定理的一阶谓词逻辑的对应物。开核给出了正逻辑的演绎定理的一种形式，而闭核则提示了从直觉逻辑到最小逻辑的还原的一种变体，这种还原可以追溯到约翰松。
2021-12-28 cs.LO
Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic
Université de Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所、洛林信息研究实验室）；Universidad Nacional de Quilmes（基尔梅斯国立大学）；Universidad de la República, Facultad de Ingeniería, IMERL（共和国大学、工程学院、数学与计算研究与应用中心）
本文提出了一种在直觉逻辑中统一建模并行性与代数效应的框架，无需单子或双积，通过引入两种lambda演算及新的集合论解释实现。
2025-09-18 cs.LO math.CT
