Glossary

Vampire contains lots of impenetrable vocabulary, acronyms, and references to other software. Hopefully talking to the team can help you, but please add to the following when you figure something out.

Acronyms

• ATP is Automatic Theorem Proving - what we endeavour to do! Note some discussion around whether this is Automated or Automatic!
• AVATAR is a method for splitting the search space into more manageable chunks, co-ordinated by a SAT solver. See AVATAR: The architecture for first-order theorem provers. Not actually an acronym (?).
• CADE is the Conference on Automated Deduction.
• CASC is the CADE ATP System Competition. It runs every year at CADE, pitting theorem provers against each other in friendly competition using problems from TPTP.
• CNF is Conjuctive Normal Form. May also refer to the corresponding TPTP sub-language, which is (almost) a subset of FOF.
• FMB is Finite Model Building, a method for finding finite counter-examples to a conjecture.
• FOF is the First-Order Formulas sub-language of TPTP. There are only two atomic types in FOF: Booleans ($o) and individuals ($i).
• LRS is the Limited Resource Strategy, a way of organising search under limited time and/or memory (discarding clauses that may not be useful given the remaining resources). See Limited resource strategy in resolution theorem proving. LRS is the default saturation algorithm in Vampire, but "Otter" and "DISCOUNT" are alternatives. NB: LRS can produce non-determinism and incompleteness as it discards clauses in response to pressure.
• LTB is Large Theory Batch, a sometime-division of CASC in which a large number of problems with a common set of axioms (theory) are attempted with a time limit for the whole batch, rather than a time limit per-problem as usual.
• SMT-COMP is the Satisfiability Modulo Theories Competition: similar to CASC, but for SMT solvers.
• SMT-LIB is the Satisfiability Modulo Theories Library: similar to TPTP, but for SMT. There is some overlap and Vampire can read the SMT-LIB format.
• TFA is based on TFF and introduces arithmetic.
• TFF is the typed first-order language of TPTP. TFF0 allows user-declared monomorphic types, and TFF1 extends TFF0 to polymorphism.
• THF is the typed higher-order language of TPTP.
• TPTP is a library of Thousands of Problems for Theorem Provers expressed in a Prolog-like syntax. See the quick start and TPTP technical report for more.

Vocabulary

• Polymorphism refers to the ability to quantify over types. This allows systems to reason about e.g. lists of any type, without having to specify particular lists like "a list of integers". There are many flavours of polymorphism: Vampire implements rank-1 polymorphism, which corresponds to the TFF1 language.
• Monomorphism is the absence of polymorphism. The TFF0 language is monomorphic.
• Term indexing is the problem of querying a large set of terms (the "database") for terms that unify, instantiate, generalise, or rename variables of a query term.
• Strategies are a combination of Vampire options. Sometimes written in an idiosyncratic format, e.g. ott+10_3_av=off:bd=preordered:drc=off:fde=none:nwc=5.0:sims=off:sp=reverse_arity:to=lpo:tgt=ground_0. The first letters are the saturation algorithm (ott for "Otter"), then a literal selection mode (10), then an age/weight ratio (3:1), then a series of colon-separated key=value options, and finally the time limit in deciseconds (!).
• Portfolio modes run a series of strategies (a "strategy schedule") in the hope that one of them will solve the problem. In practice, running several strategies in the time available solves more problems than one long run.

Other Software

• MiniSat is Vampire's current Boolean satisfiability (SAT) solver. We use it for various reasoning sub-tasks in Vampire.
• Z3 is a Satisfiability Modulo Theories (SMT) solver. We use it in a similar way to MiniSat, modulo theories.
• StarExec is a compute cluster. Confusingly, there is one instance of StarExec in Iowa, and one in Miami. CASC historically runs on StarExec.
• Spider and Snake are two approaches to the problem of generating strategy schedules for Vampire.
• A non-exhaustive list of theorem provers we have borrowed ideas from: E, SPASS, iProver, Twee, Otter, DISCOUNT, Prover9 and Mace4, ...