VAMPIRE
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.
Keywords for this software
References in zbMATH (referenced in 237 articles , 1 standard article )
Showing results 1 to 20 of 237.
Sorted by year (- Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
- Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
- Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
- Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
- Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
- Fandinno, Jorge; Lifschitz, Vladimir; Lühne, Patrick; Schaub, Torsten: Verifying tight logic programs with \textscanthemand \textscvampire (2020)
- Jakubův, Jan; Kaliszyk, Cezary: Relaxed weighted path order in theorem proving (2020)
- Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: (\mathrmK_\mathrmS\mathrmP) a resolution-based theorem prover for (\mathsfK_n): architecture, refinements, strategies and experiments (2020)
- Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
- Teucke, Andreas; Weidenbach, Christoph: SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (2020)
- Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
- Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
- Li, Di Long; Tiu, Alwen: Combining proverif and automated theorem provers for security protocol verification (2019)
- Lifschitz, Vladimir; Lühne, Patrick; Schaub, Torsten: Verifying strong equivalence of programs in the input language of \textscgringo (2019)
- Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Peuter, Dennis; Sofronie-Stokkermans, Viorica: On invariant synthesis for parametric systems (2019)