Abella证明助手的图式多态性
Schematic Polymorphism in the Abella Proof Assistant
摘要：
Abella交互式定理证明器已被证明是推理关系规范的有效工具。然而，该系统有一个局限性，这是由于它是基于简单类型化逻辑的事实：除了应用于不同类型的形式化之外，其他形式化都是相同的，必须在每个类型上重复。我们开发了一种方法，克服了这一限制，同时保留系统的逻辑基础。在这种方法中，对象构造函数、公式和其他相关的逻辑概念被允许通过类型参数化，解释为它们代表通过实例化类型参数获得的相应构造的（无限）集合。我们考虑的公式的证明结构，以这种方式被模式化的限制，其类型实例是有效的证明在简单类型逻辑。我们开发的示意性证明规则，确保这一属性，一个任务，是复杂的事实，类型信息影响的概念，在逻辑中起着关键作用的统一。我们的想法，这已经实现了系统的更新版本，容纳示意图多态性的核心逻辑Abella和可执行的规范逻辑，它嵌入。
英文摘要：
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism both in the core logic of Abella and in the executable specification logic that it embeds.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
