and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4. SETHEO is a high-performance system based on the goal-directed model elimination calculus, originally developed by a team under direction of Wolfgang Bibel. E and SETHEO have been combined (with other systems) in the composite theorem prover E-SETHEO. Vampire was originally developed and implemented at Manchester University by Andrei Voronkov and Krystof Hoder. It is now developed by a growing international team. It has won the FOF division (among other divisions) at the CADE ATP System Competition regularly since 2001. Waldmeister is a specialized system for unit-equational first-order logic developed by Arnim Buch and Thomas Hillenbrand. It won the CASC UEQ division for fourteen consecutive years (1997–2010). SPASS is a first order logic theorem prover with equality. This is developed by the research group Automation of Logic, Max Planck Institute for Computer Science. The Theorem Prover Museum is an initiative to conserve the sources of theorem prover systems for future analysis, since they are important cultural/scientific artefacts. It has the sources of many of the systems mentioned above. Popular techniques First-order resolution with unification Model elimination Method of analytic tableaux Superposition and term rewriting Model checking Mathematical induction Binary decision diagrams DPLL Higher-order unification Software systems Free software Alt-Ergo Automath CVC E GKC Gödel machine iProver IsaPlanner KED theorem prover leanCoP Leo II LCF Logictools online theorem prover LoTREC MetaPRL Mizar NuPRL Paradox Prover9 PVS Simplify SPARK (programming language) Twelf Z3 Theorem Prover Proprietary software Acumen RuleManager (commercial product) ALLIGATOR (CC BY-NC-SA 2.0 UK) CARINE KIV (freely available as a plugin for Eclipse) Prover Plug-In (commercial proof engine product) ProverBox Wolfram Mathematica ResearchCyc Spear modular arithmetic theorem prover See also Curry–Howard correspondence Symbolic computation Ramanujan machine Computer-aided proof Formal verification Logic programming Proof checking Model checking Proof complexity Computer algebra system Program analysis (computer science) General Problem Solver Metamath language for formalized mathematics Notes References II . External links A list of theorem proving tools Formal methods