当Agda遇见Vampire

AI总结：

通过集成Agda与Vampire实现自动化证明，提升构造性类型理论的自动化能力

摘要：

依赖类型证明助手为机械数学和验证软件提供了表达性基础。然而，这些系统的自动化程度要么范围有限，要么实现复杂。我们旨在通过以简单的方式将证明助手与自动定理证明器（ATPs）集成，来改善这一状况，同时保持前者的正确性保证。一个核心困难在于大多数ATPs操作在经典一阶逻辑中，而这些证明助手则基于构造性依赖类型理论。我们识别出两种语言的表达式片段——本质上是等式Horn——这允许在两个方向上都具有声音且直接的翻译。该方法产生了一个原型系统，用于将Agda的证明义务转发给ATP Vampire，然后将结果的古典证明转换为Agda可以类型检查的构造性证明项。原型自动推导了关于一个复杂字段及其根的性质的证明，这需要专业Agda开发者花费整整两天时间完成。所需工程努力相当有限，我们预计该方法将能够轻松扩展到其他ATPs和证明助手。

英文摘要：

Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the situation by integrating proof assistants with automated theorem provers (ATPs) in a simple way, while preserving the correctness guarantees of the former. A central difficulty arises from the fact that most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory. We identify an expressive fragment of both languages -- essentially equational Horn -- that admits sound, straightforward translations in both directions. The approach produces a prototype system for Agda forwarding proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check. The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity, which took professional Agda developers two full days to complete. The required engineering effort is modest, and we anticipate that the methodology will extend readily to other ATPs and proof assistants.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。