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 179 articles , 1 standard article )
Showing results 1 to 20 of 179.
Sorted by year (- Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
- Berghammer, Rudolf; Stucke, Insa; Winter, Michael: Using relation-algebraic means and tool support for investigating and computing bipartitions (2017)
- Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
- Kovács, Laura; Robillard, Simon; Voronkov, Andrei: Coming to terms with quantified reasoning (2017)
- Peltier, N.: A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules (2017)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
- Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei: Selecting the selection (2016)
- Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
- Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: $\text K_ \textS\textP$: a resolution-based prover for multimodal K (2016)
- Reger, Giles; Suda, Martin; Voronkov, Andrei: Finding finite models in multi-sorted first-order logic (2016)
- Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
- Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
- Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
- Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
- Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
- Dragan, Ioan; Kovács, Laura: Lingva: generating and proving program properties using symbol elimination (2015)