×

VAMPIRE

swMATH ID: 2918
Software Authors: Riazanov, Alexandre; Voronkov, Andrei
Description: Vampire 8.0, [RV02,Vor05] is an automatic theorem prover for first-order classical logic. It consists of a shell and a kernel. The kernel implements the calculi of ordered binary resolution and superposition for handling equality. The splitting rule and negative equality splitting are simulated by the introduction of new predicate definitions and dynamic folding of such definitions. A number of standard redundancy criteria and simplification techniques are used for pruning the search space: subsumption, tautology deletion (optionally modulo commutativity), subsumption resolution, rewriting by ordered unit equalities, and a lightweight basicness. The CASC version uses the Knuth-Bendix ordering. The lexicographic path ordering has been implemented recently but will not be used for this CASC. A number of efficient indexing techniques are used to implement all major operations on sets of terms and clauses. Run-time algorithm specialisation is used to accelerate some costly operations, e.g., checks of ordering constraints. Although the kernel of the system works only with clausal normal forms, the shell accepts a problem in the full first-order logic syntax, clausifies it and performs a number of useful transformations before passing the result to the kernel. When a theorem is proved, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the CNF.
Homepage: http://www.cs.miami.edu/~tptp/CASC/20/SystemDescriptions.html#Vampire---8.0
Keywords: VAMPIRE; high-performance theorem prover
Related Software: TPTP; E Theorem Prover; SPASS; z3; Isabelle/HOL; OTTER; Sledgehammer; Mizar; iProver; Coq; HOL Light; MPTP 0.2; HOL; AVATAR; SMT-LIB; CVC4; Mace4; MaLARea; Isabelle; Flyspeck
Cited in: 277 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
The design and implementation of VAMPIRE. Zbl 1021.68082
Riazanov, Alexandre; Voronkov, Andrei
2002
all top 5

Cited by 319 Authors

38 Voronkov, Andrei
31 Urban, Josef
19 Kovács, Laura Ildikó
17 Blanchette, Jasmin Christian
17 Kaliszyk, Cezary
16 Sutcliffe, Geoff
15 Reger, Giles
12 Suda, Martin
11 Benzmüller, Christoph Ewald
10 Paulson, Lawrence Charles
9 Schulz, Stephan
8 Hustadt, Ullrich
8 Jakubův, Jan
8 Riazanov, Alexandre
8 Waldmann, Uwe
7 Korovin, Konstantin
7 Weidenbach, Christoph
6 Böhme, Sascha
5 Bentkamp, Alexander
5 Brown, Chad Edward
5 Dixon, Clare
5 Hoder, Kryštof
5 Nieuwenhuis, Robert
5 Nipkow, Tobias
5 Robillard, Simon
5 Sorge, Volker
4 Chvalovský, Karel
4 Cruanes, Simon
4 Fleury, Mathias
4 Gleiss, Bernhard
4 Hozzová, Petra
4 Kühlwein, Daniel
4 Meng, Jia
4 Nalon, Cláudia
4 Olšák, Miroslav
4 Paskevich, Andrei
4 Pease, Adam
4 Peltier, Nicolas
4 Schmidt, Renate A.
4 Tinelli, Cesare
4 Vyskočil, Jiří
3 Asperti, Andrea
3 Barrett, Clark W.
3 Baumgartner, Peter
3 Bhayat, Ahmed
3 Bonacina, Maria Paola
3 Colton, Simon
3 Degtyarev, Anatoli Ivanovich
3 Färber, Michael
3 Fontaine, Pascal
3 Goertzel, Zarathustra Amadeus
3 Jamnik, Mateja
3 Kerber, Manfred
3 Konev, Boris
3 Lifschitz, Vladimir
3 Lühne, Patrick
3 Lyaletski, Alexander V.
3 Meier, Andreas
3 Plaisted, David Alan
3 Rabe, Florian
3 Rawson, Michael
3 Rinard, Martin C.
3 Schaub, Torsten H.
3 Schoisswohl, Johannes
3 Tassi, Enrico
3 Theiss, Frank
3 Tourret, Sophie
3 Verchinine, Konstantin
3 Vukmirović, Petar
3 Winkler, Sarah
3 Zombori, Zsolt
2 Arkoudas, Konstantine
2 Bringsjord, Selmer
2 Burel, Guillaume
2 Choi, Seungyeob
2 Duarte, André
2 Echenim, Mnacho
2 Ganzinger, Harald
2 Goubault-Larrecq, Jean
2 Gupta, Ashutosh
2 Hajdú, Márton
2 Hetzl, Stefan
2 Hillenbrand, Thomas
2 Itzhaky, Shachar
2 Janičić, Predrag
2 Kotel’nikov, Evgeny A.
2 Kragl, Bernhard
2 Kuncak, Viktor
2 Kurihara, Masahito
2 Lambers, Leen
2 Ludwig, Michel
2 McCasland, Roy L.
2 Middeldorp, Aart
2 Moser, Georg
2 Nguyen, Huu Hai
2 Pelzer, Björn
2 Pennemann, Karl-Heinz
2 Rath, Jakob
2 Sagiv, Mooly
2 Sato, Haruhiko
...and 219 more Authors

Citations by Year