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.68082Riazanov, 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 all top 5 Cited in 32 Serials 40 Journal of Automated Reasoning 9 AI Communications 6 Annals of Mathematics and Artificial Intelligence 6 Journal of Applied Logic 5 Information and Computation 5 Logical Methods in Computer Science 4 Journal of Symbolic Computation 3 Artificial Intelligence 3 Mathematics in Computer Science 2 Journal of Logical and Algebraic Methods in Programming 1 American Mathematical Monthly 1 Applied Mathematics and Computation 1 Commentationes Mathematicae Universitatis Carolinae 1 Theoretical Computer Science 1 Annals of Pure and Applied Logic 1 The Journal of Logic Programming 1 Formal Aspects of Computing 1 Journal of Logic and Computation 1 MSCS. Mathematical Structures in Computer Science 1 Cybernetics and Systems Analysis 1 Journal of Functional Programming 1 The Journal of Artificial Intelligence Research (JAIR) 1 Logic Journal of the IGPL 1 Fundamenta Informaticae 1 The Journal of Logic and Algebraic Programming 1 Theory and Practice of Logic Programming 1 Lecture Notes in Computer Science 1 Logica Universalis 1 Journal of Formalized Reasoning 1 Symmetry 1 Izvestiya Irkutskogo Gosudarstvennogo Universiteta. Seriya Matematika 1 Distinguished Dissertations all top 5 Cited in 12 Fields 265 Computer science (68-XX) 101 Mathematical logic and foundations (03-XX) 2 Category theory; homological algebra (18-XX) 2 Operations research, mathematical programming (90-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Information and communication theory, circuits (94-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Number theory (11-XX) 1 Group theory and generalizations (20-XX) 1 Geometry (51-XX) 1 Mathematics education (97-XX) Citations by Year