Abella证明助手中加强引理证明的自动化
Automating the Proofs of Strengthening Lemmas in the Abella Proof Assistant
摘要：
在逻辑推理中，往往只需要一系列假设中的一些就可以得出结论。加强引理是一个断言，即一个给定的结论在这个意义上是独立于一个特定的假设。强化引理是自动和交互式定理证明器中简化证明的许多有用技术的基础。例如，它们是一种称为从属的机制的基础，这种机制在确定特定类型的表达式不能包含另一种类型的对象时很有用，从而减少了在证明普遍量化陈述时需要考虑的情况。本文研究了遗传Harrop公式逻辑（HOHH）中加强引理证明的自动化问题。Abella证明助手嵌入了这种逻辑，使其能够证明逻辑本身和其中所写的规范的属性。以前的研究已经阐明了一个（保守）算法，用于检查声称的加强引理是否为真。我们在这里提供了一个实现该算法内的设置Abella。此外，我们展示了如何生成一个实际的证明，加强引理在阿贝拉从算法计算的信息，这样的证明作为一个更值得信赖的证书的正确性的引理比算法本身。这项工作的结果已被纳入阿贝拉系统的形式，可以调用的互动定理证明，并将导致在一个详细的证明引理和其纳入收集的事实证明一个给定的规范的“战术命令”。
英文摘要：
In logical reasoning, it is often the case that only some of a collection of assumptions are needed to reach a conclusion. A strengthening lemma is an assertion that a given conclusion is independent in this sense of a particular assumption. Strengthening lemmas underlie many useful techniques for simplifying proofs in automated and interactive theorem-provers. For example, they underlie a mechanism called subordination that is useful in determining that expressions of a particular type cannot contain objects of another type and in thereby reducing the number of cases to be considered in proving universally quantified statements. This thesis concerns the automation of the proofs of strengthening lemmas in a specification logic called the logic of hereditary Harrop formulas (HOHH). The Abella Proof Assistant embeds this logic in a way that allows it to prove properties of both the logic itself and of specifications written in it. Previous research has articulated a (conservative) algorithm for checking if a claimed strengthening lemma is, in fact, true. We provide here an implementation of this algorithm within the setting of Abella. Moreover, we show how to generate an actual proof of the strengthening lemma in Abella from the information computed by the algorithm; such a proof serves as a more trustworthy certificate of the correctness of the lemma than the algorithm itself. The results of this work have been incorporated into the Abella system in the form of a "tactic command" that can be invoked within the interactive theorem-prover and that will result in an elaboration of a proof of the lemma and its incorporation into the collection of proven facts about a given specification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
