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; Isabelle/HOL; z3; OTTER; iProver; Sledgehammer; CVC4; Coq; AVATAR; Mizar; SMT-LIB; HOL Light; MPTP 0.2; HOL; MaLARea; Mace4; Isabelle; Prover9 Cited in: 326 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 385 Authors 42 Voronkov, Andrei 33 Urban, Josef 24 Kovács, Laura Ildikó 21 Blanchette, Jasmin Christian 18 Reger, Giles 18 Sutcliffe, Geoff 17 Kaliszyk, Cezary 13 Suda, Martin 11 Benzmüller, Christoph Ewald 10 Jakubův, Jan 10 Paulson, Lawrence Charles 10 Weidenbach, Christoph 9 Korovin, Konstantin 9 Schulz, Stephan 9 Waldmann, Uwe 8 Hustadt, Ullrich 8 Riazanov, Alexandre 7 Bentkamp, Alexander 7 Tourret, Sophie 6 Böhme, Sascha 6 Bonacina, Maria Paola 6 Brown, Chad Edward 6 Dixon, Clare 6 Hozzová, Petra 6 Robillard, Simon 5 Bhayat, Ahmed 5 Cruanes, Simon 5 Hoder, Kryštof 5 Nieuwenhuis, Robert 5 Nipkow, Tobias 5 Pease, Adam 5 Peltier, Nicolas 5 Schmidt, Renate A. 5 Schoisswohl, Johannes 5 Sorge, Volker 5 Vukmirović, Petar 4 Chvalovský, Karel 4 Fisher, Michael 4 Fleury, Mathias 4 Gleiss, Bernhard 4 Kühlwein, Daniel 4 Lifschitz, Vladimir 4 Meng, Jia 4 Nalon, Cláudia 4 Olšák, Miroslav 4 Paskevich, Andrei 4 Tinelli, Cesare 4 Vyskočil, Jiří 4 Winkler, Sarah 4 Zombori, Zsolt 3 Asperti, Andrea 3 Barrett, Clark W. 3 Baumgartner, Peter 3 Bromberger, Martin 3 Colton, Simon 3 Degtyarev, Anatoli Ivanovich 3 Duarte, André 3 Echenim, Mnacho 3 Färber, Michael 3 Fontaine, Pascal 3 Goertzel, Zarathustra Amadeus 3 Hajdú, Márton 3 Jamnik, Mateja 3 Janičić, Predrag 3 Kerber, Manfred 3 Konev, Boris 3 Lühne, Patrick 3 Lyaletski, Alexander V. 3 Lynch, Christopher A. 3 Meier, Andreas 3 Plaisted, David Alan 3 Rabe, Florian 3 Rath, Jakob 3 Rawson, Michael 3 Rinard, Martin C. 3 Schaub, Torsten H. 3 Tassi, Enrico 3 Theiss, Frank 3 Verchinine, Konstantin 3 Xu, Yang 2 Arkoudas, Konstantine 2 Braun, David J. 2 Bringsjord, Selmer 2 Burel, Guillaume 2 Cao, Feng 2 Chen, Shuwei 2 Choi, Seungyeob 2 Desharnais, Martin 2 Ebner, Gabriel 2 Fandinno, Jorge 2 Ganzinger, Harald 2 Goubault-Larrecq, Jean 2 Gupta, Ashutosh 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 ...and 285 more Authors all top 5 Cited in 34 Serials 52 Journal of Automated Reasoning 10 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 Information Sciences 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 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 14 Fields 313 Computer science (68-XX) 111 Mathematical logic and foundations (03-XX) 4 Geometry (51-XX) 3 Operations research, mathematical programming (90-XX) 3 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Information and communication theory, circuits (94-XX) 2 History and biography (01-XX) 2 Category theory; homological algebra (18-XX) 1 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Number theory (11-XX) 1 Group theory and generalizations (20-XX) 1 Numerical analysis (65-XX) 1 Mathematics education (97-XX) Citations by Year