Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

When Agda met Vampire

Artjoms Šinkarovs, Michael Rawson

TL;DR

This work 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, and expects that the methodology will extend readily to other ATPs and proof assistants.

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 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.

When Agda met Vampire

TL;DR

This work 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, and expects that the methodology will extend readily to other ATPs and proof assistants.

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 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.
Paper Structure (17 sections, 1 theorem, 3 equations)

This paper contains 17 sections, 1 theorem, 3 equations.

Table of Contents

  1. Introduction
  2. Background
  3. Horn Logic and Notation
  4. The Agda Proof Assistant
  5. The Vampire Automated Theorem Prover
  6. Method
  7. Translating Agda Terms to Horn Clauses
  8. Invoking Vampire
  9. Transforming the Proof
  10. On Friedman
  11. Translating the Proof to Agda
  12. Implementation via Prolog
  13. Edge Cases and Other Inferences
  14. Case Study
  15. Discussion and Future Work
  16. ...and 2 more sections

Key Result

lemma 1

For any inference of the Horn superposition calculus with a premise of the form $C \to \bot$, the conclusion is of the form $D \to \bot$. Furthermore, a difference instance of the same rule concludes $D \to G$ from $C \to G$ for any ground atom $G$.

Theorems & Definitions (2)

  • lemma 1: agnostic
  • proof