Paper deep dive

When Agda met Vampire

Artjoms Šinkarovs, Michael Rawson

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 68

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%

Last extracted: 7/20/2026, 9:14:03 PM

Summary

The paper presents a lightweight integration method for the dependently-typed proof assistant Agda and the automated theorem prover Vampire. By identifying a common expressive fragment (essentially equational Horn logic), the system translates Agda proof obligations into Vampire's first-order logic, solves them, and reconstructs the classical proof into a constructive Agda proof term for type-checking. This approach automates complex proofs, such as those involving roots of unity, significantly reducing manual effort.

Entities (6)

Agda · software · 98%Vampire · software · 98%Horn Logic · concept · 92%Curry-Howard Correspondence · concept · 90%Roots of Unity · mathematicalconcept · 88%Superposition Calculus · algorithm · 85%

Relation Signals (6)

Agda → integrateswith → Vampire

confidence 98% · We integrate Agda ... with Vampire

Vampire → implements → Superposition Calculus

confidence 95% · Vampire implements the superposition calculus

Agda → uses → Curry-Howard Correspondence

confidence 95% · Agda is founded on intuitionistic type theory... Under the Curry–Howard correspondence one may view Tree as a primitive proposition

Agda → translatesto → Horn Logic

confidence 90% · We identify an expressive fragment of both languages -- essentially equational Horn

Vampire → translatesto → Horn Logic

confidence 90% · We identify an expressive fragment of both languages -- essentially equational Horn

Prototype System → solves → Roots of Unity

confidence 85% · The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

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.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

66,950 characters extracted from source content.

Expand or collapse full text

