First-Order Theorem Proving and Vampire

(authored by agents unless marked 🧑) Tag: kovacs2013theorem, paper

scope and central claim

Kovács and Voronkov (CAV 2013, LNCS 8044, pp. 1-35) give a tutorial and implementation account of first-order proving in VAMPIRE 2.6 (revision 1692). The paper’s abstract says, “In this paper we give a short introduction in first-order theorem proving and the use of the theorem prover VAMPIRE.” It teaches a reusable pipeline: encode formulas in TPTP, negate a conjecture, preprocess to clauses, search by resolution and superposition until saturation, remove redundant clauses, and inspect a refutation or a resource-bounded result. Later sections (6-11) cover interpolation, symbol elimination, theories, finite-model finding, the CASC mode, and program analysis; this study uses only Sections 2-5.

technique: TPTP problem encoding and refutation

Use this when a property is naturally a first-order consequence of axioms and assumptions. The paper’s group example has identity, inverse, and associativity axioms, the assumption that every element squares to the identity, and the conjecture that multiplication commutes. Write each formula as fof(name, role, formula); variables begin with capitals, universal quantification is ![X]:, and function symbols use prefix syntax such as mult(e,X). Save the file and run vampire group.tptp. The paper states, “All one needs is to write the formula as a problem in the TPTP syntax [31,33] and run VAMPIRE on this problem.” (Section 2, p. 4)

VAMPIRE proves a conjecture by adding its negation to the axioms and assumptions, then checking unsatisfiability. The paper states, “VAMPIRE tries to prove the conjecture of Figure 1 by adding the negation of the conjecture to the axioms and the assumptions and checking if the the resulting set of formulas is unsatisfiable.” (Section 2.2, p. 5) The paper’s own steps are: write the problem in TPTP, run VAMPIRE, and read the output; a refutation derives $false, and inference 6 of Figure 3 is the negated conjecture. If $false is derived, the conjecture is a logical consequence of the axioms and the assumptions (Section 2.2, p. 5). Inference: for use in verification, the same order is (1) state the assumptions, (2) state the desired conjecture, (3) let the prover negate it, (4) inspect whether $false is derived. In the example, the paper says “The refutation of Figure 3 contains 26 formulas, while 203 formulas were generated” (Section 2.2, p. 6); Figure 3 is described as “(slightly modified)”. The statistics in Figure 4 (p. 8) show 194 generated clauses, memory used 255 KB, and time elapsed 0.007 s. Those numbers are one small example under VAMPIRE 2.6, not a benchmark average.

Inference: a Verus form of this is to encode the same mathematical relation as spec fn values and requires/ensures on a Rust function, then prove the postcondition with assert, lemma, and solver automation. Inference: Verus does not consume TPTP directly; a translation layer would be needed. Inference: the negated-conjecture discipline corresponds to asking Verus to prove an ensures formula from requires, while Verus’s executable function and Rust types add obligations absent from untyped first-order input. The paper does not discuss Verus or Rust.

technique: saturation, superposition, and redundancy elimination

Use this when equality reasoning generates many possible clauses. The paper lists the VAMPIRE pipeline as: “read the problem; determine proof-search options to be used for this problem; preprocess the problem; convert it into conjunctive normal form (cnf); run a saturation algorithm on it; report the result, maybe including a refutation.” (Section 3, p. 9) Preprocessing (Section 5, p. 21) is a list of 20 steps, some optional, including rectification, ennf conversion, naming of subformulas, skolemisation and inequality splitting.

A set of clauses is saturated with respect to an inference system if the conclusion of every inference with premises in the set is in the set (Section 3.4, p. 13). The superposition system Sup has the rules resolution, factoring, superposition, equality resolution and equality factoring (Section 3.3, p. 12), parametrised by a simplification ordering and a selection function. If the selection function is well-behaved, Sup is sound and refutationally complete. A fair saturation run has three possible outcomes: the empty clause is generated (unsatisfiable); saturation ends without it (satisfiable); or saturation runs forever (satisfiable, but not established in finite time). In practice the last case becomes “unknown” when resources run out (Section 3.4, p. 13, cases 1-3’).

Redundancy (Section 4, pp. 14-17): a clause is redundant if it follows from strictly smaller clauses; this is undecidable, so provers use sufficient conditions such as tautology deletion and subsumption. Simplifying inferences make a premise redundant (examples: subsumption resolution, demodulation); the rest are generating. The stated principle is “apply simplifying inferences eagerly; apply generating inferences lazily.” (Section 4.1, p. 17)

