将阿格达与自动定理证明器结合，自动生成可验证的构造性证明。
When Agda met Vampire
- 在依赖类型与一阶逻辑间建立可逆翻译桥梁，实现双向通信。
- 自动推导出复数域单位根性质的证明，耗时仅数分钟而非两天。
- 方法简洁可复用，适合希望提升证明自动化水平的研究者。
依赖类型化证明助手为机械化数学和可信软件提供了强大基础，但其自动化能力要么范围有限，要么实现复杂。本文旨在通过简单方式将证明助手与自动定理证明器（ATP）集成，同时保持前者的正确性保证。核心难点在于多数ATP基于经典一阶逻辑，而证明助手基于构造性依赖类型理论。我们识别出两类语言中一个表达力强的公共子集——本质上为等式霍恩子句，支持双向且无损的翻译。该方法实现了一个阿格达原型系统，能将证明需求转发给ATP Vampire，再将生成的经典证明转换为阿格达可类型检查的构造性证明项。原型成功自动推导出关于带单位根的复数域性质的证明，此前需专业开发者耗时整整两天完成。工程实现工作量小，预计该方法可轻松扩展至其他ATP与证明助手。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。