A classical-logic view on a paraconsistent logic
本文研究次协调一阶逻辑 LPQ$^{\supset,\mathsf{F}}$，提出其自然演绎证明系统，通过嵌入一阶经典逻辑提供模型论与逻辑论证，并探讨其可判定性及逻辑性质，揭示其与经典逻辑的紧密联系。
2025-09-16 cs.LO math.LO
On the strongest three-valued paraconsistent logic contained in classical logic and its dual
LP $^{\supset,\mathsf{F}}$是一个三值次协调命题逻辑，本质上与J3相同。它的大多数属性都被认为是合理的次协调命题逻辑的理想属性。然而，从已经发表的结果可以很容易地得出，正好有8192个不同的三值次协调命题逻辑具有相关的性质。本文利用逻辑等价关系的性质来区分LP $^{\supset,\mathsf{F}}$与其它逻辑。作为专注于逻辑等价关系的奖金之一，它被发现，只有32的8192逻辑有一个逻辑等价关系，满足的单位，湮灭，幂等，和交换法律的合取和析取。LP $^{\supset,\mathsf{F}}$的大多数性质都被认为是合理的次协调命题逻辑的理想性质，而它的仿完全类似物也具有类似的性质。本文还利用逻辑等价关系的有关性质，将LP $^{\supset,\mathsf{F}}$的仿完全模拟与具有类似性质的其它三值仿完全命题逻辑区分开来。
2020-12-01 cs.LO math.LO
Paraconsistent Constructive Modal Logic
该研究提出构造模态逻辑CK的次协调对应逻辑族，基于带双赋值的直觉主义框架定义语义，提供希尔伯特式公理化与模块化无切割矢列演算，用于形式化矛盾但非平凡命题态度的推理并证明可判定性。
2025-08-25 cs.LO
Dialetheism, Game Theoretic Semantics, and Paraconsistent Team Semantics
我们介绍了一个变体的依赖逻辑中的真理定义不存在的获胜策略的支持者（Eloise）在语义游戏中，但在缺乏获胜策略的对手（Abelard）。我们证明了这种语言是一阶逻辑的保守但次协调的扩展，它的有效性问题可以归结为一阶逻辑的有效性问题，它能够表达自己的真值和有效性谓词，并且它在表达上等价于通用二阶逻辑。此外，我们证明了一个次协调的非依赖逻辑公式是一致的当且仅当它是等价于一些一阶逻辑句子;另一方面，我们表明，所有的次协调依赖逻辑句子等价于一些一阶句子就真（但不一定就假）。
2014-03-14 cs.LO math.LO
On Paraconsistent Weakening of Intuitionistic Negation
在[1]中，直觉主义否定逻辑的弱化系统Z_n和CZ_n是在da Costa方法的精神下发展起来的（参见[1]）。[2])通过保持，不同于da Costa，其基本性质：分配格的反序性，反演性和可加性。然而，根据[3]，这些系统不是次协调的，而是直觉主义逻辑的扩展。考虑到这一结果，我们在这里对Z_n和CZ_n的修正系作一些观察，它们也是次协调的。
2011-02-09 cs.LO
A Proof in Coq that Core Logic is not Paraconsistent
Université de Lorraine（洛林大学）
本文使用 Coq 证明 Tennant 的两个主张（即他的逻辑系统是次协调的且与最小逻辑重叠）均为假。
2026-07-20 cs.LO math.LO
Paraconsistent Gödel modal logic on bi-relational frames
我们进一步发展了次协调哥德尔模态逻辑。在本文中，我们认为它的版本赋予Kripke语义的$[0,1]$值框架与两个模糊关系$R^+$和$R^-$（程度的信任断言和否认）和两个估值$v_1$和$v_2$（支持的真理和支持的虚假性）与德摩根否定$\neg$。我们证明了\emph{does not}是哥德尔模态逻辑的扩展，并且$\Box$和$\lozenge$是不可互定义的.我们还表明，几个重要的类的框架是$\birelKGsquare$可定义的（特别是，脆，单关系，和单分支）。对于多分支框架上的$\birelKGsquare$，我们建立了一个完备的约束表演算和一个基于该演算的判定过程，并利用该判定过程证明了$\birelKGsquare$在PSPACE中的可满足性和有效性.
2023-03-24 cs.LO math.LO
The Dynamic Turn in Paraconsistency
Institute of Philosophy and Human Sciences, UNICAMP（坎皮纳斯州立大学哲学与人文科学学院）；University of Toulouse, IRIT-CNRS（图卢兹大学IRIT-CNRS）；Indian Institut of Technology (IIT)（印度理工学院）
该研究提出弗协调逻辑的动态转向，引入AMLFI1及其特殊情况PALFI1，还有带事实变化的UMLFI1，证明了这些逻辑的可靠性和完全性，它们扩展了已知认知弗协调逻辑，可形式化临时矛盾的获取与解决。
2026-07-23 cs.LO cs.MA
A machine-assisted view of paraconsistency
对于新手来说，次协调逻辑可能很难掌握。即使是逻辑专家也会发现副协调的概念是可疑的或被误导的，如果不是实际上错误的话。问题是，尽管它们通常与更熟悉的逻辑（如直觉主义逻辑或经典逻辑）有许多共同之处，但次协调逻辑在逻辑领域的其他部分必然不一致，人们可能认为这些部分不值得讨论。因此，一个人的逻辑直觉可能需要重新校准，以巧妙地与超协调性一起工作。在开始之前，我们应该清楚地认识到次协调逻辑的可能性以及次协调逻辑所指向的区别的一致性。为此，人们通常会遇到涉及两个以上真假值的矩阵来表征合适的结果关系。在双值怀疑论者的眼中，这种方法可能看起来可疑。即使是一个不怀疑的人也会怀疑是否还有其他方法。为此，在自动推理技术的帮助下探索次协调逻辑的基本概念。这种方法有其优点，因为通过将一些逻辑工作委托给机器，人们的逻辑“偏见”变得外在化。其结果是一种新的方式来欣赏的区别，次协调逻辑点确实是真实的。我们的方法甚至可以为次协调逻辑社区提出新的问题。
2013-12-16 cs.LO math.LO
Queries With Exact Truth Values in Paraconsistent Description Logics
Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800（波尔多大学、国家科学研究中心、波尔多INP、LaBRI、UMR 5800）；Japanese-French Laboratory for Informatics, CNRS, NII, IRL 2537（日法信息实验室、国家科学研究中心、日本信息机构、IRL 2537）；DI ENS, ENS, CNRS, PSL University & Inria, Paris, France（ENS DI、巴黎高等师范学院、国家科学研究中心、巴黎科学实验室与Inria、法国巴黎）
本文在准协调描述逻辑中引入四值Belnapian语义和真值算子以区分矛盾证据与正面证据，并通过归约到经典DL查询应答精确刻画了查询复杂度，证明Horn DL保持可处理的数据复杂度。
2024-08-15 cs.AI cs.DB cs.LO
Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
TU Dresden（德累斯顿工业大学）；Open Universiteit（荷兰开放大学）；University of Cape Town（开普敦大学）；ScaDS.AI Center for Scalable Data Analytics and Artificial Intelligence, Dresden/Leipzig（萨克森可扩展数据分析和人工智能中心）
本文利用近似不动点理论框架，为同时包含失败否定和强否定的模糊逻辑程序定义良好行为的语义，并证明该框架推广了多种现有语义并产生新语义。
2026-07-31 cs.LO
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
本文提出了一种用于CK、CK+ID、CK+MP和CK+MP+ ID等标准条件逻辑的无割演算SeqS.该演算使用标号和转移公式，可用于证明相应逻辑的可判定性和空间复杂度界.我们还提出了CondLean，这些逻辑实现SeqS演算SICStus Prolog写的定理证明。
2004-07-29 cs.AI cs.LO
A Resolution Prover for Coalition Logic
University of Brasília（巴西利亚大学）；Capital University of Economics and Business（首都经济贸易大学）；University of Liverpool（利物浦大学）
我们提出了一个原型工具，自动推理联盟逻辑，非正常模态逻辑，可用于推理合作机构。定理证明器CLProver是基于最近的工作，对联盟逻辑的联盟问题，联盟逻辑的范式的基于分辨率的演算。我们提供了一个概述的联盟问题和联盟逻辑的基于分辨率的演算。然后，我们详细介绍了CLProver的实现，并提出了与现有的基于表格的求解器的比较结果。
2014-04-03 cs.AI cs.LO
Paraconsistent logic and query answering in inconsistent databases
本文提出用亚相容逻辑LPQ$^{\supset,\mathsf{F}}$处理不一致数据库中的查询，无需数据库修复即可定义一致答案，并给出序列演算证明系统以支持证明搜索算法。
2023-03-11 cs.DB cs.LO
Holophrasm: a neural Automated Theorem Prover for higher-order logic
Stanford University（斯坦福大学）
我提出了一个使用深度学习和避免手工构造特征的高阶逻辑中的自动定理证明系统。Holophrasm利用Metamath语言的形式主义，并使用神经网络增强的强盗算法和序列到序列模型进行动作枚举来探索部分证明树。该系统从Metamath的set.mm模块中证明了14%的测试定理。
2016-08-10 cs.AI cs.LO
Abductive Reasoning in a Paraconsistent Framework
Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800（波尔多大学、法国国家科学研究中心、波尔多INP、LaBRI、UMR 5800）；Japanese-French Laboratory for Informatics, CNRS, NII, IRL 2537（日法信息实验室、法国国家科学研究中心、日本信息产业技术研究所、IRL 2537）；National Institute of Informatics, Tokyo, Japan（日本信息处理研究所）
本文在Belnap--Dunn四值逻辑的两种扩展中定义并研究溯因推理，证明二者不可互归约，分析相关推理任务复杂性，并给出归约到经典命题逻辑以复用现有方法。
2024-08-23 cs.AI cs.LO math.LO
Degree-preserving Godel logics with an involution: intermediate logics and (ideal) paraconsistency
University of Campinas（坎皮纳斯大学）；Artificial Intelligence Research Institute (IIIA) - CSIC（人工智能研究所（IIIA）- 西班牙国家研究委员会）；Universitat de Barcelona（巴塞罗那大学）
本文研究了介于具有involution的度保持Goedel逻辑与经典逻辑之间的中间逻辑，并探讨了其paraconsistency特性及饱和paraconsistency的特性。
2026-01-13 cs.LO math.LO
Paraconsistent and paracomplete probabilities: Measuring reliable and unreliable beliefs
University of Campinas (UNICAMP)（坎皮纳斯大学）
本文提出基于6值paradefinite逻辑LETK⁺的概率函数，利用twist结构语义解释逻辑概率，证明其可靠性与完备性，还给出LETK⁺上Jeffrey更新的语义与句法刻画并证明等价。
2026-08-21 cs.LO
A taxonomy for controlling (in)consistency
UNICAMP, CLE/IFCH（坎皮纳斯州立大学，计算与认知逻辑中心/人文与社会科学学院）
本文引入了LFIs的层级L_n^k和控制一致性逻辑（LCC），通过二维层次展示不同一致性、不一致性和否定程度，通过交换结构语义证明其正确性，并展示LFI3作为多值LFIs的范例。
2026-04-20 cs.LO
An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
University of Greifswald（格赖夫斯瓦尔德大学）
逻辑嵌入工具为非经典推理问题到经典高阶逻辑提供了一个过程编码。它是可扩展的，可以支持越来越多的不同的非经典逻辑推理的目标。当用作高阶定理证明器的预处理器或库时，该工具允许逻辑的现成自动化，否则目前很少有证明器可用。
2022-03-23 cs.AI cs.LO
AUTO2, a saturation-based heuristic prover for higher-order logic
我们介绍了一个新的定理证明经典高阶逻辑命名为auto 2。证明器的设计是为了在搜索证明时使用人类指定的算法。核心算法是通过从初始假设导出的命题空间进行最佳优先搜索，其中新命题通过称为证明步骤的用户定义函数添加。我们在Isabelle/HOL中实现了证明器，并将其应用于数学和计算机科学的几个形式化项目，展示了它可以在各种可能的证明任务中提供的高水平自动化。
2016-05-24 cs.LO
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.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
The Higher-Order Prover Leo-III (Extended Version)
Freie Universität Berlin（柏林自由大学）；University of Luxembourg（卢森堡大学）
给出了一个基于Henkin语义和选择的经典高阶逻辑自动定理证明器Leo-III。Leo-III是基于扩展的高阶调节，并接受每一个常见的TPTP方言（FOF，TFF，THF），包括他们最近的扩展秩1多态性（TF 1，TH 1）。此外，证明器本身支持几乎所有正常的高阶模态逻辑。Leo-III与一阶推理工具合作，使用多种一阶逻辑的翻译，并产生可验证的证明证书。证明器在异构基准集上进行评估。
2018-04-19 cs.AI cs.LO math.LO
A Theorem Prover for Quantum Hoare Logic and Its Applications
量子霍尔逻辑（QHL）在Ying的工作中被引入来描述和推理量子程序。在本文中，我们实现了一个定理证明QHL基于Isabelle/HOL。通过应用定理证明器，验证一个量子程序的规格等价地转化为矩阵之间的顺序关系。由于Isabelle/HOL的局限性，顺序关系的计算通过调用外部Python语言的oracle来解决。据我们所知，这是量子程序的第一个定理证明器。为了证明它的力量，两个著名的量子算法，即，Grover量子搜索和量子相位估计是Shor的多项式时间分解量子算法的关键步骤，利用定理证明器证明了这两个步骤。这是他们两人的第一次机械化证明。
2016-01-15 cs.LO
Contradiction-tolerant process algebra with propositional signals
在以前的论文中，ACP风格的进程代数，提出了命题被用作过程的状态的可见部分，并作为状态条件下，过程可以进行。这个进程代数，称为ACPps，是建立在经典命题逻辑上的。在本文中，我们提出了一个版本的ACPps建立在一个次协调命题逻辑，这是本质上相同的CLuNs。如果不采取特殊措施，许多系统将不得不处理自相矛盾的状态。对于许多这样的系统，可以想象，接受自相矛盾的状态并以基于次协调逻辑的方式处理它们是采取特殊措施的替代方案。所提出的ACPps版本可以适用于描述和分析的系统，处理自相矛盾的状态的方式基于上述的次协调逻辑。
2017-03-19 cs.LO
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Université Paris-Saclay（巴黎萨克雷大学）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；University of Greifswald（格赖夫斯瓦尔德大学）
本文提出一种在Dedukti框架中验证高阶逻辑自动定理证明器证明的通用方法论，应用于EP演算并集成至Leo-III，实现约80%证明步骤自动重构，成为首个支持独立可检查证明重构的高阶证明器。
2026-09-28 cs.LO
Isabelle: The Next 700 Theorem Provers
Isabelle是一个通用的定理证明器，设计用于各种形式理论的交互式推理。目前，它为构造类型论、各种一阶逻辑、Zermelo-Fraenkel集合论和高阶逻辑提供了有用的证明过程。这一调查伊莎贝尔作为一个介绍文学。它解释了为什么一般的定理证明是有益的。它提供了一个彻底的历史伊莎贝尔，从它的起源在LCF系统。它提出了一个帐户的逻辑是如何表示，说明使用经典逻辑。该方法与爱丁堡逻辑框架进行了比较。几个伊莎贝尔对象逻辑。
2000-10-31 cs.LO
Decoupling Evidence Sources in Paraconsistent Logic: A Generalized PAL2v Framework for Educational Assessment
Center for Logic, Epistemology and the History of Science (CLE), State University of Campinas (UNICAMP)（圣保罗州立大学逻辑、认识论与科学史中心）；Institute of Philosophy and the Humanities (IFCH), State University of Campinas (UNICAMP)（圣保罗州立大学哲学与人文学院）；Faculdade Israelita de Ciências da Saúde Albert Einstein (FICSAE)（阿尔伯特爱因斯坦以色列健康科学学院）
本文针对PAL2v逻辑中证据坐标耦合导致矛盾状态不可达的问题，提出解耦证据源构造，使所有逻辑状态可达，并给出完全决策过程，应用于教育评估以量化学生表现与投入差距。
2026-09-15 cs.LO math.ST stat.TH
GeoLogic -- Graphical interactive theorem prover for Euclidean geometry
计算机中的数理逻辑领域主要由自动定理证明器（ATP）和交互式定理证明器（ITP）控制。这两种方法都很难被人工智能从人类模仿的方法中获得：ATP通常使用对人类不友好的逻辑基础，而ITP则用于形式化现有的证明，而不是解决问题。我们的目标是创建一个简单的人类友好的数学问题解决逻辑系统。我们选择了欧几里得几何的案例研究，因为它可以很容易地可视化，具有简单的逻辑，但可能会提供许多不同难度的高中问题。为了使环境对用户友好，我们放弃了ITP所要求的严格逻辑，允许从图片中推断拓扑事实。我们提出了我们的系统为欧几里德几何，连同一个图形应用程序GeoLogic，类似GeoGebra，它允许用户交互式地研究和证明几何设置的属性。
2020-05-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
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
Working with first-order proofs and provers
软件正确性测试一直是一项重要而复杂的任务。最近，算法甚至实现的关键属性的形式化证明变得越来越实用。目前，最强大的自动化证明搜索工具使用一阶逻辑，而流行的交互式证明助手使用高阶逻辑。我们提出了一套正在进行的工具，旨在最终提供一个可用的一阶逻辑计算机辅助证明环境。
2019-04-03 cs.LO
Note on paraconsistency and reasoning about fractions
我们应用次协调逻辑来推理分数。
2015-03-06 cs.LO math.LO
Implementing the First-Order Logic of Here and There
University of Pernambuco（巴伊亚大学）；University of Potsdam（波茨坦大学）
本文提出了一种基于sequent 计算机和直觉逻辑嵌入的HT一阶逻辑自动定理证明器，并通过基准测试验证了其有效性。
2026-01-07 cs.AI cs.LO cs.PL
Proving Theorems using Incremental Learning and Hindsight Experience Replay
DeepMind
传统的一阶逻辑自动定理证明器依赖于速度优化的搜索和许多手工设计的算法，这些算法被设计成在广泛的领域中工作得最好。文献中的机器学习方法要么依赖于这些传统的证明器来引导自己，要么无法达到可比的性能。在本文中，我们提出了一个一般的增量学习算法的训练域特定的证明一阶逻辑没有等式，只基于一个基本的给定子句算法，但使用一个学习子句评分功能。子句被表示为图，并呈现给具有谱特征的Transformer网络。为了解决稀疏性和初始缺乏训练数据以及缺乏自然课程，我们将事后经验重放适应于定理证明，以便即使在没有证据的情况下也能够学习。我们表明，以这种方式训练的证明者可以在证明的数量和质量方面与TPTP数据集上的最先进的传统证明者相匹配，有时甚至超过。
2021-12-20 cs.AI cs.LO
Superposition for Lambda-Free Higher-Order Logic
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；Aesthetic Integration（Aesthetic Integration公司）；Max-Planck-Institut für Informatik（马克斯·普朗克信息学研究所）
本文为无λ高阶逻辑提出反驳完备的超位置演算，支持部分应用，通过非完全单调项序实现，在Zipperposition中实现并评估，有望推动全高阶逻辑自动定理证明器的发展。
2021-04-09 cs.AI cs.LO
Self-extensional logics of formal inconsistency: Decidability and limits for paraconsistency
Centre for Logic, Epistemology and the History of Science (CLE), University of Campinas (UNICAMP)（坎皮纳斯大学逻辑、认识论与科学史中心）；Institute of Philosophy and the Humanities (IFCH), University of Campinas (UNICAMP)（坎皮纳斯大学哲学与人文学院）
本文研究自扩展次协调逻辑RmbC的可判定性，分类一致性公理，识别爆炸性核心，证明其有限模型性质与可判定性，确定有效性问题的2-EXPTIME上界和coNP困难下界。
2026-09-21 cs.LO
Restricted Rules of Inference and Paraconsistency
在本文中，我们研究了逻辑的两个同伴，即，左变量包含同伴和限制规则同伴，它们的性质和相互关系，特别是与次协调。证明了两个伴点重合的一个充分条件。本文给出了两个新的逻辑系统--直觉次协调弱Kleene逻辑（IPWK）和次协调预粗糙逻辑（PPRL）--作为左变量包含逻辑的例子。IPWK是直觉命题逻辑（IPC）的左变量包含同伴，也是IPC的限制规则同伴，PPRL是Pre-Rough逻辑（PRL）的左变量包含同伴，但与PRL的限制规则同伴不同.这相当于引入了一个污染的真假值，旨在表示一种不确定性状态。
2021-07-13 cs.LO math.LO
Proceedings Eleventh Workshop on User Interfaces for Theorem Provers
该系列研讨会汇集了对设计，开发和评估自动推理工具的用户界面感兴趣的研究人员，例如交互式证明助手，自动定理证明器，模型查找器，形式化方法工具以及可视化和操作逻辑公式和证明的工具。第11届逻辑学大会在奥地利维也纳举行，是逻辑学领域有史以来规模最大的联合会议维也纳夏季会议的一部分。本会议录包含了八篇被接受在研讨会上发表的论文以及两篇受邀论文。
2014-10-29 cs.HC cs.LO
Using Automated Theorem Provers to Teach Knowledge Representation in First-Order Logic
学习人工智能的本科生常常难以将知识表示为逻辑句子。这是一种似乎需要大量实践才能获得的技能，这表明教学策略涉及分配大量练习，这些练习涉及一些知识的表达，使用自然语言（如英语）进行交流，作为某种逻辑中的句子。掌握这种技能所需的练习数量太多，以至于典型的人工智能课程教学团队无法对学生的努力提供及时的反馈。因此，需要一个自动化的评估系统，这样的练习，以确保学生得到足够的实践量，与反馈的快速传递，让学生在他们的理解和纠正错误。本文介绍了一个自动评分系统的知识表示练习使用一阶逻辑。归结定理证明器\textit{Prover9}用于检查学生提交的公式是否与教师提供的解决方案在逻辑上等价。这个系统已经被注册在本科人工智能班的学生使用了几年。使用这一教学工具导致了统计上的显着改善一阶逻辑知识表示问题出现在课程期末考试。本文解释了这个系统是如何工作的，提供了学生学习成果的变化分析，并探讨了这个系统的潜在增强功能，包括通过用基于表格的方法取代解决定理证明器来提供丰富的形成性反馈的可能性。
2015-07-14 cs.CY cs.LO
Swap Kripke models for deontic LFIs
本文首次将交换结构与克里普克模型结合，为基于LFIs的道义逻辑构造非确定性语义，并首次给出$C^{D}_n$层级的完整公理化与语义。
2025-06-06 cs.LO math.LO
The Abella Interactive Theorem Prover (System Description)
Abella是一个交互式系统，用于推理对象语言的各个方面，这些方面已经通过基于语法结构的递归规则正式呈现。Abella使用两级逻辑方法来规范和推理。一个级别由规范逻辑定义，该规范逻辑支持结构语义规则的透明编码，并且还支持它们的执行。第二个层次，称为推理逻辑，嵌入规范逻辑，并允许开发有关规范的属性的证明。这两种逻辑的一个重要特征是，它们利用lambda树语法方法来处理对象语言中的绑定。除此之外，Abella还被用来证明λ演算的正规化性质、λ演算的截容许性、类型唯一性和主体归约性质。本文讨论了Abella的逻辑基础，概述了它支持的定理证明的风格，最后描述了它最近的一些应用。
2008-05-23 cs.LO cs.PL
Extensional Higher-Order Paramodulation in Leo-III
University of Luxembourg（卢森堡大学）
Leo-III是一个自动化的定理证明器，用于扩展类型论，具有Henkin语义和选择。通过将基于调节的证明搜索适应于高阶逻辑来启用具有原始等式的推理。证明器可以与多个外部专家推理系统（诸如一阶证明器和SMT求解器）协作。Leo-III与TPTP/TSTP框架兼容，用于输入格式，报告结果和证明，以及推理系统之间的标准化通信，例如，从证明助手（如Isabelle/HOL）内部进行证明重建。Leo-III支持多态一阶和高阶逻辑，所有正常的量化模态逻辑以及不同的道义逻辑中的推理。它的发展开始了TPTP基础设施的不断扩展，以在非经典逻辑中进行推理。
2021-02-28 cs.AI cs.LO cs.SC
A Survey on Theorem Provers in Formal Methods
机械推理是处于数理逻辑和人工智能交叉点的一个关键研究领域。开发机械推理系统（也称为定理证明器）的主要目的是使数学家能够通过计算机程序证明定理。然而，这些工具随着时间的推移而发展，现在在复杂和大规模系统的建模和推理中发挥着至关重要的作用，特别是安全关键系统。从技术上讲，数学形式主义和自动推理为基础的方法来执行推理，并在定理证明生成证明。在文献中，有一个全面的文件，可以提供适当的指导，定理证明器的设计，性能，逻辑框架，优势，差异和应用领域的偏好的短缺。在这项工作中，40多个定理证明器进行了详细的研究和比较，提出了一个全面的分析和评价这些工具。定理证明器的各种参数的基础上，其中包括：实现架构，使用的逻辑和演算，库支持，自动化水平，编程范式，程序设计语言，差异和应用领域进行了调查。
2019-12-06 cs.FL cs.LO cs.SE
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
Abduction Prover in Isabelle/HOL
Institute of Computer Science, the Czech Academy of Sciences（捷克科学院计算机科学研究所）
针对基于表达逻辑的证明助手自动化程度低的问题，提出了一种利用溯因推理识别有用猜想并自动构建证明脚本的Isabelle/HOL溯因证明器。
2026-06-03 cs.AI cs.LO cs.PL
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
Northwestern University（西北大学）；IBM Research（IBM研究院）；IBM T.J. Watson Research Center（IBM托马斯·J·沃森研究中心）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；MIT-IBM Watson AI Lab（麻省理工学院-IBM沃森人工智能实验室）；IBM Zurich Lab（IBM苏黎世实验室）；The University of Auckland（奥克兰大学）
自动定理证明器传统上依赖于手动调整的算法来指导它们如何执行证明搜索。深度强化学习已经被提出作为一种方法来满足这种推理的需要，然而，它在自动定理证明中的部署仍然是一个挑战。在本文中，我们介绍了TRAIL，这是一个将深度强化学习应用于基于饱和的定理证明的系统。TRAIL利用（a）定理证明器状态的新神经表示和（b）推理选择过程在基于注意力的行动策略方面的新特征。我们通过系统的分析表明，这些机制使TRAIL显着优于以前的基于学习的定理证明器在两个基准数据集的一阶逻辑自动定理证明（证明约15%以上的定理）。
2020-09-16 cs.AI cs.LG cs.LO
Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities
我们提出了一个简单的理论解释的建设和正确性的增量和最坏情况下的模态逻辑的最佳决策过程与不测。该程序给出了一个抽象的重要方面的Goré和Widmann的PDL证明。从一个输入公式开始，该过程会生成一个Pratt样式的图形表，直到该表证明或否定该公式的可满足性。该程序提供了一个基础，实际证明，因为可满足性和不可满足性的公式，往往可以确定与小tableaux。
2012-09-06 cs.LO
On the Relational Translation Method for Propositional Modal Logics
模态逻辑中定理证明的一种方法是将它们转换为谓词演算，然后使用传统的归结式定理证明器。这种方法在实践中被认为是不合适的，因为得到的公式太长，而且不可能证明模态公式的非定理性。在本文中，我们证明了（关系）翻译方法的实际可行性。使用最先进的一阶谓词逻辑定理证明器，我们证明了模态逻辑文献中的许多基准定理。我们证明了命题模态和时态逻辑公式的无效性，使用模型生成器或可满足性测试的经典逻辑。许多可满足的公式被发现具有非常小的模型。最后，几种不同的方法进行了比较。
2021-12-29 cs.LO
Automating Induction by Reflection
尽管最近在全一阶理论的自动化定理证明方面取得了进展，归纳推理仍然对最先进的定理证明器提出了严峻的挑战。其原因是，在一阶逻辑中，归纳法需要无限数量的公理，这对于需要有限输入的计算机辅助定理证明器来说是不可行的。数学实践就是把这些无穷公理集指定为公理方案。不幸的是，这些图式定义不能在一阶逻辑中形式化，因此不支持作为一阶定理证明器的输入。在这项工作中，我们介绍了一种新的方法，启发真理的公理理论领域，允许表达示意归纳定义，在多排序的一阶逻辑的标准语法。此外，我们测试的实际可行性的方法与国家的最先进的定理证明，比较它的求解器的本地技术处理归纳。本文是LFMTP 21提交文件的扩展版本，具有相同的标题。
2021-06-09 cs.LO
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
本文为通信混合程序的动态逻辑提出均匀替换演算，通过公理替代公理模式并集中健全性检查，简化了含通信与并行性的混合系统证明器实现。
2023-07-18 cs.LO
Automating Induction by Reflection
尽管最近在全一阶理论的自动化定理证明方面取得了进展，归纳推理仍然对最先进的定理证明器提出了严峻的挑战。其原因是，在一阶逻辑中，归纳法需要无限数量的公理，这对于需要有限输入的计算机辅助定理证明器来说是不可行的。数学实践就是把这些无穷公理集指定为公理方案。不幸的是，这些图式定义不能在一阶逻辑中形式化，因此不支持作为一阶定理证明器的输入。在这项工作中，我们介绍了一种新的方法，启发真理的公理理论领域，允许表达示意归纳定义，在多排序的一阶逻辑的标准语法。此外，我们测试的实际可行性的方法与国家的最先进的定理证明，比较它的求解器的本地技术处理归纳。
2021-07-16 cs.LO
Formal verification of a proof procedure for the description logic ALC
描述逻辑（DL）是一种用于以结构化和形式化的方式表示和推理应用领域知识的语言。为了实现这一目标，已经实施了几个证明器，如RACER和FaCT++，但这些证明器本身尚未获得认证。为了确保这些DL中推导的合理性，有必要正式验证这些推理机应用的推导。形式化方法为证明过程的规范和验证提供了强大的工具，其中包括证明过程的可靠性，完整性和终止性等属性的方法。在本文中，我们提出了一个证明过程的描述逻辑ALC的定义，基于语义tableau方法。我们通过使用Isabelle证明助手证明其可靠性、完备性和终止性来确保证明器的有效性。证明分为两个阶段进行，首先在抽象级别上建立这些属性，然后将它们实例化以用于基于列表的实现。
2013-07-31 cs.LO
