HolPy: Interactive Theorem Proving in Python
HolPy是一个用Python实现的交互式定理证明系统。它使用高阶逻辑作为逻辑基础。它的主要功能包括广泛使用宏来生成，检查和存储证明，基于JSON的理论格式，以及用于在Python中实现证明自动化和其他扩展的API。一个点和点击为基础的用户界面，实现了通用的定理证明。我们描述了HolPy的主要设计决策、当前应用和未来计划。
2020-01-27 cs.LO
Introduction to Iltis: An Interactive, Web-Based System for Teaching Logic
逻辑是计算机科学许多现代领域的基础。在人工智能中，作为数据库查询语言的基础，以及在正式的软件和硬件验证中，使用逻辑形式主义和推断新知识来建模场景是未来计算机科学家的重要技能。Iltis项目旨在提供一个基于网络的交互式系统，支持逻辑方法的教学。特别是，该系统应（a）支持学习建模知识，并使用命题逻辑，模态逻辑和一阶逻辑推断新知识，以及（b）为学生提供即时反馈和支持。本文提出了一个原型系统，目前支持命题逻辑的上述任务。第一印象，它的使用在二年级逻辑课程的计算机科学学生的报告。
2018-04-04 cs.CY cs.LO
The Design of an Interactive Proof Mode for Dafny
Alexandru Ioan Cuza University（亚历山德鲁·约安库扎大学）；Amazon Web Services Inc（亚马逊网络服务有限公司）
Dafny 系统引入交互证明模式，通过动机示例和原型实现展示其设计与功能。
2025-12-23 cs.LO
The logic of interactive Turing reduction
本文从可计算性逻辑的语义出发，将直觉蕴涵理解为交互式算法约简，给出了直觉演算的蕴涵片段的可靠性和完备性证明。这个概念--更准确地说，是归约的相关概念--是图灵归约从传统的输入/输出问题到任意交互程度的计算任务的概括。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version
TU Dresden（德累斯顿工业大学）
描述逻辑蕴涵的解释为大型本体的维护提供了重要的支持。在本体编辑器中通常用于此目的的“证明”精确指出本体中负责给定蕴涵的部分。蕴涵的证明使中间的推理步骤变得明确，从而解释了一个结论实际上是如何推导出来的。我们提出了一个交互式的系统，探索描述逻辑证明，称为Evonne，可视化的表达DL写的本体论的后果证明。我们描述了用于计算这些证明的方法，以及一个称为基于签名的证明浓缩的功能。此外，我们使用真实的本体来评估生成的证明的质量。
2022-05-19 cs.AI cs.LO
Interactive Proof Presentations with Cobra
我们提出了眼镜蛇，一个现代的证明演示框架，利用尖端的演示技术与最先进的交互式定理证明器一起，将形式化的数学作为活动文档呈现。眼镜蛇提供了一种简单的方式来提出证明和一种新颖的方法，礼堂互动。演示文稿由定理证明者现场检查，并且允许演示者和观众进行现场更改。
2017-01-25 cs.LO
A Logic of Interactive Proofs (Formal Theory of Knowledge Transfer)
我们提出了一个交互式证明的逻辑作为交互式计算的直观基础的框架，我们通过一个交互式的类似的Goedel-McKinsey-Tarski-Artemov定义的直观逻辑嵌入到一个经典的模态逻辑的证明，和Curry-Howard同构之间的直观证明和类型化的程序。我们的交互式证明实现了持久的认知影响，在他们的预期社区的同行评审，包括在诱导的（命题）知识，他们的证明目标的（个人）知识的证明与解释审查。也就是说，交互式证明通过在多代理分布式系统中传输某些个人知识（可知证明）来实现命题知识（可知事实）的转移。换句话说，我们作为一个社区可以拥有正式的共同知识，即如果我们的一个对等成员知道证明，那么该成员就会知道它的证明目标。最后但并非最不重要的是，我们证明了非平凡的交互式计算定义在我们的简单类型的交互式组合逻辑，但等价于非交互式计算定义的简单类型的组合逻辑。
2017-08-08 cs.CR cs.DC cs.LO
A Monadic Framework for Interactive Realizability
我们给出了一个新的介绍互动的可实现性与更明确的语法。交互式可实现性是一种可实现性语义，它将Curry-Howard对应扩展到（次）经典逻辑，更确切地说，扩展到一阶直觉算术（Heyting Arithmetic），该算术由排除中间法则扩展到简单的存在公式，这是一个由其在证明挖掘中的应用所激发的系统。Monad可以通过提供一种干净和模块化的方式来包含纯函数式语言中的不纯功能来构建函数式程序。我们表示交互式实现器的抽象框架，适用于一元的方法在函数式编程修改的可实现性，以获得更“宽松”的可实现性的概念，是适合于经典逻辑。特别是，我们使用的状态和异常单子的组合，以捕捉从错误中学习的交互式实现者在语法层面上的性质。
2013-10-15 cs.LO
Teaching Interactive Proofs to Mathematicians
这项工作讨论了一种方法来教数学家的重要性和有效性的应用交互式定理证明工具，在他们感兴趣的特定领域。该方法旨在通过短期课程鼓励使用这些工具。特别是，它讨论了如何使用的情况下，研究代数概念和属性，使用的证明助手原型验证系统PVS促进兴趣的数学家在他们的机械化证明的发展。
2020-10-30 cs.LO
A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices
具有寄存器和语音的交互式系统（简称“rv系统”）是一种用于交互式计算的模型，该模型相对于时空对偶变换获得了闭寄存器机（“语音”是“寄存器”的时间对偶对应物）。同样的，AGAPIA v0.1，一种用于rv系统的结构化程序设计语言，是经典while程序（针对特定类型的数据）的时空对偶闭包。典型的AGAPIA程序描述了位于不同地点的开放过程，并具有对环境做出适当反应的时间窗口。该语言自然地支持流程迁移、结构化交互和在异构机器上部署组件。本文介绍了一种用于验证AGAPIA v0.1程序的类Hoare时空逻辑。作为一个案例研究，一个流行的分布式终止检测协议的形式化验证证明。
2008-10-19 cs.LO cs.PL
Towards Interactive Logic Programming
线性逻辑编程使用可证明性作为计算的基础。在基于可证明性的操作语义中，如果$G_1$和$G_2$都可从$P$求解，则从程序$P$执行加性-合取目标$G_1 \& G_2$简单地以成功终止。这是一种不令人满意的情况，因为在这种语义中缺少\&的中心动作--用户选择$G_1$或$G_2$的动作。我们建议修改上面的操作语义以允许用户更积极地参与。我们说明了我们的想法，通过muProlog，Prolog的扩展添加剂的目标。
2015-07-01 cs.LO cs.PL
The Abella Interactive Theorem Prover (System Description)
Abella是一个交互式系统，用于推理对象语言的各个方面，这些方面已经通过基于语法结构的递归规则正式呈现。Abella使用两级逻辑方法来规范和推理。一个级别由规范逻辑定义，该规范逻辑支持结构语义规则的透明编码，并且还支持它们的执行。第二个层次，称为推理逻辑，嵌入规范逻辑，并允许开发有关规范的属性的证明。这两种逻辑的一个重要特征是，它们利用lambda树语法方法来处理对象语言中的绑定。除此之外，Abella还被用来证明λ演算的正规化性质、λ演算的截容许性、类型唯一性和主体归约性质。本文讨论了Abella的逻辑基础，概述了它支持的定理证明的风格，最后描述了它最近的一些应用。
2008-05-23 cs.LO cs.PL
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
我们提出了一个综合的两个证明风格的交互式定理证明：程序风格（其中证明是脚本的命令，如在Coq）和声明式风格（其中证明是文本在一个受控的自然语言，如在Isabelle/Isar）。我们的方法结合了声明式风格的优点-编写正式证明的可能性，如正常的数学文本-和程序风格-强大的自动化和帮助形成的证明，包括确定中间步骤的声明。我们的方法是新的，显着不同的方式，程序和声明式的证明风格已经结合在伊莎贝尔，Ssreflect和Matita系统。我们的方法是通用的，可以实现任何程序的交互式定理证明器，无论其架构和逻辑基础。为了展示我们提出的方法的可行性，我们将其完全实现为一个名为miz 3的证明接口，位于HOL Light交互式定理证明器之上。这个接口使用的声明式语言是Mizar系统语言的一个轻微变体，可以用于任何交互式定理证明器，无论其逻辑基础如何。miz 3界面允许轻松访问HOL Light的全套战术和正式库，因此具有“工业实力”。我们的方法提供了一种方法，自动转换任何程序的证明，一个声明的副本，其中转换后的证明是类似的大小，原来的。由于所有的声明式系统本质上都有相同的证明语言，这提供了一种在交互式定理证明器之间移植证明的简单方法。
2012-03-27 cs.LO
An interactive semantics of logic programming
我们适用于逻辑编程的一些最近出现的想法，从该领域的减少为基础的通信系统，目的是提供证据的隐藏的相互作用和协调机制，规则的运作机制，这样的编程范式。语义框架，我们选择了我们的结果是瓦片逻辑，它的优点是允许一个统一的治疗目标和意见，并应用抽象的分类工具来证明结果。作为主要的贡献，我们提到的有限表示的抽象统一，和并发和协调的抽象语义逻辑编程的最常见的语义相一致。此外，拼块语义的组合性由标准结果保证，因为它减少了对与逻辑程序相关联的拼块系统享有拼块分解属性的检查。还讨论了处理约束系统的方法的扩展。
2001-07-17 cs.LO cs.PL
A Formal Approach based on Fuzzy Logic for the Specification of Component-Based Interactive Systems
形式化方法被广泛认为是分布式交互系统的规范、仿真、开发和验证的一种强有力的工程方法。然而，大多数形式化方法依赖于二值逻辑，因此受限于该逻辑的公理：规范有效或无效，组件行为可实现或不可实现，安全属性保持或被违反，系统可用或不可用。特别是当问题域具有不确定性，不精确性和不确定性时，这些方法的应用成为一项具有挑战性的任务。为了克服形式化方法的严格工作方式所带来的局限性，本文的主要目的是通过使用模糊逻辑来放松形式化规范的布尔概念。本方法是基于焦点理论，一个基于模型的和严格的形式化方法，基于组件的交互式系统。这项工作的贡献是双重的：i）我们引入了规范技术的基础上，模糊逻辑，可用于顶部的焦点开发正式规范的定性方式; ii）我们部分扩展焦点理论的模糊，它允许规范的模糊组件和模糊的相互作用。虽然前者提供了一种方法来近似I/O行为下的不精确性，后者能够捕捉到一个更定量的规格属性，如可实现性。
2015-03-17 cs.LO cs.SE
Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
School of Software, Northwestern Polytechnical University（西北工业大学软件学院）；School of Computer Science and Ningbo Institute, Northwestern Polytechnical University（西北工业大学计算机科学与宁波研究院）；Research Institute of Trustworthy Autonomous Systems, Southern University of Science and Technology（南方科技大学可信自主系统研究院）；Department of Computer Science and Engineering, Southern University of Science and Technology（南方科技大学计算机科学系）
本文研究了现有证明合成技术无法证明的定理特征，提出基于人类专家证明模式的模式引导战术搜索方法，提升证明成功率和复杂定理的证明能力。
2026-04-27 cs.LO
Statistical Proof Pattern Recognition: Automated or Interactive?
在本文中，我们比较了不同的现有方法，在数据采掘的大型证明库中的自动化和交互式定理证明。
2013-03-05 cs.LO cs.SE
A gentle introduction to Girard's Transcendental Syntax for the linear logician
从技术上讲，先验语法是关于设计具有计算基础的逻辑。它提出了一个新的证明理论框架，其中逻辑（证明，公式，真理，......）并不比计算更原始。所有的逻辑实体和活动都将在给定的计算模型上以格式化/结构化的形式呈现，该模型应尽可能通用，简单和自然。先验语法中逻辑的选择基础是一种我称之为“恒星解析”的计算模型，它基本上是罗宾逊一阶子句解析的无逻辑重构，具有与瓦片系统相关的动态。先验语法的一个初始目标是从这个新框架中恢复线性逻辑。特别地，该模型自然地编码证明结构的切割消除。通过使用“交互式类型”的思想，让人想起可实现性理论，可以设计公式/类型来概括线性逻辑的连接词。由于交互式类型，我们能够达到一个语义自由的空间，正确性标准被视为测试（如在单元测试或模型检验）证明逻辑正确性，从而允许有效地使用逻辑实体。
2022-04-05 cs.LO
Interactive Visualization of Saturation Attempts in Vampire
形式化方法的许多应用需要对系统属性进行自动推理，例如系统安全性和保密性。为了提高自动推理引擎（如SAT/SMT求解器和一阶定理证明器）的性能，有必要了解这些引擎在生成正式证书（如逻辑证明和/或模型）方面的成功尝试和失败尝试。这种分析是具有挑战性的，因为在证明/模型搜索期间生成了大量的逻辑公式。在本文中，我们专注于饱和为基础的一阶定理证明，并介绍了SATVIS工具的交互式可视化饱和为基础的证明尝试在一阶定理证明。我们建立在世界领先的定理证明器VAMPIRE之上的SATVIS，通过交互式可视化SATVIS中VAMPIRE的饱和尝试。我们的工作结合了自动布局和可视化的衍生图引起的饱和尝试与交互式转换和搜索功能。因此，我们能够分析和调试（失败）证明尝试的吸血鬼。由于其交互式可视化，我们相信SATVIS可以帮助专家和非专家在定理证明理解一阶证明和分析/完善失败的证明尝试的一阶证明。
2020-01-13 cs.LO
Automatic verification and interactive theorem proving
自动验证是通过计算机验证正确性证书。相关的工具，通常称为证明助手或交互式证明器，提供了一个交互式环境，用于创建正式证书，其正确性可以完全自动地进行评估。这种系统在数学和计算机科学中都有应用，在数学中证书是定理的证明，在计算机科学中证书证明给定软件在其规范方面的正确性。
2017-01-13 cs.LO
ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic
本文提出证明检索引擎ProofCloud，为高阶逻辑中的已验证证明提供快速搜索与复用服务，并首次给出OpenTheory仓库的完整证明检查结果和基准。
2024-12-30 cs.LO
Surface Proofs for Nonsymmetric Linear Logic (Extended Abstract)
证明了乘性线性逻辑中的一个证明可以表示为一个修饰曲面，使得两个证明仅当它们的曲面在几何上等价时，它们在逻辑上等价。这是arXiv的扩展摘要：1601.05372。
2017-01-18 cs.LO
Automated proof search system for logic of correlated knowledge
本文提出了相关知识逻辑的自动证据检索系统和可判定性。证明系统的核心是具有可靠性、完备性、截集规则和结构规则的可容许性以及所有规则的可逆性等性质的逻辑演算。证明搜索过程的基础上的微积分执行自动终止证明搜索，并允许我们实现相关知识的逻辑决策结果。
2019-02-23 cs.LO
Incorporating Inductions and Game Semantics into Logic Programming
归纳和博弈语义是对传统逻辑程序设计的两个有用的扩展。具体地说，归纳法可以捕获逻辑编程中更广泛的一类可证明公式。采用博弈语义可以使逻辑编程更具交互性。在本文中，我们提出了一个执行模型的逻辑语言与这些功能。这种执行模型密切遵循现实生活中的推理过程。
2015-08-08 cs.LO
Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK
本研究整合模态逻辑终止表方法与直觉主义模态逻辑IK的有穷框架性质，为FIK和LIK给出更简洁的全新可判定性证明。
2025-03-24 cs.LO
FMP for QD logics. A wrong proof
本文旨在证明准密集逻辑具有FMP，但证明中存在无法修复的重大错误。
2026-03-16 cs.LO
Logic of Non-Monotonic Interactive Proofs (Formal Theory of Temporary Knowledge Transfer)
我们提出了一个单调逻辑的内部化非单调或即时交互证明（LiiP）和重建现有的单调逻辑的内部化单调或持久交互证明（LiP）作为一个最小的保守扩展LiiP。即时交互式证明在其预期的同行评审者社区中产生了脆弱的认识影响，这种影响在于通过与解释评审者的证明知识对他们的证明目标的知识的短暂归纳：如果我的同行评审者知道我的证明，那么她至少会（在那一瞬间）知道它的证明目标是正确的。它们的影响是脆弱的，它们对知识的归纳也是短暂的，因为它可能只在学习证明的瞬间才存在。这就解释了将真值可以变化的陈述的证明内在化的重要可能性，与不变陈述相反，这些陈述不能有持久的证明。因此，即时交互证明通过在多个交互代理的分布式系统中传输某些个人知识（可知的非单调证明）来实现某些命题知识（可知的短暂事实）的临时转移。
2013-01-31 cs.CR cs.DC cs.LO
Focusing and Polarization in Intuitionistic Logic
聚焦证明系统提供了一个范式，以结构化的可逆和不可逆推理规则的应用程序的切割自由证明。Andreoli的线性逻辑的聚焦证明系统已经被应用于证明搜索和证明归一化方法。文献中的各种证明系统都表现出某种程度上的聚焦特性。我们提出了一个新的，集中的证明系统的直觉逻辑，称为LJF，并显示如何其他证明系统可以映射到新的系统，通过插入逻辑连接，过早地停止聚焦。我们还使用LJF设计了一个经典逻辑的集中证明系统。我们的方法来设计和分析这些系统的基础上的完整性集中在线性逻辑和极性的概念，出现在吉拉德的LC和LU证明系统。
2007-08-16 cs.LO
A survey of proof nets and matrices for substructural logics
本文是一个调查的两种“压缩”证明计划，\emph{matrix method}和\emph{proof nets}，适用于各种逻辑沿着子结构层次从经典的所有方式到非关联的Lambek系统。为后者提供了一种新的处理证明网。证明网和矩阵的描述给出了一个统一的符号序列的基础上，使各种逻辑的计划的属性可以很容易地进行比较。
2012-03-22 cs.LO
Complexity of correctness for pomset logic proof nets
我们表明，它是coNP-完全的，以决定是否一个给定的证明结构的pomset逻辑是一个正确的证明网，使用图论在我们以前的文件（arXiv：1901.10247）。
2023-01-23 cs.LO
ALICE: An Advanced Logic for Interactive Component Engineering
本文介绍了一个概述的验证框架ALICE在其当前版本0.7。它基于通用定理证明器Isabelle [Pau 03 a]。在ALICE中，软件或硬件组件被指定为具有定向通信信道的全状态黑盒。组件通过这些通道发送和接收异步消息。组件的行为通常被描述为一种与观察结果的关系，这种关系以流经其输入和输出通道的消息流的形式出现。支持非定时和定时以及基于状态的、递归的、关系的、等式的、假设/保证的和函数式的规格说明。因此，ALICE是非常适合的形式化和验证的分布式系统建模与此流处理范例。
2014-10-16 cs.LO cs.SE
Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings
我们使用分支离散时间结构上的STIT语义来表征四种类型的代理知识。它们是\emph{ex ante}知识、\emph{ex interim}知识、\emph{ex post}知识和专有技术。前三个概念来自于对决策过程中信息披露阶段的博弈论分析，第四个概念在行动逻辑和道义逻辑中都获得了突出地位，作为一种形式化能力的手段。近年来，人工智能领域的逻辑学家认为，任何关于责任归属和罪责的全面研究都应该包括对这类知识的适当处理。本文旨在澄清以前的尝试，正式在STIT逻辑，并提出替代的解释，在我们看来，更类似于STIT传统的责任研究。我们提出的逻辑使用扩展与知识运营商的Xstit语言，公式进行评估分支离散时间模型。我们还提出了一个公理系统的逻辑，并解决其健全性和完整性。
2019-11-19 cs.LO math.LO
An Interactive Proof of Termination for a Concurrent $λ$-calculus with References and Explicit Substitutions
在本文中，我们介绍了一个类型化的，并发的$λ$ -演算的引用具有显式替换变量和引用。除了通常的安全属性，我们恢复了强正常化。证明是基于一个reductiontechnique和一个原始的互动属性让人想起游戏语义的方法。
2021-02-09 cs.LO cs.PL
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
本文给出了基本正规时态逻辑Kt的一个线性嵌套演算。我们表明，演算，使向后证明搜索，反模型建设和句法切割消除。因此，线性嵌套序列提供了为包含逆的模态逻辑提供足够的证明理论所需的最小嵌套量。作为奖励，这产生了对称模态逻辑KB的无切演算。
2019-07-02 cs.LO
Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
我们产生了一个可判定的超直觉正常模态逻辑的内在直觉（从而析取和单调）交互式证明（LIIP）从现有的经典对应的经典单调非析取交互式证明（LiP）。直觉主义交互式证明在可能的对抗性通信媒介CM（被想象为一个杰出的代理人）中产生持久的认知影响，并且只有在这种情况下，它才包括通过CM的证明知识永久地归纳出他们的证明目标的完美知识和分离知识：如果CM知道我的证明，那么CM将持续地并且分离地知道我的证明目标是真的。因此，直觉交互式证明通过某些个体知识（可知直觉证明）的传输，在多智能体分布式系统的通信介质中实现了选言命题知识（选言可知事实）的持久传输。我们（必然）以CM为中心的证明概念也是KD 45-信念的析取显式细化，并且也产生了标准S5-知识的这种细化。单调性而非公共性是LiP、LIiP及其内在证明概念的共性。作为一个副作用，我们提供了一个简短的内在证明的析取性质的直觉主义逻辑（最初证明的哥德尔）。
2014-04-08 cs.CR cs.LO math.LO
Logic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)
我们产生了一个可判定的经典正常模态逻辑的内在否定完全，从而析取非单调交互式证明（LDiiP）从现有的逻辑对应的非单调或即时交互式证明（LiiP）。LDiiP内化了以主体为中心的证明论，这些理论是否定完备的（最大的）和一致的（因此严格弱于例如皮亚诺算术），并享有析取属性（如直觉主义逻辑）。换句话说，内化证明论是超过滤器，所有内化证明目标都是确定的，通过析取内化证明（因此也称为认识决定者）对代理人来说是可证明或不可证明的。尽管如此，LDiiP本身是经典的（单调的，非构造性的），负不完全的，并且不具有析取性质。我们的交互式证明的否定完全性的代价是它们的非单调性和非公共性（仅适用于单例代理社区）。作为一个正常的模态逻辑，LDiiP享有一个标准的Kripke语义，我们证明通过调用选择公理的LiiP的，然后构造一个具体的预言计算功能。LDiiP的以代理人为中心的内在化证明概念也可以被视为标准KD 45信念的否定完全析取显式精化，并产生S4可证明性的析取但否定不完全显式精化。
2013-05-29 cs.CR cs.DC cs.LO
A program logic for union bounds
我们提出了一个基于联合界的概率霍尔逻辑aHL，这是一个来自基本概率论的工具。虽然联合界很简单，但它是分析随机算法的一个非常常用的工具。在形式化验证术语中，联合边界允许对算法可能出错的可能方式进行灵活和组合推理。它也使得关于概率的推理和关于事件的推理之间能够清晰地分离，这在我们的逻辑中被表示为标准的一阶公式。值得注意的是，我们逻辑中的断言是非概率性的，尽管我们可以从判断中得出概率性的事实。我们的逻辑还可以证明交互式程序的准确性，程序必须在输入到达时立即产生中间输出，而不是一次访问整个输入。此设置还启用自适应性，其中较晚的输入可能取决于较早的中间输出。我们展示了如何证明准确性的几个例子，从差分隐私文学，互动和非互动。
2019-11-08 cs.LO cs.PL
An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
微分线性逻辑丰富了线性逻辑与额外的逻辑规则的指数连接，对偶的通常规则的遗弃，削弱和收缩。本文提出了微分线性逻辑的证明网语法及其指称模型的范畴公理化。我们还介绍了一个简单的分类条件下，这些模型的一般反导数操作变得可用。最后，我们简要地描述了集合和关系的模型，并给出了有限性空间和线性和连续函数的模型更详细的说明。
2016-06-06 cs.LO
Interactive Unawareness Revisited
我们分析了海菲兹，迈耶和席佩尔（HMS）介绍的互动无意识模型。我们考虑两个公理化的模型，捕捉不同的概念的有效性。这些公理化使我们能够比较HMS方法的标准（S5）认知逻辑和其他两种方法的无意识：费金和Halpern和莫迪卡和Rustichini。我们发现，HMS方法和其他之间的差异主要是由于使用的有效性的概念和事实，即HMS是基于一个3值命题逻辑。
2005-09-19 cs.AI cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Proof Normalisation in a Logic Identifying Isomorphic Propositions
我们定义了一个片段的命题逻辑同构命题，如$A\land B$和$B\land A$，或$A\Rightarrow (B\land C)$和$(A\Rightarrow B)\land(A\Rightarrow C)$被识别。我们定义了系统I，这个逻辑的证明语言，并证明其规范化和一致性。
2019-04-22 cs.LO
Proof-graphs for Minimal Implicational Logic
众所周知，命题经典证明的规模可能是巨大的。证明理论研究发现正常或切割自由证明和他们各自的非正常证明之间的指数差距。本文的目的是研究如何降低命题推理的权重。我们提出了形式主义的证明图的纯蕴涵逻辑，这是一个特定的形状，旨在捕捉演绎的逻辑结构的图形。这种形式主义的优点是公式可以在简化证明中共享。本文给出了最小蕴涵逻辑证明图的精确定义，并给出了证明图的规范化过程。与标准的树状形式主义相比，我们的规范化并没有增加节点的数量，当应用到相应的最小证明图表示。
2014-04-01 cs.LO
A Proof Tree Builder for Sequent Calculus and Hoare Logic
我们已经开发了一个基于Web的教学证明助手，证明树生成器，它可以让你从最初的目标向上应用规则在微积分和霍尔逻辑的一个简单的命令式语言。我们配备了一个基本的证明自动化功能和Z3集成我们的工具。普林斯顿大学自动推理课程的学生使用了我们的工具，并发现它很直观。证明树生成器可在https://proof-tree-builder.github.io上在线获得。
2023-03-10 cs.LO
Focused Proof-search in the Logic of Bunched Implications
集束蕴涵（BI）逻辑自由地组合了加法和乘法连接词，包括蕴涵;然而，尽管其证明理论得到了充分的研究，但BI中的证明搜索一直是一个难题。聚焦原则是对证明-搜索空间的一种限制，它可以捕获各种目标导向的证明-搜索过程。在本文中，我们表明，集中的证明搜索是完整的BI首先重新制定传统的束的嵌套序列，使用更简单的数据结构，然后与极化和集中的变体，我们显示是健全的和完整的，通过削减消除参数。这建立了一个操作语义集中证明搜索的逻辑集束的影响。
2021-01-26 cs.LO
A Vernacular for Coherent Logic
我们提出了一个简单的，但表现力的证明表示，从不同的证明助手证明可以很容易地生成。该表示法只使用了少量的推理规则，并且基于一阶逻辑的一个片段，称为相干逻辑。融贯逻辑已经被许多研究者认为是一种适用于许多日常数学发展的逻辑。建议的证明表示是伴随着相应的XML格式和一套XSL转换生成正式的证明Isabelle/Isar和Coq，以及证明表示在一个自然语言的形式（在LATEX或HTML格式）。此外，我们的自动定理证明器的连贯逻辑出口证明建议的XML格式。所有的工具都是公开的，还有一组样本定理。
2014-05-14 cs.LO
Infinitary and Cyclic Proof Systems for Transitive Closure Logic
传递闭包逻辑是通过引入传递闭包算子而获得的一阶逻辑的已知扩展。虽然其他具有归纳定义的一阶逻辑的扩展是由一组归纳定义先验参数化的，但传递闭包算子的添加一致地捕获了所有有限归纳定义。在本文中，我们提出了一个无穷证明系统的传递闭包逻辑，这是一个无限下降式对应的现有（显式归纳）证明系统的逻辑。我们表明，作为一阶逻辑与归纳定义的类似系统，我们的无穷系统是完整的标准语义和包含显式系统。此外，传递闭包算子的一致性允许使用简单的语法标准来定义语义上有意义的完整限制。因此，对规则无穷（即循环）证明的限制为自动化归纳推理的有效系统提供了基础。
2018-06-28 cs.LO
Birkhoff style proof systems for hybrid-dynamic quantum logic
本研究基于混合与动态模态逻辑构建量子逻辑框架，提出量子子句概念及对应推理证明规则，验证了其可靠性与紧致性，并证明了该逻辑片段的Birkhoff完备性，为量子逻辑编程与形式规约提供理论支撑。
2024-06-19 cs.LO
Logical Pseudocode: Connecting Algorithms with Proofs
证明（微积分，自然演绎）和命令式算法（伪码）是两个众所周知的共存概念。那他们是什么关系？我们的答案是，\[ imperative\ algorithms\ =\ proofs\ with\ cuts \]这一观察导致一个推广的伪码，我们称之为{ \it逻辑伪码}。它类似于可计算性逻辑\cite{Jap03,Jap08}的自然演绎证明。其中的每一个陈述都对应于自然演绎中的一个证明步骤。因此，相对于伪代码，它的优点是保证每个语句相对于初始规范是正确和安全的。它也可以被看作是可计算性逻辑网（\colw）的扩展，具有正向推理能力。
2022-02-14 cs.LO
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
2000-06-05 cs.LO
Interpreting a Classical Geometric Proof with Interactive Realizability
我们展示了如何提取一个单调的学习算法从一个经典的几何语句的证明，通过解释的证明，通过交互式可实现性，可实现语义的经典逻辑。该陈述是关于包含实平面中的有限点集的凸角的存在性，并且它与凸包的存在性有关。我们将实数定义为有理数的柯西序列，因此等式和排序是不可判定的。虽然证明表面上看起来是建设性的，但它使用经典推理来处理实数之间的不可判定比较，使得底层算法无效。交互式可实现性解释将证明所描述的非有效线性算法转换为使用回溯从错误中学习的有效算法。有效的算法表现出“智能”的行为，只执行证明最终语句所需的精度的比较。这种行为并没有明确的计划，但产生于柯西序列之间的比较的交互式解释。
2013-09-05 cs.CG cs.LO
A Witness Extraction Technique by Proof Normalization Based on Interactive Realizability
我们提出了一套新的减少自然演绎推导，可以提取证人从封闭的推导简单的存在公式在海廷算术（HA）加上排除中间法限制简单的存在公式（EM 1），一个系统的动机是其利益证明挖掘。我们对经典逻辑的归约与所有现有的归约都大不相同。他们的灵感来自于通过提出可证伪的假设并检验它们来学习的非正式思想，以及交互式的可实现性解释。我们提取证人直接从推导HA+ EM 1减少，没有编码推导的可实现性解释。
2013-05-15 cs.LO math.LO
Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic
在这篇文章中，我们将展示如何在最小蕴涵逻辑中证明超多项式大小的任何公式A在经典蕴涵命题逻辑中具有多项式大小的证明。这一事实提供了一个支持任何经典命题重言式都有简短证明的论点，即，NP = CoNP。
2015-08-13 cs.CC cs.LO
Proof systems for partial incorrectness logic (partial reverse Hoare logic)
本文为部分不正确性逻辑（部分反向霍尔逻辑）定义了普通和循环两种证明系统，证明其可靠且相对完备，并通过循环不变式及循环证明转化方法完成完备性证明。
2025-02-28 cs.LO cs.PL
