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; CVC4; MPTP 0.2; Coq; SMT-LIB; iProver; HOL; AVATAR; HOL Light; Mace4; MaLARea; Isabelle; Flyspeck Cited in: 297 Documents 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 343 Authors 38 Voronkov, Andrei 32 Urban, Josef 20 Blanchette, Jasmin Christian 20 Kovács, Laura Ildikó 17 Kaliszyk, Cezary 17 Sutcliffe, Geoff 16 Reger, Giles 13 Suda, Martin 11 Benzmüller, Christoph Ewald 10 Jakubův, Jan 10 Paulson, Lawrence Charles 9 Schulz, Stephan 9 Waldmann, Uwe 9 Weidenbach, Christoph 8 Hustadt, Ullrich 8 Korovin, Konstantin 8 Riazanov, Alexandre 7 Bentkamp, Alexander 6 Böhme, Sascha 6 Bonacina, Maria Paola 6 Dixon, Clare 6 Robillard, Simon 6 Tourret, Sophie 5 Brown, Chad Edward 5 Cruanes, Simon 5 Hoder, Kryštof 5 Nieuwenhuis, Robert 5 Nipkow, Tobias 5 Sorge, Volker 5 Vukmirović, Petar 4 Bhayat, Ahmed 4 Chvalovský, Karel 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ří 4 Winkler, Sarah 3 Asperti, Andrea 3 Barrett, Clark W. 3 Baumgartner, Peter 3 Colton, Simon 3 Degtyarev, Anatoli Ivanovich 3 Duarte, André 3 Färber, Michael 3 Fontaine, Pascal 3 Goertzel, Zarathustra Amadeus 3 Jamnik, Mateja 3 Janičić, Predrag 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 Verchinine, Konstantin 3 Zombori, Zsolt 2 Arkoudas, Konstantine 2 Bringsjord, Selmer 2 Bromberger, Martin 2 Burel, Guillaume 2 Choi, Seungyeob 2 Echenim, Mnacho 2 Ganzinger, Harald 2 Goubault-Larrecq, Jean 2 Gupta, Ashutosh 2 Hajdú, Márton 2 Hetzl, Stefan 2 Heule, Marijn J. H. 2 Hillenbrand, Thomas 2 Itzhaky, Shachar 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 Narboux, Julien 2 Nguyen, Huu Hai 2 Nummelin, Visa 2 Pelzer, Björn ...and 243 more Authors all top 5 Cited in 33 Serials 49 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 American Mathematical Monthly 2 Journal of Logical and Algebraic Methods in Programming 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 ACM Transactions on Computational Logic 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 285 Computer science (68-XX) 109 Mathematical logic and foundations (03-XX) 2 History and biography (01-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 Number theory (11-XX) 1 Group theory and generalizations (20-XX) 1 Geometry (51-XX) 1 Mathematics education (97-XX) Citations by Year