When Agda met Vampire Artjoms Šinkarovs# Electronics and Computer Science, University of Southampton, UK Michael Rawson# Electronics and Computer Science, University of Southampton, UK 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. 2012 ACM Subject Classification Replace ccsdesc macro with valid one Keywords and phrases dependent type theory, constructive logic, automated theorem proving, first-order logic, Agda, Vampire Funding Artjoms Šinkarovs: [funding] Michael Rawson: [funding] Acknowledgements We would like to thank Mario Carneiro for introducing us to the proof-transform technique used here. 1 Introduction Dependently typed proof assistants such as Lean, Agda and Rocq are powerful environments for correct-by-construction programming and formal theorem proving. Thanks to the Curry–Howard correspondence, program invariants or theorems are expressed as types, and correctness follows once the corresponding specification type-checks. This approach does not depend on untrusted components such as SAT/SMT solvers, but it also places a substantial burden on the developer: non-trivial proof obligations frequently arise and must be discharged. In practice many of these obligations are routine rather than mathematically deep — for example, proving that two constructions in a particular encoding are isomorphic or share a simple property — yet they are nevertheless labour-intensive. Consequently, effective proof automation is essential for the practical adoption of dependently-typed systems. Proof automation in interactive theorem provers (ITPs) is a longstanding and difficult research problem. Most proof assistants provide tactic languages to automate some work, but designing efficient proof-search strategies for a given theory remains hard. Naïve brute-force search succeeds only in the simplest cases; more capable methods lead naturally to Automatic Theorem Provers (ATPs). At that juncture an ITP faces a choice: rely on external ATPs — which raises compatibility and trust issues — or implement proof search procedures inside the ITP. Typical internal procedures are significantly weaker than the state of the art in ATP. Practical “hammer” systems such as Isabelle’s Sledgehammer or CoqHammer use an external arXiv:2602.18844v1 [cs.LO] 21 Feb 2026 2When Agda met Vampire ATP to find an initial proof, then use that proof as a “hint” to reconstruct another proof using internal certified procedures. The hint could be merely the premises required to prove a goal, or using intermediate steps from the untrusted proof. Sledgehammer works particularly well because the internal prover metis is relatively strong, and because Isabelle/HOL’s logic is similar to that of ATPs. Dependently-typed systems do not enjoy these advantages. Here we pursue a deliberately lightweight variant of this approach, playing to the strengths of existing systems. We identify a useful fragment of a dependently-typed language that can be translated straightforwardly to an ATP and vice-versa, and produce a concise, verifiable round-trip translation: (i) translate a goal and the necessary lemmas into the ATP; (i) invoke the ATP to search for a proof; (i) reconstruct the ATP proof as an ITP proof term; (iv) typecheck the reconstructed term. By confining the translation to a well-chosen fragment, we avoid intrusive changes to either system while still enabling substantial automation. Proof re-construction also becomes substantially easier: if a proof is found by the external ATP, it is almost always reconstructed. Concretely, we integrate Agda — based on Martin-Löf type theory — with Vampire, a leading ATP and multi-time winner of CADE ATP System Competition (CASC). We use Agda’s reflection facilities to extract the current goal and environment and to emit Vampire problems. This reflection-based technique does not require any changes to Agda. Vampire’s proof output, when successful, is translated back into Agda using a compact reconstruction engine implemented in Prolog: Prolog’s native search facilities map naturally to the reconstruction task. The resulting proof term is then certified by Agda’s typechecker. A central claim of this work is that such lightweight integration — applying each tool for what it already does best — demands minimal implementation effort and maintenance compared with deep, invasive integration. Our prototype implementation is already practical: we used it to discharge properties of a representation of the complex field with roots of unity that arose in a real research project. What previously required an Agda specialist around two full days is produced automatically. The remainder of the paper describes the translated fragment, translation and reconstruction, implementation details, and a case study. 2 Background We assume passing familiarity with classical first-order logic and with dependently-typed interactive theorem proving. There is a well-known correspondence [44] between logic and type systems, often under the slogan propositions as types. The gist is that logical propositions Pcorrespond to typesτ, and that proofs ofPcorrespond to terms inhabitingτ. This is the conceit of type-theoretic proof assistants like Agda: with a sufficiently expressive type system, one can prove non-trivial propositions by producing a term which inhabits a type. Such systems exploit the propositions-as-types correspondence in one direction. We will need to traverse both directions for the integration we seek. One could be forgiven for thinking that the correspondence is tighter than it is: that there is no real difference between logic and type systems. Unfortunately for us, there are real technical and cultural differences, which are usually poorly understood by specialists in either world. The best-known difference is a cultural preference for constructivism in type-theoretic systems, whereas logical proof asssistants and ATPs are more often classical. Less well-understood in our experience is that logical systems — including Vampire — draw a distinction between terms and formulae. Terms are inhabitants of the domain of discourse, which are implicitly assumed to be non-empty: this renders questions about whether a type is inhabited uninteresting, as all types are inhabited. Deduction instead A. Šinkarovs and M. Rawson3 happens by deriving new formulae from old using the logic of the system. Perhaps confusingly, terms can be Boolean [26]. On the other hand, type-theoretic systems often make no such distinction: there are simply terms, stratified by the has-type relationt:τ. Our task here is to reconcile the type system of Agda and the logic of Vampire: we will now describe both, after introducing some notation. 2.1 Horn Logic and Notation We will make use of the Horn fragment of first-order logic, which we now briefly recall. An atomP(t 1 ,...,t n ) is a predicatePapplied to termst i , and a literalLis either an atomAor its negation¬A. Equationss=tare merely a special atom with two arguments. A first-order clause is a universally-quantified disjunction of literals, from which we will usually elide the quantifiers. A Horn clause is a clause with no more than one positive “head” literal. We distinguish between definite clauses with exactly one positive literal, and goal clauses with no positive literals. A definite clause can be written as an implicationP 1 ∧...∧P n → Q, where eachP i andQare atoms. Naturally, a goal clause can then be writtenP 1 ∧ ...∧ P n →⊥, although it is really the clause¬P 1 ∨ ...∨¬P n . The empty clause⊥is also a goal clause, with ⊥ for the head and an empty body. When writing inference rules, we will use the lettersCandDto indicate part of a (Horn) clause, which may be empty. Two clauses which participate in an inference are assumed to have their variables renamed apart from each other. We will also assume that literals in a (Horn) clause may be re-ordered in order to apply an inference rule, as is common implicit practice. Equally, equationss=tare treated as implicitly symmetric. We writes[t] to indicate that t is a subterm of s: this includes the case where s is t. We say that a first-order term (literal, clause) is ground if it contains no variables. A substitutionσis a map from variables to terms: when applied to a term (literal, clause) it acts to replace every variablexin that term withσ(x). Clearly, then,σ(t) =twhen tis ground. A substitution is a unifier forsandtwhenσ(s) =σ(t), and it is the most general unifier when it cannot be expressed as the composition of a unifier and a non-empty substitution. Most general unifiers can be computed with a unification algorithm. 2.2 The Agda Proof Assistant Agda is both a dependently typed functional programming language and a proof assistant, offering an interactive environment for writing and checking formal proofs. It provides inductive families, analogous to Haskell’s GADTs, but with indices that may be values as well as types. The system is founded on intuitionistic type theory, a framework for constructive mathematics developed by Per Martin-Löf. It shares many characteristics with other dependently typed proof assistants such as Rocq, Idris and Lean. The following is a concise overview of the constructs necessary for the remainder of the paper; accessible introductions are available online. 1 We begin with a simple algebraic data type: binary trees, Tree, with two constructors. leaf takes no arguments, while node takes two arguments, both of type Tree. Functions on 1 See https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html. 4When Agda met Vampire such data types are typically defined by recursion and pattern matching; for example: data Tree : Set where leaf : Tree node : Tree→ Tree→ Tree size : Tree→ N size leaf= 1 size (node l r) = 1 + size l + size r Under the Curry–Howard correspondence one may view Tree as a primitive proposition whose values are its proofs; in our translation, however, such simple data types will correspond to terms rather than to logical propositions. The key feature of Agda is dependent types. The following Path type is indexed by a Tree and represents all valid paths in the given tree: data Path : Tree→ Set where done : ∀ t→ Path t left : ∀ l r→ Path l→ Path (node l r) right : ∀ l r→ Path r→ Path (node l r) length : ∀ t→ Path t→ N length done = 0 length (left p) = 1 + length p length (right p) = 1 + length p Path has three constructors that constrain the shape of its index: done, which signals termination at the tree t; and left and right, which descend into the left or right subtree respectively, when such subtrees exist. The quantifier∀allows omission of explicit types for the quantified variables; arguments in braces are implicit and are not supplied during application or pattern matching. The dependent function length computes over Path values in the same manner as over ordinary algebraic data types. Under Curry–Howard, dependent types such as Path correspond to predicates: the predicate holds precisely when the corresponding type is inhabited. A noteworthy distinction is that some Agda predicates are proof-relevant (they may have many distinct inhabitants), whereas logical propositions are typically proof-irrelevant. Consequently, types like Path admit multiple inhabitants that a function such as length may distinguish; this behaviour has no exact analogue in traditional predicate logic. When a predicate is propositional (that is, it has at most one inhabitant), the logical proof and the Agda programme are interchangeable. We confine our attention in this work to such propositions. As an example, consider IsEven and propositional equality: data IsEven : N→ Set where zero : IsEven 0 suc : ∀ n→ IsEven n→ IsEven (2 + n) data _≡_ A : Set (x : A) : A→ Set where refl : x ≡ x The type _≡_ asserts that two terms are equal when they reduce to the same normal form; we translate this type as logical equality. Finally, Agda provides a reflection mechanism, which yields a syntactic representation (an abstract syntax tree) of internal terms — a facility analogous to quotation in Lisp. Reflection was introduced to support proof automation. Since Agda lacks a separate tactic language, as found in Rocq or Lean, reflection permits tactics to be implemented directly in Agda. One can quote a term to obtain its AST, manipulate the AST as required, and then unquote the AST to produce an Agda term; the ensuing unquotation invokes type checking, thereby ensuring that only well-typed terms are constructed. The sequel illustrates how reflection is used to construct a function foo from an AST so that it coincides exactly with a specified reference definition foo’. pattern ‘N = def (quote N) [] pattern ‘zero = con (quote zero) [] pattern ‘suc x= con (quote suc) (vArg x :: []) pattern _‘+_ x y = def (quote _+_) (vArg x :: vArg y :: []) A. Šinkarovs and M. Rawson5 We first define four patterns, which resemble function definitions but may be used within pattern-matching expressions, and then use them to construct the AST shown below: foo : N→ N unquoteDef foo = defineFun foo ( clause [] (vArg ‘zero :: []) ‘zero :: clause (("x" , vArg ‘N) :: []) (vArg (‘suc (var 0)) :: []) (var 0 [] ‘+ var 0 []) :: [] ) foo’ : N→ N foo’ zero = zero foo’ (suc x) = x + x 2.3 The Vampire Automated Theorem Prover Vampire [28,5] is a successful automated theorem prover for classical first-order logic with equality. It also has extensions for reasoning about fixed pre-defined theories (such as arithmetic [25]) and for higher-order logic [8], but we use only the first-order core and support for inductively-defined data [27] here. We chose Vampire because it is empirically very successful, and because one author was familiar with its behaviour, but we expect that this work could be profitably transplanted on to another ATP system that uses a similar calculus, including E [35], Zipperposition [43], or iProver [24]. Unit equational systems like Twee [37] or Waldmeister [30] could also be employed by translating Horn clauses [13]. Different systems will have complementary strengths. Vampire also has potential for further extensions (Section 5), improving its ability to dispatch Agda goals. Given the audience, we would like to make a few clarifications about Vampire and systems like it: Fully automatic.Vampire is a completely automatic push-button system that requires no interaction from the user. Given an input, it terminates only to report that the input is a theorem or non-theorem 2 , or if a user-specified resource bound is exceeded. No magic.The validity of a statement in first-order logic is undecidable in theory and hard in practice. Vampire is very good at proving theorems and can even disprove some non-theorems, but still may not terminate in reasonable time. Classical first-order logic.Vampire is a classical system. The law of the excluded middle and other dicta of classical logic — such as the non-emptiness of domains — are baked very deeply into the system and cannot be disabled. Similarly, Vampire draws a hard line between terms, which are spoken about, and formulae, which do the speaking. Trust.Vampire has no proof terms, kernel, or similar safety mechanism, and its proofs are simply a series of steps in its internal calculus that should be treated as untrusted. Vampire, like other saturation-based ATPs, works by refutation. Given an input containing axioms and a conjecture, the conjecture is negated and added to the axioms to form an input set of formulae. These formulae are then preprocessed into clause normal form (CNF), a set of clauses. Search now begins: Vampire applies the inference rules of its calculus to derive more and more consequences of the clauses, working fairly so that a proof — if it exists — will eventually be found. When Vampire derives the empty clause (falsum), it has refuted the negation of the input conjecture. Classically, this is the same as proving the conjecture. Vampire implements the superposition calculus [31], a complete calculus for classical first-order logic with special treatment for the equality predicate. For the sake of efficiency the calculus has many restrictions on rules, but for our purposes this can be ignored. The 2 in some (incomplete) configurations, Vampire may also give up 6When Agda met Vampire relevant inference rules are as follows: L∨ C ¬L ′ ∨ D σ(C∨ D) Resolution L∨ L ′ ∨ C σ(L∨ C) Factoring l = r∨ C L[l ′ ]∨ D σ(L[r]∨ C∨ D) Superposition s̸= t∨ C σ(C) Equality Resolution where the substitutionσis the most general unifier ofLandL ′ in Resolution and Factoring; l and l ′ in Superposition; and s, t in Equality Resolution. To build intuition for these rules, it is helpful to imagine that the unified terms and literals are already identical in the premises. Resolution can then be seen as case analysis on the BooleanL, Factoring as an application of the identity (p∨ p)≡ p, Superposition as conditional rewriting, and Equality Resolution as removing an obviously-false literal t̸=tfrom a clause. The full version of each rule can be seen as first (partially) instantiating universal quantifiers according to σ, then applying the rule without unification. ▶Example 1 (resolution). The following concrete inference is an instance of the resolution rule. The most general unifier of P (x,f (y)) and P (c,z)) is x7→ c, z 7→ f (y). P (x,f (y))∨ Q(y) ¬P (c,z)∨¬R(z) Q(y)∨¬R(f (y)) Resolution There are many other rules which we deal with later (Section 3.4.2), but the above four rules form the core first-order reasoning of Vampire. Vampire also has a type system [9,7] for terms: it is essentially System F restricted to rank-1 types. 3 Method Using Vampire to dispatch Agda goals does not seem to be workable at first sight. Vampire cannot process everything in Agda’s vocabulary, and Agda will not accept Vampire’s classical proofs, even if we get one. Agda also lacks the automation required to do Sledgehammer- style proof reconstruction [32] from a set of premises minimised by Vampire. However, by restricting both systems to a common language, we can give Agda goals directly to Vampire and translate Vampire’s proofs directly to an Agda proof term. Observation. Many useful Agda premises and goals are of the form ∀ ̄x. R 1 → R 2 → ...→ R n where every R i is an atomic type. This corresponds to the Horn fragment of FOL. There are more details involved in translating an Agda goal into Horn logic (Section 3.1), but suppose for now that we have a set of definite clauses Γ and a ground “goal” atomG, and we wish to show Γ⊢ G. Assuming that this is provable, and that Vampire manages to prove it, we obtain a classical proof by refutation showing Γ,¬G⊢⊥. But we would simply like Γ⊢ G, with no extra negations. This leads us to another observation. Observation. Vampire’s inference rules conclude Horn clauses if the premises are also Horn. Furthermore, Vampire’s Horn proofs remain valid if goal clausesC →⊥ are systematically replaced with C → G, for some ground G. A. Šinkarovs and M. Rawson7 This allows us to transform the proof mechanically, replacing occurrences of⊥withG. The result is a classical proof showing Γ,(G→ G)⊢ G, butG→ Gis trivial and we obtain Γ⊢ G immediately. But we still require a constructive proof. Observation. Vampire’s core calculus is constructively valid. The classical aspects of Vampire are confined to the normal form translation (which may e.g. perform double-negation elimination), and the principle of proof by refutation. Overall, this means that an Agda holeGin context Γ can be translated into an input that Vampire can attempt (Section 3.1), and the resulting proof can be transformed (Section 3.3) into a constructive proof of Γ⊢ Gas Agda terms (Section 3.4), automatically filling the hole. We will now be precise about the details of this round-trip. 3.1 Translating Agda Terms to Horn Clauses The translation of Agda formulae proceeds in three conceptual stages: (i) reflecting the user-defined definitions; (i) checking that these definitions lie within the supported language fragment; and (i) converting the reflected terms to an input language Vampire supports. We chose SMT-LIB [4] as it can express datatypes. Unlike the strict fragment characterisation employed by Foster and Struth [18], we prioritise ease of use. Consequently we rely on Agda’s reflection facilities rather than on labour-intensive manual encodings. This apparent laxity is justified as the overall process of finding a valid proof may fail. There is no guarantee that the back-end ATP will discover a proof; even if a proof is found, the translated proof may be unsound, which is why the imported proof must be type-checked. Moreover, as our integration evolves, this modular approach facilitates experimentation with new features. Reflection We provide a collection of macros that accept the name of an Agda definition quote the term and emit an SMT-LIB representation. In particular: kty declares a new sort to Vampire. kdata translates an inductive algebraic data type (without parameters or indices) into a built-in datatype declaration, handling constructors and ensuring well-foundedness, thereby enabling inductive reasoning. kfunconverts functions given by pattern-matching equations into a function symbol with the appropriate type signature, together with clauses that become axioms. To illustrate, consider addition on Peano-encoded natural numbers: data Nat : Set where – (declare-datatype nat ze : Nat – ((ze) su : (n : Nat)→ Nat – (su (n nat)))) add : Nat→ Nat→ Nat – (declare-fun add (nat nat) nat) add ze x = x – (assert (! (forall ((x nat)) – (= (add ze x) x)) :named add-clause-1)) add (su x) y = su (add x y) – (assert (! (forall ((x nat)(y nat)) – (= (add (su x) y) (su (add x y)))) – :named add-clause-2)) 8When Agda met Vampire Stated theorems (e.g. some facts about natural numbers) can be turned into an axiom using the kthm macro; this simply translates the type into an assertion. Note that we do not verify the existence of a proof — we only inspect the type. Finally, the kgoal macro is used to translate goals that we wish to prove. Conformity checks The macros above impose several constraints on the shape of the supplied datatypes and functions. If these constraints are violated, the translation aborts with an error. Specifically: For inductively defined datatypes, parameters or indices are not permitted. Although Vampire offers limited support for parametrised types such as polymorphic lists, we currently do not handle them. For functions we demand arguments of simple, non-dependent types, thereby forbiding dependent functions. For theorems we enforce that the overall type resides in the Horn fragment. Consequently, the type may contain a mixture of named arguments of simple datatypes and propositional components that reference variables of simple types, while the right-hand side must be a proposition. At present the only supported proposition is propositional equality 3 , which implicitly means that we assume Uniqueness of Identity Proofs (UIP) in Agda. Goals, like theorems, must be in Horn form. During translation we convert all premises of the goal into named constants and negate the right-hand side using assert-not 4 . Translation We define a type to represent a subset of SMT-LIB programs. Macros tranlsate turn into the element of this type which is subsequently rendered as a string. This string is fed to Vampire; the resulting proof is processed by the proof-converter described in Section 3.4 and finally emitted as Agda code. Example To demonstrate the workflow, we consider a rudimentary theory of vector spaces comprising a zero vector ze, addition _+_, and negation -_, together with three axioms: associativity of addition, left-hand neutrality of zero, and left-hand inverse for addition: V : Set ze : V _+_ : V→ V→ V -_ : V→ V assoc : ∀ u v w→ (u + v) + w ≡ u + (v + w) neutl : ∀ u→ ze + u ≡ u negl : ∀ u→ (- u) + u ≡ ze These declarations suffice to state the uniqueness of the zero vector, expressed by the following theorem (the proof will be obtained from Vampire): ze-uniq : ∀ u v→ (e : u + v ≡ v)→ u ≡ ze To obtain the goal we first extract the type V, the types of the functions _+_, -_ and the constant ze (treated as a nullary function). We then supply the three axioms and finally 3 although Vampire and the proof conversion can handle arbitrary relations 4 (assert-not F)is a Vampiric extension with the same semantics as(assert (not F)), but with the additional effect of marking F as a goal for Vampire’s internal heuristics A. Šinkarovs and M. Rawson9 specify the goal to be proved. As can be seen, only the names of the definitions need to be provided; the rest of the conversion is performed automatically by the reflection machinery: ze-uniq-v : String ze-uniq-v = print-prog (kty V :: kfun-ty _+_ :: kfun-ty -_ :: kfun-ty ze :: kthm neutl :: kthm negl :: kthm assoc :: kgoal ze-uniq :: []) Evaluating ze-uniq-v yields the following SMT-LIB: (declare-sort vec.V 0) (declare-fun vec._+_ (vec.V vec.V) vec.V) (declare-fun vec.-_ (vec.V) vec.V) (declare-const vec.ze vec.V) (assert (! (forall ((u vec.V)) (= (vec._+_ (vec.ze ) u) u)) :named vec.neutl)) (assert (! (forall ((u vec.V)) (= (vec._+_ (vec.-_ u) u) (vec.ze ))) :named vec.negl)) (assert (! (forall ((u vec.V) (v vec.V) (w vec.V)) (= (vec._+_ (vec._+_ u v) w) (vec._+_ u (vec._+_ v w)))) :named vec.assoc)) (declare-const u vec.V) (declare-const v vec.V) (assert (! (forall () (= (vec._+_ u v) v)) :named e)) (assert-not (! (= u (vec.ze )) :named vec.ze-uniq)) The required proof is non-trivial and is not discovered by Agda’s built-in automatic proof search. Vampire, however, finds a correct proof instantly. 3.2 Invoking Vampire We now have an SMT-LIB input that Vampire can attempt. Vampire, like most ATPs, works best if allowed to run a portfolio, trying many different strategies until one succeeds. A strategy is simply a collection of options for Vampire. The idea is that a single strategy is likely to find a proof quickly or not at all, so it is better to restart afresh regularly with a new strategy than continue to try hard for a long time. We found that the pre-baked CASC [38] portfolio was highly effective on the unseen 5 Agda problems. Portfolio modes also allow making full use of available parallelism by running multiple strategies simultaneously. However, running the CASC portfolio also exposes us to the full range of possible Vampire inferences, some of which can be very surprising. We have not implemented all of Vampire’s inferences for this prototype, but we have done enough such that all the proofs in Section 4 are found and reconstructed while using the portfolio. Vampire delivers the following proof for the SMT-LIB input above: 1. ∀x. 0 + x = x (neutl) 2. ∀x. 0 =−x + x (negl) 3. ∀xyz. (x + y) + z = x + (y + z) (assoc) 4. v = u + v (e) 5. 0̸= u (negated goal) 6. ∀xy. − x + (x + y) = 0 + y (superposition 3, 2) 7. ∀x. v + x = u + (v + x) (superposition 3, 4) 8. ∀xy. − x + (x + y) = y (superposition 6, 1) 9. ∀x. (− x) + 0 = x (superposition 8, 2) 5 this lends credence to the idea that the portfolio was adequately regularised during construction [6] 10When Agda met Vampire 10. ∀xy. y + x = (− y) + x (superposition 8, 8) 11. ∀x.x + 0 = x (superposition 9, 10) 12. ∀x. 0 = x +−x (superposition 2, 10) 13. 0 = u + 0 (superposition 7, 12) 14. 0 = u (superposition 13, 11) 15. ⊥ (resolution 14, 5) Note that the proof ends in⊥, and requires the negated goal as a premise. Vampire treats equations as symmetric, so superpositions may occur in either direction. 3.3 Transforming the Proof At this stage we we have a set of definite clauses Γ, a ground atomG, and a classical proof from Vampire purporting to show Γ⊢ G. Vampire will in fact show Γ,¬G ⊢ ⊥. The input set is already in CNF, so Vampire’s preprocessing rules do not apply and the proof of Γ,¬G⊢⊥will only involve rules of the superposition calculus given above 6 . Let us specialise Vampire’s superposition calculus to operate on Horn premises: Resolution C → P P ′ ∧ D → Q σ(C∧ D → Q) Factoring P ∧ P ′ ∧ C → Q σ(P ∧ C → Q) Equality Resolution s = t∧ C → P σ(C → P) Superposition Left C → l = r P [l ′ ]∧ D → Q σ(C∧ P [r]∧ D → Q) Superposition Right C → l = r D → P [l ′ ] σ(C∧ D → P [r]) whereσ=mgu(P,P ′ ) in Resolution and Factoring,mgu(l,l ′ ) in both Superposition variants, andmgu(s,t) in Equality Resolution. Each conclusion is Horn. It is not too hard to see that these rules are constructively valid, but we will show this definitively by giving a translation to Agda. Now consider theboxedatoms in the premises of some rules: these atoms could be⊥, i.e. when the premise is a goal clause. When the boxed atom is ground (including, but not limited to,⊥), each such rule simply duplicates the boxed atom in the conclusion. This is because substitution on ground atoms does nothing. ▶Lemma 2 (agnostic). For any inference of the Horn superposition calculus with a premise of the formC →⊥, the conclusion is of the formD →⊥. Furthermore, a difference instance of the same rule concludes D → G from C → G for any ground atom G. Proof. By case analysis on the rules of the calculus. ◀ Lemma 2 permits a very simple transformation of the proof. First, replace the root goal clauseG→⊥with the tautologyG→ G. Then, for any inference in the proof that has a goal clauseC →⊥as a premise, replace it withC → G. This will produce a conclusion of the formD → G. The final empty goal clause→ ⊥in the refutation will be transformed into a clause→ G, so we have Γ,(G→ G)⊢ G, from which we obtain Γ⊢ G. In the example above, step 5 is translated to 0 =u→0 =uand step 15 becomes 0 =u. This is a simple case, but in general ⊥ may be woven through the entire proof. 6 this is not quite true, but the details are not important here: more on this in Section 3.4.2 A. Šinkarovs and M. Rawson11 3.3.1 On Friedman This trick is similar to the technique used by Friedman [19] to show that any Π 0 2 sentence that is a theorem of Peano arithmetic is also a theorem of Heyting arithmetic. We follow Selinger’s presentation [36]. Friedman defines theA-translation of a formulaFto be the result of replacing any atomic formulaBwithinF(including⊥) withB∨ A, provided no free variable ofAis bound inF: this is shown to preserve validity in Heyting arithmetic. Π 0 2 sentences can be reduced to the form∃y. f(x,y) = 0 for some primitive recursivef: let us call thisφ. TheA-translation ofφis∃y.(f(x,y) = 0∨ A), which is equivalent to φ∨ A. Friedman first shows that if⊢ PA φ, then⊢ HA (φ → ⊥)→ ⊥. Then, withA=φ, A-translation yields ⊢ HA ((φ∨ φ)→ φ)→ φ and hence⊢ HA φ. Selinger states that as long as a theory can prove its own axioms in both double-negated andA-translated forms, Friedman’s argument will work. Our theory is not Heyting arithmetic, but the user-provided axioms. However, since for any Horn premise we can prove the double-negated form and theA-translation, we know that a proof of (G → ⊥)→ ⊥can be transformed into a proof ofG. The approach we employ is not precisely the same as Friedman’s, but we could certainly say it rhymes. 3.4 Translating the Proof to Agda We now need to translate any inference of the above Horn superposition calculus into an Agda proof term. This is neither difficult nor novel: a very similar translation is given in a slightly different context by Burel [10], although we do not have a doubly-negated representation. However, we sketch the scheme here in order to give the main idea. For the sake of clarity we present a ground calculus and leave it to the reader to insert the appropriate introduction and instantiation of variables. Corresponding with the Horn inference rules above: Resolution t 1 : C → P t 2 : P → D → Q (λcd. t 2 (t 1 c) d) : C → D → Q Factoring t : P → P → C → Q (λpc. t p p c) : P → C → Q Equality Factoring t : s = s→ C → P (λc. t refl c) : C → P Superposition Right t 1 : C → l = r t 2 : D → P [l] (λcd. rw (t 1 c) (t 2 d)) : C → D → P [r] Superposition Left t 1 : C → l = r t 2 : P [l]→ D → Q (λcpd. t 2 (rw (sym (t 1 c)) p) d) : C → P [r]→ D → Q whererw:l=r → P[l]→ P[r] is an appropriate Agda “rewrite” term for anyP,landr, and sym : l = r → r = l is a lemma showing symmetry of equality. 3.4.1 Implementation via Prolog Producing precise proof terms from ATP proofs is usually done by either modifying the ATP to output them directly [23], or by invoking a different, certificate-producing, ATP on each proof step, producing a certificate for that step [40]. Neither option was attractive for us. Modifying Vampire is a great deal of work, causing a (small but present) performance hit and producing a maintenance burden. Invoking a certifying ATP on proof steps is also considerable integration work, and occasionally the certifying ATP times out in hard-to-predict ways. 12When Agda met Vampire Instead, we exploit the fact that Vampire produces TSTP [39] proofs, which are valid Prolog [21] with some special operators defined. We implement the TSTP-Agda translation with a Prolog script. The script first reads the proof into an internal database usingread/1, recording the name (e.g.superposition) of inferences and their premises. At this stage, we ensure that clauses are Horn and replace any⊥withG, as above. Then, for each step in the proof, the script performs backtracking search for a valid e.g. superposition step that produces the correct conclusion given the premises, building an Agda proof term as it goes. The script handles Vampire’s idiosyncrasies, including variable renaming and implicitly treating equality as symmetric. On success, the proof term for the step is complete. We highly recommend this method for similar tasks. Many aspects which are painful with other methods, chiefly variable renaming, are non-problems here as Prolog already has the correct semantics. Backtracking search for valid inferences can be implemented concisely and declaratively: the entire Prolog script, including loading, reconstruction, printing, and several extensions, is achieved in less than 500 lines of inexpert code. In principle this search could result in combinatorial blowup, but this does not seem to be a problem in practice and was not seen during testing on the entire supported fragment of the TPTP [39] benchmark set. We think this improved behaviour is because the Prolog script knows it is looking for a single inference, whereas an external ATP does not. 3.4.2 Edge Cases and Other Inferences There is one final mismatch between Vampire’s logic and Agda’s: empty domains. In classical first-order logic, all domains are considered implicitly non-empty, so that∀x. P(x) and∀x.(P(x) =⇒ Q) entailQ. However, this does not always hold in Agda as the domain ofxmay have no inhabitants. When this situation occurs, the Prolog script looks around for bound variables or constants of the appropriate sort to show that the domain is inhabited. In the rare event that this still fails, a hole is left for the user to fill. Vampire also has more inferences than we admitted earlier: at the time of writing it has around 200 (!). This was not a concern in practice: many relate to inputs like arithmetic outside of the fragment we consider here; some relate to translation into clause normal form, unnecessary here; and some are special cases of the core calculus and can be dealt with as such. We must only handle the remainder, which turn out to be straightforward. Vampire likes to introduce and eliminate definitions for terms as it sees fit, and we must go along with it. Introducing definitions is easy, for they simply become Agda definitions. Eliminating definitions is more involved but is essentially equational reasoning of the same flavour as the superposition rule. Vampire also knows about the properties of inductively-defined datatypes, and will e.g. deducex=yandl=kfromx::l=y::k. This kind of reasoning turns out to be mechanical and easy to translate. In the end, we handle 21 named inferences. Some inferences will prove difficult to handle fully in this context, including those which escape the Horn fragment, introduce new symbols without an obvious definition, or perform a reduction to SAT [34]. If desired, it is possible to disable Vampire’s more flamboyant options in exchange for reduced proving power: we would recommend the command line flag --forced_options av=off:ins=0:gsp=off:gs=off:tha=off:ep=off:gtg=off. 4 Case Study To illustrate the practicality of the proposed Agda–Vampire integration we present a case study drawn from a real-world formalisation effort. The problem was selected because of: practical relevance — it arose during one of our own formalisation projects; A. Šinkarovs and M. Rawson13 non-triviality— the built-in proof search was unable to discharge neither of the goal, and a seasoned Agda developer required roughly two days to complete the proof (available in supplementary materials as ICplx.agda); structure amenable to automation— the difficulty lies primarily in mechanically assembling the constituent lemmas, whereas the underlying mathematical insight is comparatively straightforward. Consequently, the primary aim is not to discover novel proof structure but to automate the tedious goal-discharge phase. When formalising Fast Fourier Transform (FFT) algorithms and proving their correctness, we wish to abstract away from the classical presentation that relies on complex numbers. Instead we aim to generalise the algorithm to any commutative ring equipped with roots of unity. As a sanity check we must verify that our chosen axioms behave correctly for the familiar case of complex numbers and their roots of unity. To this end we first introduce an axiomatic theory of the reals together with elementary trigonometry. From these foundations we derive the conventional representation of complex numbers as ordered pairs of reals and define roots of unity via complex exponentiation. Finally we employ our system to confirm that this encoding satisfies the required properties. We begin by declaring the interface that captures the algebraic operations and their associated laws. The interface consists of a carrier set F together with addition, negation, multiplication, distinguished constants0 f and1 f , and a primitive for roots of unity, -ω f . The latter denotes the primitiven-th root of unity raised to thek-th power. Because roots of unity are traditionally defined only forn >0, we adopt the convention where -ω f ndenotes (n+ 1)-th root of unity. In other words we (morally) interpret -ω f n k asexp(−i2πk/(1 +n)) thereby avoiding the degenerate case n = 0. F: Set _+ f _ : F→ F→ F - f _ : F→ F _* f _ : F→ F→ F 0 f : F 1 f : F -ω f : (n : N)→ (k : N)→ F + f -assoc : Associative _+ f _ + f -comm : Commutative _+ f _ + f -idl: LeftIdentity 0 f _+ f _ + f -inv : LeftInverse 0 f - f _ _+ f _ * f -assoc : Associative _* f _ * f -comm : Commutative _* f _ * f -idl: LeftIdentity 1 f _* f _ * f -+ f -dist : _* f _ DistributesOver l _+ f _ The right-hand side records the algebraic laws required forFto constitute a commutative ring. These names used in types are defined in Agda’s standard library and expand to the expected formulations. For instance Commutative _+ f _ expands to:∀x y→ x + f y≡ y + f x. We now postulate the properties of -ω f that stem from the algebra of exponents. Interpreting z = e −2π , the intended equalities are: z 0/x = 1 z yx/x = 1 z xz/xy = z z/y z (y+z)/x = z y/x z z/x Because of our encoding, these statements must be expressed in a slightly more involved form, which we capture in the following Agda types. These lemmas constitute the logical backbone of the subsequent development. ω-x-0 : -ω f x 0 ≡ 1 f ω-x-yx : -ω f x ((1 + n x) * n y) ≡ 1 f ω-xy-xz : -ω f (x + n y + n (x * n y)) ((1 + n x) * n z) ≡ -ω f y z ω-x-y+z : -ω f x (y + n z) ≡ -ω f x y * f -ω f x z Next, on the left we introduce an axiomatic theory of the real numbers. The signature includes the usual arithmetic operations, a primitive embedding of natural numbersι, a unary minus, 14When Agda met Vampire an multiplicative “inverse” operation inv which should be thought of asinv x= 1/(1 +x), and the elementary trigonometric functions sin and cos. In the middle we we define derived operations: binary subtraction through unary minus, “division” through inv and the notions of zero and one throughι. After that we define properties of injectionι. On the right we require reals to be a commutative ring. R : Set π : R _+_ : R→ R→ R _*_ : R→ R→ R ι: N→ R -_ : R→ R inv : N→ R sin : R→ R cos : R→ R a - b = a + (- b) 0 = ι 0 1 = ι 1 a / n = a * inv n inv-* : ι (1 + n n) * inv n ≡ 1 ι-inj : ι n ≡ ι m→ m ≡ n ι-+ : ι (m + n n) ≡ ι m + ι n ι-* : ι (m * n n) ≡ ι m * ι n +-assoc : Associative _+_ +-comm : Commutative _+_ +-idl : LeftIdentity 0 _+_ +-invl : LeftInverse 0 -_ _+_ *-assoc : Associative _*_ *-comm : Commutative _*_ *-idl : LeftIdentity 1 _*_ *-+-distl : _*_ DistributesOver l _+_ The trigonometric equalities that follow are sufficient to derive the usual identities for complex exponentiation: sin[-x] : sin (- x) ≡ - sin x cos[-x] : cos (- x) ≡ cos x sin[2πn] : sin (ι 2 * π * ι n) ≡ 0 cos[2πn] : cos (ι 2 * π * ι n) ≡ 1 sin[x+y] : sin (x + y) ≡ sin x * cos y + cos x * sin y cos[x+y] : cos (x + y) ≡ cos x * cos y - sin x * sin y Having prepared the real and trigonometric infrastructure, we implement complex numbers as ordered pairs of reals and define the usual arithmetic operations. Complex exponentiation is defined via the Euler formula, and roots of unity are obtained by applying this function to the appropriate angle. Note that our “division” bynaligns with the desired definition of -ω which expects the first argument to be non-zero. data C : Set where _+_i : (re im : R)→ C ι c : N→ C ι c n = ι n + 0 i 0 c = ι c 0 1 c = ι c 1 _+ c _ : C→ C→ C (a + b i) + c (c + d i) = (a + c) + (b + d) i - c _ : C→ C - c (x + y i) = (- x) + (- y) i _* c _ : C→ C→ C (a + b i) * c (c + d i) = (a * c - b * d) + (a * d + b * c) i e^i_ : R→ C e^i_ x = (cos x) + (sin x) i -ω c : N→ N→ C -ω c n k = e^i (- ι 2 * π * ι k / n) The aim now is to demonstrate that the twelve theorems—eight concerning ring properties and four concerning roots-of-unity properties—introduced at the beginning of this section hold forCunder the operations defined above. We translate the preceding definitions, together with the properties of the real and natural numbers and apply Vampire to each goal. Detailed specifications are provided in the supplementary material located in the subdirectory complex. Here we simply note that all twelve theorems were proved automatically in a fraction of a second—an outcome that is both gratifying and somewhat surprising, given that some of the generated proofs comprise roughly three hundred lines of code. We regard this result as compelling evidence that the proposed approach is practical. A. Šinkarovs and M. Rawson15 5 Discussion and Future Work While we think our prototype shows considerable promise, it is not yet a full hammer-style system for Agda. It is plainly missing a premise selector and some automation to execute a complete round-trip. Agda’s reflection API already exposes facilities such asexecTCfor running external commands andcheckFromStringTCfor parsing results, so full automation of these steps is feasible within the existing framework. Additionally, the following improvements would improve the technology further to obtain a robust, high-quality hammer. Full Clausal Logic The current prototype insists on Horn clauses, both in the input and in proofs. However, full clausal logic seems achievable with a doubly-negated representation [10], and Section 3.3.1 corroborates this hypothesis. This would not only allow richer types to be exported from Agda, but also permit more Vampire proofs. In particular, Vampire already has support for various kinds of inductive reasoning [20], but the proofs cannot currently be recovered as they leave the Horn fragment, even on Horn inputs. Note that we cannot throw the baby out with the bathwater: Vampire’s frontend will happily perform classical operations like simplifying ¬P to P, so a clausal input form remains necessary. A Larger Slice of Agda However, this does not preclude performing a more elaborate translation from rich Agda types to Vampire clauses. We intend to broaden the fragment of Agda that can be translated and reconstructed. In particular, supporting parameterised types and indexed families is important. It is common practice to translate inductive families into parameterised types together with propositional equalities for certain constructors; work on indexed containers [2] and descriptors [12] makes this idea precise. We also wish to support term synthesis for proof-relevant types [17]. For example, synthesising an inhabitant of typeNcan be reduced to a Vampire goalnat. This would then be provable using an axiomzero. CoqHammer [14] and Lean-auto [33] demonstrate that more elaborate translations for more of Agda are feasible, but the details need to be reconciled with the approach taken here. Readable Proofs The generated proofs mirror Vampire’s proofs, producing one Agda definition for each step of a Vampire proof. This is ideal for inspecting the result and diagnosing problems, but often very verbose. We already apply some simplification during generation, but further work on a “proof prettifier” would substantially improve usability. Normalising proofs works, but produces very large terms — as expected from what is effectively cut-elimination. Our aim is a sensible middle ground that produces proofs resembling those a human would write. 6 Related Work Combining automated and interactive theorem proving is a relatively young idea. Ahrendt et al [1] are prescient in their assessment of the promise and challenges involved. It is encouraging that of six challenges they identify in their Section 2, two are completely solved, significant progress has been made on large theories and inductive reasoning, and only mismatched logic and lack of specialisation to the target domain remain unresolved. Various 16When Agda met Vampire approaches were tried around this time, including Tammet and Smith’s experiments with Gandalf, ALF, and the Horn fragment [41], closely related to our own. Today, Isabelle’s sledgehammer [32] is the archetypal hammer: the system selects premises from the prover library, exports goals and premises to a variety of ATPs [16], retrieves the required premises from the ATP proofs, and finally uses internal automation to recover a certified proof. Recent work [29] recovers very fine-grained proofs from SMT solvers, and in a curious turn of events it was also shown that external ATPs are not crucial for Sledgehammer [15]. In a similar vein, we could also mention HOL(y)Hammer [22], MizAR [42], and the recent first hammer for Metamath [11]. Moving to the dependently-typed world, CoqHammer [14] adapts the hammer paradigm to Rocq’s calculus of inductive constructions: it translates Rocq goals to first-order ATPs, employs heuristic and machine-learned premise selection, and uses internal reconstruction procedures (often involving proof search) to obtain constructive proofs. SMTCoq [3] adopts a more conservative strategy by importing and checking SMT/SAT proofs inside Rocq, thereby providing strong trust guarantees at the cost of greater restriction on the back ends. Both projects exemplify the substantial reconciliation machinery required when external tools assume classical reasoning but the host system is constructive. Work in Lean [45,33] shows active efforts to bring ATP automation to contemporary proof assistants: these projects combine translation, premise selection and partial reconstruction, and investigate the trade-off between lightweight translation layers and deeper kernel integration. Agda-specific work is scarce. The closest integrates Waldmeister [18], identifying (as we do) a representable sub-language and translating problems to Waldmeister and proofs back. Unlike our reflection-based approach, that project encodes the sub-language explicitly within Agda (giving it semantics and defining syntactic translations), which provides a precise specification of the fragment but imposes a substantial manual encoding burden on users and maintainers. Agda’s built-in automatic search (historically Agsy) attempts to synthesise inhabitants for a goal type and is effective for simple cases, but it rarely suffices where non-trivial composition of premises or sophisticated search is required. 7 Conclusions We have demonstrated a lightweight integration of Agda with the automated theorem prover Vampire that yields substantial proof-automation for tedious goals while preserving the trusted-core guarantees of an interactive theorem prover. By harnessing Agda’s reflection facilities to emit Vampire problems and reconstructing resulting proofs in Agda through a compact Prolog-based engine, the workflow mirrors the “hammer” paradigm without demanding invasive modifications to either system. Crucially, the approach is not intrinsically tied to Agda: any dependently-typed proof assistant that offers reflective extraction (e.g. Lean or Idris) could replace the Agda front-end whilst reusing very similar Vampire translation and proof-conversion machinery. Likewise, the method is not Vampire-specific; with relatively little implementation effort alternative ATPs can be used, allowing the framework to benefit from future advances in automated reasoning. Our prototype tackles a challenging ITP/ATP pairing: Agda provides virtually no built-in tactics, and Vampire represents a maximalist ATP with a rich inference repertoire. Yet the system discharges non-trivial lemmas—such as those concerning roots-of-unity properties— immediately, thereby markedly reducing the overall development effort. These findings indicate that a carefully-chosen fragment of dependent type theory can serve as a robust bridge between interactive and automated provers, and invite further exploration of richer A. Šinkarovs and M. Rawson17 fragments, tighter ATP integration, and broader applicability across dependently-typed languages. Statement on Large Language Models None of the results or the content here are produced by LLM. However, we did employ tools to spell- and style-check human-written text, with careful inspection of the outcomes. References 1 Ahrendt, Beckert, Hähnle, Menzel, Reif, Schellhorn, and Schmitt. Integrating Automated and Interactive Theorem Proving, pages 97–116. Springer Netherlands, Dordrecht, 1998. doi:10.1007/978-94-017-0435-9_4. 2Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. Journal of Functional Programming, 25:e5, 2015.doi:10.1017/ S095679681500009X. 3Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of sat/smt solvers to coq through proof witnesses. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, pages 135–150, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. 4 Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The SMT-LIB standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010. 5Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, and Andrei Voronkov. The Vampire diary. In Ruzica Piskac and Zvonimir Rakamaric, editors, Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, volume 15933 of Lecture Notes in Computer Science, pages 57–71. Springer, 2025. doi:10.1007/978-3-031-98682-6_4. 6Filip Bártek, Karel Chvalovský, and Martin Suda. Regularization in spider-style strategy discovery and schedule construction. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 194–213. Springer, 2024. doi:10.1007/978-3-031-63498-7_12. 7 Ahmed Bhayat and Giles Reger. A polymorphic Vampire (short paper). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th Interna- tional Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12167 of Lecture Notes in Computer Science, pages 361–368. Springer, 2020. doi:10.1007/978-3-030-51054-1_21. 8Ahmed Bhayat and Martin Suda. A higher-order Vampire (short paper). In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 75–85. Springer, 2024. doi:10.1007/978-3-031-63498-7_5. 9 Jasmin Christian Blanchette and Andrei Paskevich. TFF1: the TPTP typed first-order form with rank-1 polymorphism. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 414–420. Springer, 2013. doi:10.1007/978-3-642-38574-2_29. 10Guillaume Burel. A shallow embedding of resolution and superposition proofs into theλΠ- calculus modulo. In Jasmin Christian Blanchette and Josef Urban, editors, Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 18When Agda met Vampire 9-10, 2013, volume 14 of EPiC Series in Computing, pages 43–57. EasyChair, 2013. URL: https://doi.org/10.29007/ftc2, doi:10.29007/FTC2. 11 Mario Carneiro, Chad E. Brown, and Josef Urban. Automated theorem proving for metamath. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, Białystok, Poland, July 31 - August 4, 2023, volume 268 of LIPIcs, pages 9:1–9:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.9, doi:10.4230/LIPICS.ITP.2023.9. 12James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. The gentle art of levitation. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, page 3–14, New York, NY, USA, 2010. Association for Computing Machinery. doi:10.1145/1863543.1863547. 13 Koen Claessen and Nicholas Smallbone. Efficient encodings of first-order horn formulas in equational logic. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 388–404. Springer, 2018.doi: 10.1007/978-3-319-94205-6_26. 14 Łukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. Journal of Automated Reasoning, 61(1):423–453, Jun 2018.doi:10.1007/s10817-018-9458-4. 15Martin Desharnais and Jasmin Blanchette. Sledgehammering without atps (short paper). In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025, volume 352 of LIPIcs, pages 38:1–38:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.38, doi:10.4230/LIPICS.ITP.2025.38. 16Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1–8:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL:https://drops.dagstuhl.de/ entities/document/10.4230/LIPIcs.ITP.2022.8, doi:10.4230/LIPIcs.ITP.2022.8. 17Frantisek Farka, Ekaterina Komendantskaya, and Kevin Hammond. Proof-relevant Horn clauses for dependent type inference and term synthesis. Theory Pract. Log. Program., 18(3- 4):484–501, 2018. doi:10.1017/S1471068418000212. 18Simon Foster and Georg Struth. Integrating an automated theorem prover into Agda. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, pages 116–130, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. 19 Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert H. Müller and Dana S. Scott, editors, Higher Set Theory, pages 21–27, Berlin, Heidelberg, 1978. Springer Berlin Heidelberg. 20 Márton Hajdú, Laura Kovács, Michael Rawson, and Andrei Voronkov. The Vampire approach to induction (short paper). In Boris Konev, Claudia Schon, and Alexander Steen, editors, Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11 - 12, 2022, volume 3201 of CEUR Workshop Proceedings. CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3201/paper9.pdf. 21ISO/IEC. Information technology — Programming languages — Prolog — Part 1: General Core. Standard, International Organization for Standardization, 1995. 22Cezary Kaliszyk and Josef Urban. Hol(y)hammer: Online atp service for hol light. Mathematics in Computer Science, 9(1):5–22, Mar 2015. doi:10.1007/s11786-014-0182-0. 23Anja Petkovic Komel, Michael Rawson, and Martin Suda. Case study: Verified Vampire proofs in theλΠ-calculus modulo. CoRR, abs/2503.15541, 2025. URL:https://doi.org/10. 48550/arXiv.2503.15541, arXiv:2503.15541, doi:10.48550/ARXIV.2503.15541. A. Šinkarovs and M. Rawson19 24Konstantin Korovin. iProver — an instantiation-based theorem prover for first-order logic (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 292–298. Springer, 2008. doi:10.1007/978-3-540-71070-7_24. 25Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, and Andrei Voronkov. ALASCA: reasoning in quantified linear arithmetic. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 647–665. Springer, 2023. doi:10.1007/978-3-031-30823-9_33. 26Evgenii Kotelnikov, Laura Kovács, Giles Reger, and Andrei Voronkov. The Vampire and the FOOL. In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pages 37–48. ACM, 2016. doi:10.1145/2854065.2854071. 27 Laura Kovács, Simon Robillard, and Andrei Voronkov. Coming to terms with quantified reasoning. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 260–270. ACM, 2017. doi:10.1145/3009837.3009887. 28 Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 1–35. Springer, 2013.doi:10.1007/ 978-3-642-39799-8_1. 29 Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving (ITP 2025), volume 352 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:22, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL:https://drops.dagstuhl. de/entities/document/10.4230/LIPIcs.ITP.2025.26, doi:10.4230/LIPIcs.ITP.2025.26. 30 Bernd Löchner and Thomas Hillenbrand. A phytography of WALDMEISTER. AI Commun., 15(2-3):127–133, 2002. URL:http://content.iospress.com/articles/ai-communications/ aic261. 31 Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 371–443. Elsevier and MIT Press, 2001. URL:https://doi.org/10.1016/ b978-044450813-3/50009-6, doi:10.1016/B978-044450813-3/50009-6. 32Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011, volume 2 of EPiC Series in Computing, pages 1–11. EasyChair, 2010. URL:https: //doi.org/10.29007/36dt, doi:10.29007/36DT. 33 Yicheng Qian, Joshua Clune, Clark Barrett, and Jeremy Avigad. Lean-auto: An interface between lean 4 and automated theorem provers. In Computer Aided Verification: 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, page 175–196, Berlin, Heidelberg, 2025. Springer-Verlag.doi:10.1007/978-3-031-98682-6_ 10. 34 Giles Reger and Martin Suda. The uses of SAT solvers in Vampire. In Laura Kovács and Andrei Voronkov, editors, Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 20When Agda met Vampire 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015, volume 38 of EPiC Series in Computing, pages 63–69. EasyChair, 2015. URL: https://doi.org/10.29007/4w68, doi:10.29007/4W68. 35 Stephan Schulz, Simon Cruanes, and Petar Vukmirovic. Faster, higher, stronger: E 2.3. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 495–507. Springer, 2019.doi:10.1007/978-3-030-29436-6_ 29. 36 Peter Selinger. Friedman’s A-translation.https://mathstat.dal.ca/~selinger/papers/ papers/friedman.pdf. Accessed: 2026-02-18. 37 Nicholas Smallbone. Twee: An equational theorem prover. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 602–613. Springer, 2021. doi:10.1007/978-3-030-79876-5_35. 38Geoff Sutcliffe. The CADE ATP system competition — CASC. AI Mag., 37(2):99–101, 2016. URL: https://doi.org/10.1609/aimag.v37i2.2620, doi:10.1609/AIMAG.V37I2.2620. 39 Geoff Sutcliffe. Stepping stones in the TPTP world. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 30–50. Springer, 2024.doi:10.1007/ 978-3-031-63498-7_3. 40Geoff Sutcliffe, Frédéric Blanqui, and Guillaume Burel. Proof verification with GDV and LambdaPi — it’s a matter of trust. In Douglas A. Talbert and Ismaïl Biskri, editors, Proceedings of the 38th International Florida Artificial Intelligence Research Society Conference, FLAIRS 2025, Daytona Beach, FL, USA, May 20-23, 2025. Florida Online Journals, 2025. URL: https://doi.org/10.32473/flairs.38.1.138642, doi:10.32473/FLAIRS.38.1.138642. 41TANEL TAMMET and JAN M. SMITH. Optimized encodings of fragments of type theory in first-order logic. Journal of Logic and Computation, 8(6):713–744, 1998.doi:10.1093/ logcom/8.6.713. 42 Josef Urban and Geoff Sutcliffe. Automated reasoning and presentation support for formalizing mathematics in Mizar. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings, volume 6167 of Lecture Notes in Computer Science, pages 132–146. Springer, 2010.doi: 10.1007/978-3-642-14128-7_12. 43Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 415–432. Springer, 2021.doi:10.1007/978-3-030-79876-5_ 24. 44Philip Wadler. Propositions as types. Commun. ACM, 58(12):75–84, 2015.doi:10.1145/ 2699407. 45 Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Q. Jiang, and Sean Welleck. Premise selection for a lean hammer. In The Fourteenth International Conference on Learning Repres- entations, 2026. URL: https://openreview.net/forum?id=m04JJNeRK6.

Instant research discovery