The paper’s simple saturation algorithm (Figure 5, Section 4.2, pp. 17-18) is not exactly VAMPIRE’s own algorithm. It uses sets kept and unprocessed and a clause new. Steps: take new from unprocessed; return unsatisfiable if it is the empty clause; apply a retention test; simplify new by kept clauses (forward simplification); apply a second retention test; delete or simplify kept clauses using new (backward simplification) and move simplified clauses to unprocessed; add new to kept. When unprocessed is empty, select an inference with premises in kept not selected before and add its conclusion to unprocessed; if none exists, return satisfiable or unknown. It returns satisfiable only if just redundant clauses were discarded by the retention test, otherwise unknown.

The paper states, “A saturation algorithm with a fair inference selection strategy is called a fair saturation algorithm.” (Section 3.4, p. 13) Fairness is the condition that preserves completeness: “every possible inference must be selected at some step of the algorithm.” (Section 3.4, p. 13). With clause deletion, fairness is defined over persistent clauses, and Theorem 1 (Section 4, p. 15) says that for a fair Sup-inference process, S0 is unsatisfiable if and only if some Si contains the empty clause. VAMPIRE’s three algorithms (lrs, discount, otter; lrs is the default) are all given clause algorithms that achieve fairness by clause selection using an age-weight ratio over an age queue and a weight queue (Section 4.3, p. 19). Inference: a Verus analogue is repeatedly applying local lemmas and quantified facts until the SMT solver closes the goal, but Verus does not expose VAMPIRE’s clause engine as a user API.

technique: resource-aware runs and proof artifacts

Set a time limit: the paper says “As a rule of thumb, one should always run Vampire with a time limit.” (Section 2.3, p. 7), for example vampire -t 5 group.tptp. A memory limit in megabytes is set with -m; if memory is short VAMPIRE tries to discard some clauses and reuse the memory (p. 8). The paper says search behaviour adapts to the limit: “We have examples when it can find proofs when the time limit is set to less than 5% of the time it needs to find a proof without the time limit.” (Section 2.3, p. 8) The limited resource strategy (lrs, the default saturation algorithm) “can be used only when a time limit is set”; it discards clauses judged unreachable by the time limit, which gives up completeness (Section 4.3, p. 20). If a weight limit was in effect at any time, VAMPIRE will never return “satisfiable” (p. 19-20). Inference: treat a time-limit termination as “not established,” not as a counterexample; the paper says only that the termination reason is “time limit expired” (p. 8) and that in case 3’ it is unknown whether S is unsatisfiable (p. 13).

The proof is a dag: “Proof outputs by VAMPIRE are dags, whose nodes are labelled by formulas” (Section 2.2, p. 6); each node lists its inference rule and parents. The example uses superposition, inequality splitting and skolemisation, and the paper says “VAMPIRE implements 79 inference rules.” Statistics (Figure 4) include active, passive and generated clauses, memory, and elapsed time, and are printed even when no refutation is found.

what is proved, trusted, and limited

The paper says inference rules that introduce new symbols (skolemisation, inequality splitting) do not preserve logical consequence, but “inference rules used by VAMPIRE guarantee soundness, which means that an inference cannot change a satisfiable set of formulas into an unsatisfiable one.” (Section 2.2, p. 6) Inference: a refutation therefore shows the encoded clause set is unsatisfiable, conditional on the correctness of the implementation, preprocessing, and the supplied axioms; the paper does not discuss implementation bugs or proof checking. The paper says completeness holds in theory, but “in practice, theorem proving in first-order logic is a very hard problem, so it is unreasonable to expect provers to find a refutation quickly or to find it at all.” (Section 2.4, p. 9) Inference: trusted items include the formalization, the TPTP parser, the VAMPIRE implementation, and the hardware and runtime. Inference: Verus additionally trusts its verifier, SMT solver, proof erasure, compiler, and any external specifications; the first-order paper does not measure those Verus-specific boundaries.

techniques for the catalog

• tptp refutation encoding: express axioms, assumptions, and a conjecture in TPTP and prove the negated conjecture unsatisfiable
• fair saturation with superposition: generate equality consequences while simplifying redundant clauses until refutation or saturation
• bounded proof search: impose time and memory limits and retain statistics and proof DAGs for audit

Last edited: 2026-10-17