Verified completeness in Henkin-style for intuitionistic propositional logic
本文在Lean定理证明器中形式化并验证了Troelstra和van Dalen提出的直觉主义命题逻辑Henkin式完备性证明，是该方法下首个经机械验证的同类成果，源码已开源。
2023-10-03 cs.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
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
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
Duality between unprovability and provability in forward proof-search for Intuitionistic Propositional Logic
逆方法是一种基于饱和度的定理证明技术;它依赖于前向证明搜索策略，可以应用于享有子公式属性的无切演算。在这里，我们应用这种方法来推导直觉命题逻辑中的目标公式G的不可证明性。为了这个目的，我们设计了一个前向演算FRJ（G）的直觉不可证明性，这是倾向于建设性地确定公式G的不可证明性，通过提供一个简洁的反模型，特别是我们证明了生成的反模型具有最小的高度。此外，我们澄清的作用，饱和的数据库获得的结果失败的证明搜索在FRJ（G），通过展示如何从这样的数据库中提取一个派生见证直观的有效性的目标。
2018-04-18 cs.LO math.LO
A modal logic amalgam of classical and intuitionistic propositional logic
由哥德尔在1932年提出并由麦肯锡和塔斯基在1948年证明的一个著名的结果是：$φ$是直觉命题逻辑IPC的一个定理当且仅当它的哥德尔翻译$φ'$是模态逻辑S4的一个定理。在本文中，我们扩展了在我们的前一篇文章（S. Lewitzka，Algebraic Semantics for a Modal Logic Close to S1，J. Logic and Comp.，doi：10.1093/logcom/exu 067），并证明了：命题公式$φ$是IPC的一个定理当且仅当$\squareφ$是L的一个定理（实际上，我们证明了：$Φ\vdash_{IPC}φ$当且仅当$\squareΦ\vdash_L\squareφ$，对于命题$Φ,φ$）.因此，映射$φ\mapsto\squareφ$是IPC到L中的嵌入，即L包含IPC的副本。此外，L是经典命题逻辑CPC的保守扩展。在这个意义上，L是CPC和IPC的混合物。证明了L是完备的。一类具有（非正规）模态算子的特殊Heyting代数。
2015-06-03 cs.LO math.LO
The intuitionistic fragment of computability logic at the propositional level
从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI 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
From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
本文针对直觉主义命题逻辑，论证其基扩展语义涵盖了一种基于消去规则的证明论有效性版本的陈述内容，既阐释了基扩展语义的运作原理，也证明了该版本证明论有效性的完备性。
2024-09-12 cs.LO math.LO
Intuitionistic modal logics: epistemic reasoning with distributed knowledge
本文向直觉主义信念与认知逻辑的参数化语言中添加菱形算子，并证明了所得的带分布式知识的逻辑关于其关系语义的完备性。
2025-09-16 cs.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
On an ecumenical natural deduction with stoup -- Part I: The propositional case
由Gentzen提出并由Prawitz进一步研究的自然演绎系统是最著名的证明理论框架之一。它的成功部分是基于这样一个事实，即自然演绎规则呈现了逻辑常数的简单表征，特别是在直觉主义逻辑的情况下。然而，为了处理经典逻辑而对直觉规则集进行扩展的做法受到了很多批评。事实上，大多数这样的扩展都在通常的引入和消除规则之外增加了管理否定的额外规则。因此，几个元逻辑属性，最突出的一个是和谐，失去了。Dag Prawitz提出了一个自然演绎的普世体系，其中经典逻辑和直觉主义逻辑被编入同一个体系。在这个系统中，古典主义逻辑学家和直觉主义逻辑学家将共享全称量词、合取词、否定词和荒谬的常量，但他们各自有自己的存在量词、析取词和蕴涵词，具有不同的含义。Prawitz的主要观点是，这些不同的含义是由一个双方都能接受的语义框架给出的。在本文中，我们提出了一种不同的方法适应，自然演绎框架，吉拉德的stoup机制。这将允许定义一个纯粹的和谐自然演绎系统的命题片段普拉维茨的普世逻辑。
2022-04-06 cs.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
The ILLTP Library for Intuitionistic Linear Logic
使用标准化问题集对自动定理证明（ATP）系统进行基准测试是一种用于测量其性能的成熟方法。然而，这种库的非经典逻辑的可用性是非常有限的。在这项工作中，我们提出了一个库基准吉拉德的（命题）直觉线性逻辑。为了快速引导问题的集合，并讨论相关问题的选择和理解它们作为线性逻辑定理的意义，我们使用Kleene直觉定理集合在传统专著“元数学导论”中的翻译。我们分析了四种不同的翻译直觉逻辑线性逻辑和比较他们的证明使用线性逻辑为基础的证明与聚焦。为了增强我们库中的问题集，我们将这三个保持可靠性的翻译应用于ILTP库中的命题基准。最后，我们产生了一个全面的可达性问题的Petri网和编码等问题的线性逻辑序列，从而扩大了我们的问题集。
2019-04-15 cs.LO
Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version)
Heyting代数（即直觉命题演算的代数模型）上的单调多项式的最小和最大不动点总是存在的，即使这些代数不是完全格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉主义逻辑的$μ$ -演算是平凡的，每个$μ$ -公式等价于一个不动点自由公式。本文给出了公式的最小不动点和最大不动点的公理化，以及计算等价于给定$μ$ -公式的不动点自由公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每一个单调公式通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。我们从算法中提取出这样的n的上界，这取决于公式的大小。对于某些公式，我们证明了这些上界是多项式的和最优的。
2018-03-05 cs.LO math.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
New Proofs of Weak Normalization for Propositional Logic
Chennai Mathematical Institute（钦奈数学研究所）
本文提出直觉主义自然演绎弱规范化的新证明，仅处理割，提供局部规则选择收缩或归约子证明，并在Lean中形式化，给出确定性算法。
2026-10-01 cs.LO
Fixed-point elimination in the intuitionistic propositional calculus
这是现有文献的一个结果，最小和最大的单调多项式的不动点Heyting代数，即直觉命题演算的代数模型总是存在的，即使这些代数是不完整的格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉逻辑的$μ$ -演算是平凡的，每个$μ$ -公式等价于一个不动点自由公式。本文给出了公式的最小不动点和最大不动点的公理化，以及计算等价于给定$μ$ -公式的无不动点公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每个单调公式都通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。我们从算法中提取出这样的n的上界，这取决于公式的大小。对于某些公式，我们证明了这些上界是多项式的和最优的。
2016-01-04 cs.LO math.CT math.LO
Isabelle/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.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
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
本文提出推广标准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
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
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
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
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
Classical and Intuitionistic Subexponential Logics are Equally Expressive
经典逻辑的直觉限制被标准地看作是增加了逻辑的表达性，因为经典逻辑可以通过双重否定在直觉逻辑中得到充分的表示，而另一个方向没有真值保持的命题编码。在这里，我们表明，次指数逻辑，这是一个家庭的子结构的经典逻辑，每个参数在一个前序的次指数连接词的改进，不遭受这种不对称性，如果前序是系统修改的编码的一部分。准确地说，我们显示了合成（即，聚焦的）对给定编码取模的部分双导数。我们的编码特定的次指数前序的特殊情况下，产生了已知的和新的充分性定理的子结构逻辑。
2010-06-16 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 General Glivenko-Gödel Theorem for Nuclei
格利文科定理说，在命题逻辑中，一个公式的经典可证明性包含了该公式的双重否定的直觉可证明性。我们概括Glivenko的定理从双重否定到任意核，从可证明性在微积分归纳产生的抽象后果关系，并从命题逻辑的任何一组对象。由此产生的守恒定理带有精确的有效性标准，这使我们能够立即包括Gödel的Glivenko定理的一阶谓词逻辑的对应物。开核给出了正逻辑的演绎定理的一种形式，而闭核则提示了从直觉逻辑到最小逻辑的还原的一种变体，这种还原可以追溯到约翰松。
2021-12-28 cs.LO
Cut-free Deductive System for Continuous Intuitionistic Logic
本文提出了一种无割推理论系统，用于连续直觉逻辑，通过代数方法证明了其完备性和割可接受性。
2026-02-05 cs.LO math.LO
Intuitionistic Justification Logic, Semantically
University of Birmingham（伯明翰大学）
本文为直觉主义辩护逻辑（含满足子项）提出两类语义模型，证明其可靠性与完全性，并通过实现定理建立与直觉主义模态逻辑的联系。
2026-07-01 cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Combining intermediate propositional logics with classical logic
在[17]中，我们介绍了一种模态逻辑，称为$L$，它结合了直觉命题逻辑$IPC$和经典命题逻辑$CPC$，并且是完全的w.r.t.代数语义学然而，对于Kripke风格的语义来说，$L$似乎太弱了。在本文中，我们增加了积极和消极的内省，并表明，由此产生的逻辑$L5$有一个Kripke语义。对于中间逻辑$I$，我们考虑$L5$的参数化版本$L5(I)$，其中$IPC$被$I$取代。$L5(I)$可以看作是$I$中关于真值推理的经典模态逻辑。从我们的研究结果，我们得出一个简单的方法来确定代数和Kripke语义的一些特定的中间逻辑。我们讨论了一些计算机科学感兴趣的例子，即这里和那里的逻辑，哥德尔-达米特逻辑和扬科夫逻辑。我们的方法提供了新的证明的完整性定理，由于Hoclane，Dummett/Horn和Jankov，分别。
2015-10-19 cs.LO
Dualized Simple Type Theory
我们提出了一种新的双直觉类型论，称为对偶类型论（DTT）。它是一个简单的类型论，具有完美的直觉对偶性，并对应于单边极化的微积分。我们证明DTT强正规化，并证明类型保持。DTT基于一种新的命题双直觉逻辑，称为对偶直觉逻辑（DIL），它建立在Pinto和Uustalu的逻辑L之上。DIL是L的一种简化，通过删除几个可接受的推理规则，同时保持一致性和完整性。此外，DIL是使用二元语法定义的，通过用极性标记公式和逻辑连接词，从而减少了定义逻辑所需的推理规则的数量。我们给出了相容性的一个直接证明，但证明完全性是通过约简到L。
2016-08-07 cs.LO
On Equivalence of Infinitary Formulas under the Stable Model Semantics
在直觉主义逻辑中等价的命题公式，或者在其扩展中被称为这里和那里的逻辑，具有相同的稳定模型。我们将这个定理扩展到具有无限长合取和析取的命题公式，并展示如何将此推广应用于证明答案集编程中聚合的性质。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-03-26 cs.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
There are (other) ways to negate in propositional team semantics
本文研究命题团队语义中的否定机制，证明完全直觉主义否定不增加向下封闭逻辑的公理化复杂度，并证明同时含依赖原子与包含原子的命题逻辑具有表达完备性。
2024-10-10 cs.LO math.LO
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
本文基于证明助手Isabelle/HOL，利用自由逻辑的浅层语义嵌入对范畴论进行元逻辑研究，形式化了初等拓扑斯与对称幺半闭范畴，并构建了易于使用的Isabelle范畴论库，为未来形式化研究奠定基础。
2023-06-16 cs.LO math.CT math.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
Intuitionistic Non-Normal Modal Logics: A general framework
我们定义了一类直觉非正规模态逻辑，它们可以被看作是经典模态逻辑的直觉对应物。我们首先考虑单峰逻辑，它只包含必然性和可能性之间的一个。然后，我们考虑更重要的情况下，双峰逻辑，其中包含两个模态算子。在这种情况下，我们定义了几个必要性和可能性之间的相互作用，尽管比对偶性弱。对于所有的逻辑，我们提供了一个希尔伯特公理化和一个切自由的代数演算，在此基础上，我们还证明了它们的可判定性。然后，我们给我们的逻辑在邻域模型的语义特征。我们的语义框架捕获模块化不仅我们的系统，但也已经知道的直觉非正常模态逻辑，如建设性K（CK）和Wijesekera的建设性并发动态逻辑的命题片段。
2019-01-28 cs.LO math.LO
Labelled Sequent Calculi for Propositional Team Logics
University of Helsinki（赫尔辛基大学）；University of Amsterdam, University of Southern Denmark（阿姆斯特丹大学，南丹麦大学）；University of Bern（伯尔尼大学）；Utrecht University（乌得勒支大学）
为基于团队语义的四种逻辑（基本探究逻辑、命题直觉主义依赖逻辑及其张量析取扩展）提供了可靠且完备的带标签矢列演算，并证明了弱化、收缩和切割规则的可容许性，最后给出了带简化标签的终止证明搜索过程。
2026-07-01 cs.LO
Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic
本文提出了一种在直觉逻辑中统一建模并行性与代数效应的框架，无需单子或双积，通过引入两种lambda演算及新的集合论解释实现。
2025-09-18 cs.LO math.CT
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
本文研究了命题直觉主义逻辑、一阶非常数论域直觉主义逻辑和一阶常数论域直觉主义逻辑的标号演算和套演算之间的关系。它示出，拟合的嵌套结石自然产生于其相应的标记结石-为上述每一个逻辑-通过消除标记派生的结构规则。这两种类型的系统之间的平移对应关系被用来表明嵌套演算从其相关的标记演算中继承了证明理论属性，例如规则的完整性，可逆性和切割容许性。由于标记的演算很容易通过逻辑的语义，本文提出的方法可以被看作是一个，从而细化版本的标记演算（包含嵌套的演算片段）具有良好的性能直接从逻辑的语义。
2021-04-19 cs.LO math.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
Intuitionistic Common Knowledge
Peking University（北京大学）
本文研究了直觉逻辑中的共同知识逻辑变种ICK，扩展了直觉命题逻辑IPL，引入多层知识算子和共同知识算子，并通过birelational Kripke模型分析其语义，证明了逻辑的完备性、有限模型性质和可判定性。
2026-05-01 cs.LO math.LO
Double-Negation Elimination in Some Propositional Logics
本文回答了两个问题（在文献中提出），每一个关于保证存在的证明免费的双重否定。一个证明是免费的双重否定，如果它的推导步骤都不包含一个项的形式n（n（t））的某些条款t，其中n表示否定。第一个问题要求对假设的条件，如果满足，保证存在一个双重否定-免费证明时，结论是免费的双重否定。第二个问题是关于经典命题演算的公理系统的存在性，该公理系统的使用，对于具有无双重否定结论的定理，保证了无双重否定证明的存在。在给出回答第一个问题的条件之后，我们通过关注Lukasiewicz三公理系统来回答第二个问题。然后，我们将我们的研究扩展到无限值微积分和直觉主义逻辑，并推广了双重否定自由的概念。利息的双重否定证明完全依赖于推理规则浓缩分离，这是一个将肯定前件与适当的一般替换规则相结合的规则。自动推理程序OTTER在本研究中发挥了不可或缺的作用。
2003-01-24 cs.LO
