Lean on Vampire Proofs (Short Paper)

Abstract

Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampires output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean

Figures (4)

• Figure 1: Simplified Vampire proof showing that if every element of a group has order two, the group is commutative. Here, $\mathsf{mul}$ denotes the group operator and $\mathsf{id}$ the group's identity element. The variables $x,y$ are implicitly universally quantified, whereas $\sigma_0$ and $\sigma_1$ are Skolem constants. The proof steps $\text{Sup, FwDem}$ respectively denote superposition and its variant forward demodulation.
• Figure 2: (a) Lean theorem representing the superposition step 160 of \ref{['fig:group-proof']}. (b) The instantiation of paramodulation (i.e. more general superposition) for (a). Clauses $C, D$ are empty for the instance of \ref{['fig:group-proof']}.
• Figure 3: Number of proofs found by baseline Vampire (column 2) vs our Lean proof reconstructions (columns 3--5), sorted for success/failure reasons. Success means trusted Vampire proofs, validated by Lean.
• Figure 4: (a) Comparing baseline Vampire and our Vampire version outputting a Lean file; here, we include only CNF and FOF problems where baseline Vampire found a proof by contradiction. This plot only accounts for the overhead in Vampire, not for Lean proof reconstruction and checking time. Notice the logarithmic y-axis. (b) A scatter plot comparing the Lean proof reconstruction and checking runtime vs the Vampire runtime. (c) A scatter plot of Lean runtime vs number of theorems in a Lean input file.