Value Coalition Logic: A Typed Assignment-Based Reconstruction of Coalition Logic
School of Computer and Information Engineering (School of Artificial Intelligence), Henan Normal University（河南师范大学计算机与信息工程学院（人工智能学院））
本文提出价值联盟逻辑，通过类型化变量赋值重构经典联盟逻辑，在保持策略语义不变的同时，在原子层面引入值域完备性与互斥性，并证明与命题联盟逻辑在有限类型签名下真值等价，从而揭示值级不变量。
2026-05-25 cs.LO
Coalition and Group Announcement Logic
动态认知逻辑模型的能力，使各种公告和影响对方的知识，近年来已被广泛研究。这类逻辑的两个著名例子是组公告逻辑和联盟公告逻辑。它们使我们能够推理在非竞争和竞争环境中，代理人群体可以通过联合声明实现什么目标。在本文中，我们考虑这些逻辑的组合-联盟和组公告逻辑，并提供其完整的公理化。此外，我们部分回答了集团和联盟公告运营商如何互动的问题，并解决了其他一些开放的问题。
2017-07-27 cs.LO
Coalition and Group Announcement Logic
动态认知逻辑模型的能力，使各种公告和影响对方的知识，近年来已被广泛研究。这类逻辑的两个著名例子是组公告逻辑和联盟公告逻辑。它们使我们能够推理在非竞争和竞争环境中，代理人群体可以通过联合声明实现什么目标。本文考虑了这两种逻辑的一种组合--联盟逻辑和相对群通告逻辑，并给出了它的完备公理化。此外，我们部分回答了集团和联盟公告运营商如何互动的问题，并解决了其他一些开放的问题。
2018-10-03 cs.LO
Seven kinds of equivalent models for generalized coalition logics
Beijing Normal University（北京师范大学）
本文提出七类等价模型用于广义联盟逻辑，通过分析不同假设条件下的模型，揭示了八种联盟逻辑的有效公式集由六种其他模型决定。
2025-12-08 cs.GT cs.LO
Strategic Coalitions with Perfect Recall
Vassar College（瓦萨学院）；Lafayette College（拉斐特学院）
本文提出了一种双模态逻辑，描述了分布式知识模态和联盟专有技术模态之间的相互作用。与其他类似的系统不同，这里提出的一个假设所有代理的完美回忆。完美召回在系统中被一个公理捕获。主要的技术成果是所提出的逻辑系统的可靠性和完备性定理。
2017-11-14 cs.AI cs.LO
Reasoning About the Transfer of Control
University of Liverpool（利物浦大学）
我们介绍DCL-PC：一种逻辑，用于推理代理人和代理人联盟的能力如何通过将控制权从一个代理人转移到另一个代理人而改变。DCL-PC的逻辑基础是CL-PC，一种推理合作的逻辑，其中代理和代理联盟的能力源于原子布尔变量到单个代理的分布-联盟的选择对应于联盟控制的变量的分配。DCL-PC的基本模型结构是联盟C可以合作带来phi的形式。DCL-PC扩展了CL-PC的动态逻辑模态，其中原子程序的形式是代理i将变量p的控制权交给代理j;与动态逻辑中的常见情况一样，这些原子程序可以使用序列，迭代，选择和测试运算符组合以形成复杂的程序。通过将这种动态转移程序与合作模式相结合，可以推断代理人和联盟的权力如何受到控制权转移的影响。我们给出了两种替代语义的逻辑：一个直接的语义，在其中我们捕获的布尔变量的分布代理;和一个更传统的Kripke语义。我们证明了这些语义是等价的，然后给出了一个公理化的逻辑。我们调查的计算复杂性的模型检验和可满足性的DCL-PC，并表明，这两个问题是PSPACE完全的（因此不差于底层逻辑CL-PC）。最后，我们研究了DCL-PC的控制特性。我们区分一阶控制-代理或联盟通过分配值到代理或联盟控制下的变量来控制某些事务状态的能力-和二阶控制-代理通过将变量转移到其他代理来控制其他代理的能力。我们给出了二阶控制的逻辑刻画。
2014-01-16 cs.AI cs.LO
Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
我们提出了一个变体的ATL与分布式知识运营商的基础上同步和完善的召回语义。这种逻辑中的联盟模式是基于对完整历史的部分观察，并结合了联盟成员之间的合作形式，其中代理基于该联盟的系统历史的分布式知识发布其行动。我们表明，模型检验是可判定的这种逻辑。该技术利用两个变种的游戏与不完美的信息和部分可观察的目标，以及一个子集的建设，用于识别状态的历史是无法区分的考虑联盟。
2010-06-08 cs.LO cs.MA
First-Order Coalition Logic
本文提出融合CL与SL核心思想的一阶联盟逻辑FOCL，支持对智能体动作任意量化，证明其表达力严格更强，并给出SL变体中首个可靠完备的公理化。
2025-05-11 cs.LO
AUTO2, a saturation-based heuristic prover for higher-order logic
我们介绍了一个新的定理证明经典高阶逻辑命名为auto 2。证明器的设计是为了在搜索证明时使用人类指定的算法。核心算法是通过从初始假设导出的命题空间进行最佳优先搜索，其中新命题通过称为证明步骤的用户定义函数添加。我们在Isabelle/HOL中实现了证明器，并将其应用于数学和计算机科学的几个形式化项目，展示了它可以在各种可能的证明任务中提供的高水平自动化。
2016-05-24 cs.LO
Together We Know How to Achieve: An Epistemic Logic of Know-How
达成目标的联盟战略的存在并不一定意味着联盟有足够的信息来知道如何遵循该战略。这也不意味着联合政府知道这种战略的存在。本文研究了分布式知识、联盟战略和联盟“专有技术”战略之间的相互作用。主要的技术成果是一个健全和完整的三模态逻辑系统，描述了这种相互作用的性质。
2017-06-15 cs.AI cs.GT cs.LO
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.LO
An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
University of Greifswald（格赖夫斯瓦尔德大学）
逻辑嵌入工具为非经典推理问题到经典高阶逻辑提供了一个过程编码。它是可扩展的，可以支持越来越多的不同的非经典逻辑推理的目标。当用作高阶定理证明器的预处理器或库时，该工具允许逻辑的现成自动化，否则目前很少有证明器可用。
2022-03-23 cs.AI 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
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
Modal Extensions of Łukasiewicz Logic for Modeling Coalitional Power
推理联盟力量的模态逻辑抓住了与博弈形式相关的有效性函数的概念。联盟逻辑的主要目标是提供形式化的工具，用于对游戏框架的动态进行建模，该游戏框架的状态可能对应于不同的游戏形式。研究的两类有效性函数分别是可玩有效性函数族和真可玩有效性函数族。在本文中，我们推广了有效性函数的概念，超越了是/否真值尺度。这使我们能够描述联盟根据在有限的ukasiewicz链中取值的结果函数来评估其有效性的情况。然后，我们介绍了两个模态扩展的Eukasiewicz有限值逻辑与多值邻域语义，以编码的多值有效性函数的性质与游戏形式。作为我们的主要结果，我们证明了两个新引入的模态逻辑的完备性定理。
2015-12-08 cs.LO math.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
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
GeoLogic -- Graphical interactive theorem prover for Euclidean geometry
计算机中的数理逻辑领域主要由自动定理证明器（ATP）和交互式定理证明器（ITP）控制。这两种方法都很难被人工智能从人类模仿的方法中获得：ATP通常使用对人类不友好的逻辑基础，而ITP则用于形式化现有的证明，而不是解决问题。我们的目标是创建一个简单的人类友好的数学问题解决逻辑系统。我们选择了欧几里得几何的案例研究，因为它可以很容易地可视化，具有简单的逻辑，但可能会提供许多不同难度的高中问题。为了使环境对用户友好，我们放弃了ITP所要求的严格逻辑，允许从图片中推断拓扑事实。我们提出了我们的系统为欧几里德几何，连同一个图形应用程序GeoLogic，类似GeoGebra，它允许用户交互式地研究和证明几何设置的属性。
2020-05-07 cs.LO
A Logic of Inability
Henan Normal University（河南师范大学）
本文提出一种扩展的联盟逻辑，引入明确的无法能力算子，用于研究能力的模态概念，证明了其正确性、完备性和保守性，并分析了其模态行为。
2026-04-30 cs.LO math.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
Budget-Constrained Coalition Strategies with Discounting
Vassar College（瓦萨学院）；King’s College（国王学院）
贴现未来成本和回报是会计、博弈论和机器学习中的常见做法。尽管如此，现有的逻辑推理的战略与成本和资源的限制不考虑贴现。本文提出了一个健全的和完整的逻辑系统推理的约束下的战略能力，将折扣纳入其语义。
2021-05-10 cs.AI cs.GT 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
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
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
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
The Abella Interactive Theorem Prover (System Description)
Abella是一个交互式系统，用于推理对象语言的各个方面，这些方面已经通过基于语法结构的递归规则正式呈现。Abella使用两级逻辑方法来规范和推理。一个级别由规范逻辑定义，该规范逻辑支持结构语义规则的透明编码，并且还支持它们的执行。第二个层次，称为推理逻辑，嵌入规范逻辑，并允许开发有关规范的属性的证明。这两种逻辑的一个重要特征是，它们利用lambda树语法方法来处理对象语言中的绑定。除此之外，Abella还被用来证明λ演算的正规化性质、λ演算的截容许性、类型唯一性和主体归约性质。本文讨论了Abella的逻辑基础，概述了它支持的定理证明的风格，最后描述了它最近的一些应用。
2008-05-23 cs.LO cs.PL
A Survey on Theorem Provers in Formal Methods
机械推理是处于数理逻辑和人工智能交叉点的一个关键研究领域。开发机械推理系统（也称为定理证明器）的主要目的是使数学家能够通过计算机程序证明定理。然而，这些工具随着时间的推移而发展，现在在复杂和大规模系统的建模和推理中发挥着至关重要的作用，特别是安全关键系统。从技术上讲，数学形式主义和自动推理为基础的方法来执行推理，并在定理证明生成证明。在文献中，有一个全面的文件，可以提供适当的指导，定理证明器的设计，性能，逻辑框架，优势，差异和应用领域的偏好的短缺。在这项工作中，40多个定理证明器进行了详细的研究和比较，提出了一个全面的分析和评价这些工具。定理证明器的各种参数的基础上，其中包括：实现架构，使用的逻辑和演算，库支持，自动化水平，编程范式，程序设计语言，差异和应用领域进行了调查。
2019-12-06 cs.FL cs.LO cs.SE
A declarative approach to specifying Paxos using three-valued modal fixpoint logic
Heriot-Watt University（赫瑞-瓦特大学）；Ethereum Foundation（以太坊基金会）
本文提出三值模态不动点逻辑 Coalition Logic，将分布式算法表示为逻辑理论以声明式地规约和推导正确性，通过 Paxos 算法验证了其处理复杂系统的能力。
2026-10-23 cs.LO math.LO
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
ITMO University（圣彼得堡国立信息技术、机械学与光学研究型大学）；Australian National University（澳大利亚国立大学）
介绍了基于新的冲突消解演算的无等式纯一阶逻辑第一定理证明器Scavenger。冲突解决有一个限制性的决议推理规则，类似于（一阶泛化）单位传播，以及一个规则，用于假设决策文字和规则派生新的条款（一阶泛化）冲突驱动的条款学习。
2017-10-31 cs.AI cs.FL cs.LO
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
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
On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
针对交替时间时序逻辑ATL$^*$无法比较多策略交互、无法要求智能体共策略的局限，提出扩展逻辑HyperATL$^*_S$，支持超性质下的策略交互比较与策略共享，证明其模型检测可判定并实现工具HyMASMC完成基准评估。
2024-03-12 cs.AI cs.LO cs.MA
Formal verification of a proof procedure for the description logic ALC
描述逻辑（DL）是一种用于以结构化和形式化的方式表示和推理应用领域知识的语言。为了实现这一目标，已经实施了几个证明器，如RACER和FaCT++，但这些证明器本身尚未获得认证。为了确保这些DL中推导的合理性，有必要正式验证这些推理机应用的推导。形式化方法为证明过程的规范和验证提供了强大的工具，其中包括证明过程的可靠性，完整性和终止性等属性的方法。在本文中，我们提出了一个证明过程的描述逻辑ALC的定义，基于语义tableau方法。我们通过使用Isabelle证明助手证明其可靠性、完备性和终止性来确保证明器的有效性。证明分为两个阶段进行，首先在抽象级别上建立这些属性，然后将它们实例化以用于基于列表的实现。
2013-07-31 cs.LO
Quantified Multimodal Logics in Simple Type Theory
German Research Center for Artificial Intelligence (DFKI GmbH)（德国人工智能研究中心（DFKI GmbH））；International University of Germany（德国国际大学）；Jacobs University Bremen（不来梅雅各布大学）；Universität des Saarlandes（萨尔大学）
我们提出了一个简单的嵌入量化多模态逻辑的简单类型论，并证明其可靠性和完备性。模态算子被一类可能世界上的量化所取代。我们提出了简单的实验，使用现有的高阶定理证明，证明嵌入允许自动证明这些逻辑中的语句，以及它们的Meta属性。
2009-05-14 cs.AI cs.LO
Metamath Zero: The Cartesian Theorem Prover
随着定理证明器技术使用的扩展，对工具正确性的依赖也在增加。Metamath Zero是一个验证系统，旨在简化逻辑和实现，而不影响验证的效率。它是用自己的语言正式指定的，并支持与其他证明语言之间的大量翻译。本文描述了元路径零的抽象逻辑，本质上是一个多排序的一阶逻辑，以及二进制证明格式和它可以确保基本上线性时间验证的方式，同时仍然是简洁和有效的规模。Metamath Zero目前保持着ZFC中证明的$\mathtt{set .mm}$ Metamath库的最快验证记录（包括Wiedijk的100个形式化目标中的71个），不到200 ms。最终，我们打算用它来验证验证器实现的正确性，直到二进制可执行文件，因此它可以用作更复杂证明系统的信任根。
2020-03-30 cs.LO math.LO
Polymorphism Meets DHOL
University of Innsbruck（因斯布鲁克大学）；University of Melbourne（墨尔本大学）；University of Erlangen-Nuremberg（埃尔朗根-纽伦堡大学）
本文提出多态性DHOL，通过扩展HOL实现依赖类型，提升高阶逻辑在数据结构、范畴论等领域的应用效率，并通过工具实现自动化证明。
2026-07-01 cs.LO
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
我们提出了一个句法抽象方法，通过使用标准一阶逻辑和命题模态逻辑的定理证明器来推理一阶模态逻辑。
2014-09-12 cs.LO
Named Models in Coalgebraic Hybrid Logic
DFKI（德国人工智能研究中心）；Universität Bremen（不来梅大学）；Imperial College London（伦敦帝国理工学院）
混合逻辑扩展了模态逻辑，支持对由所谓的名词指定的各个状态进行推理。我们在共代数语义的广泛背景下研究混合逻辑，其中Kripke框架被替换为给定函子的共代数，从而涵盖了广泛的推理原则，包括，例如，概率、分级、默认或联合运算符。具体而言，我们建立通用标准，一个给定的共代数混合逻辑承认命名的规范模型，随后的完整性证明纯扩展一方面，和扩展的混合语言与本地绑定的其他。我们用一些例子来实例化我们的框架。值得注意的是，我们证明了具有局部约束的分次混合逻辑的完备性。
2010-02-03 cs.AI cs.LO
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
Key Laboratory of System Software（系统软件重点实验室）；State Key Lab. of Computer Science, Institute of Software Chinese Academy of Sciences（中国科学院计算技术研究所计算机系统结构国家重点实验室）；University of Chinese Academy of Sciences（中国科学院大学）；Huawei Technologies Co., Ltd.（华为技术有限公司）；National Key Laboratory of Space Integrated Information System, Institute of Software Chinese Academy of Sciences（中国科学院软件研究所空间信息系统国家重点实验室）；School of Computer Science, Peking University（北京大学计算机学院）
针对混合通信顺序进程（HCSP）建模的混合系统，提出基于混合霍尔逻辑的自动定理证明器HHLPar，通过符号分解、同步组合规范及集成外部求解器实现自动验证，经Isabelle/HOL形式化确保可靠，简化巡航控制系统实验验证了其性能。
2025-11-12 cs.LO
Certification of Prefixed Tableau Proofs for Modal Logic
不同的定理证明器倾向于以不同的格式产生证明对象，尤其是模态逻辑，其中已经提出了几种演绎形式主义（以及基于它们的证明器）。这项工作属于建立一个共同的规约语言，以证明在广泛的演绎形式主义的一般项目。特别是，通过使用从模态语言翻译成一阶极化语言和一个检查器，其小内核是基于一个经典的集中式微积分，我们能够证明模态证明标记的微积分，前缀tableaux和自由变量前缀tableaux。我们描述了逻辑K的一般方法，给出了它在一个类prolog语言中的实现，提供了一些例子，并讨论了如何将该方法扩展到其他正规模态逻辑
2016-09-14 cs.LO
Encoding TLA+ set theory into many-sorted first-order logic
我们提出了一个编码的Zermelo-Fraenkel集理论到许多排序的一阶逻辑，输入语言的国家的最先进的SMT求解器。这种转换是基于TLA+ Proof System中SMT求解器的后端证明器的主要组件。
2015-08-16 cs.LO
Proceedings of the 12th Workshop on User Interfaces for Theorem Provers
DFKI（德国人工智能研究中心）；U Coimbra（科英布拉大学）；University of Edinburgh（爱丁堡大学）；FU Berlin（柏林自由大学）；Stanford（斯坦福大学）；INRIA Sophia-Antipolis（法国国家信息与自动化研究所索菲亚-安提波利斯分部）
该系列研讨会汇集了对设计，开发和评估自动推理工具的用户界面感兴趣的研究人员，例如交互式证明助手，自动定理证明器，模型查找器，形式化方法工具以及可视化和操作逻辑公式和证明的工具。第12届CNOP在葡萄牙科英布拉举行，是自动推理国际联合会议（IJCAR'16）的一部分。研讨会包括一次特邀演讲、六次提交论文的介绍以及关于推理工具及其用户界面的生动实践会议。这些后续会议记录包含四篇投稿论文，在研讨会后经过第二轮审查后被接受出版，以及邀请论文。
2017-01-24 cs.AI cs.HC cs.LO
Sharing a Library between Proof Assistants: Reaching out to the HOL Family
我们今天观察到大量的证明系统的多样性。这种多样性的负面后果是，许多定理被证明了许多次。与程序设计语言不同，这些系统很难协同工作，因为它们不实现相同的逻辑。逻辑框架是一类定理证明器，它们通过实现各种逻辑的能力来克服这个问题。在这项工作中，我们研究了STTforall逻辑，简单类型论，已被编码在逻辑框架Dedukti的扩展。我们提出了一个翻译从这个逻辑OpenTheory，证明系统和互操作性工具之间的证明HOL家庭。我们已经使用这个翻译导出了一个包含费马小定理的算术库到OpenTheory和另外两个证明系统Coq和Matita。
2018-07-05 cs.LO
