The design and implementation of VAMPIRE

By Alexandre Riazanov, Andrei Voronkov. AI Communications, 2002

549 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/e333828f5aca95fcdb796c7924d16cbf1a5efebb

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

A proposal for an owl rules language (2004, methodology): “Finally, an alternative way to provide reasoning support for ORL would be to extend the translation of OWL into TPTP(11) implemented in the Hoolet system,(12) and use a first order prover such as Vampire to reason with the resulting first order theory [23, 30].”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, background): “These justifications can be found automatically by Sledgehammer [7], which internally invokes automatic theorem provers [4, 9, 41].”
OWL rules: A proposal and prototype implementation (2005, methodology): “The resulting theory is passed to a FO prover (Vampire in our case), where it can be used for reasoning tasks such as satisfiability checking and instance checking.”
Recognising Textual Entailment with Logical Inference (2005, methodology): “To check whether an entailment holds or not, we use two kinds of automated reasoning tools: Vam-pire, a theorem prover (Riazanov and Voronkov, 2002), and Paradox, a model builder (Claessen and S¨orensson, 2003).”
LUBM: A benchmark for OWL knowledge base systems (2005, unknown): “Another useful evaluation would compare memory-based systems that support complex reasoning, including OWLIM (a Sesame SAIL that supports in-memory OWL Lite reasoning), Hoolet [36] (an OWL DL reasoner that uses the Vampire [29] theorem prover), and Jena with the OWL Lite rule set enabled.”
Building a push-button RESOLVE verifier: Progress and challenges (2011, unknown): “In addition, Isabelle can be configured so that it can send the VCs to a powerful fully automated first-order prover, such as Vampire [ RiV02 ]o r E[ Sch04].”
Practical solution techniques for first-order MDPs (2009, methodology): “We use the Vampire theorem prover (Riazanov and Voronkov, 2002) for detecting equivalence and inconsistency.”
Formal methods: Practice and experience (2009, unknown): “For example, Vampire is an automatic theorem prover for first-order classical logic [Riazanov and Voronkov 2002].”
The Meaning Factory: Formal Semantics for Recognizing Textual Entailment and Determining Semantic Similarity (2014, methodology): “After conversion to first-order logic, we checked with the theorem prover Vampire (Riazanov and Voronkov, 2002) whether a proof could be found for the first sentence entailing the second, and whether a contradiction could be detected for the conjunction of both sentences translated into first-order ”