Designing a Safe Forward Chaining Tactic Using Productive Proofs

Kaustuv Chaudhuri

doi:10.1007/978-3-032-06085-3_16

2026-01-01

Kaustuv Chaudhuri *

Arunava Gantait

Dale Miller

DOI：10.1007/978-3-032-06085-3_16

原文链接

查看原文

摘要

En 中文

我们提出了一种在具有等式的一阶直觉主义多排序逻辑中，对正向链和饱和进行的证明理论处理。极性和聚焦证明的概念是我们方法的核心，因为它们为几何蕴含作为双极公式提供了表征，同时也为描述正向链和有效证明的概念提供了自然设置。我们确定了在给定公式集下，正向链保证在有限步内达到饱和的条件。这项研究的动机部分源于探索自动化Abella定理证明器的途径，该证明器依赖于关系规范，并且典型证明开发中的定理本质上就是双极公式。我们通过展示计算同余闭包和协助其他等式及关系推理任务的示例，来说明自动化正向链和饱和对Abella的潜在益处。

Keyword:

SEQUENT CALCULI

CUT-ELIMINATION

SYSTEM