When Agda met Vampire
Artjoms \v{S}inkarovs, Michael Rawson

TL;DR
This paper presents a method to integrate Agda with the ATP Vampire by translating between constructive and classical logic, enabling automated proofs while maintaining correctness guarantees.
Contribution
It introduces an expressive fragment for sound translation between Agda and Vampire, creating a prototype system that automates proof obligations in dependent type theory.
Findings
Automated proofs were generated for complex algebraic properties.
The approach simplifies proof automation in dependently-typed systems.
The prototype required modest engineering effort.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Model-Driven Software Engineering Techniques
