Resolution Theorem Proving

By L. Bachmair, H. Ganzinger, David A. McAllester, C. Lynch. Handbook of Automated Reasoning, 2001

515 citations recorded by the source corpus.

How researchers see this paper

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

OWL rules: A proposal and prototype implementation (2005, background): “Given a set of first-order formulas, Vampire transforms it into an equisatisfiable set of clauses, and then tries to demonstrate inconsistency of the clause set by saturating it with ordered resolution and superposition (see [3, 33]).”
Query Answering for OWL-DL with Rules (2004, background): “It is well-known that this calculus remains complete if ground literals are totally ordered under an arbitrary ordering ≻, and inferences are performed on maximal literals only [3].”
Bridging the gap between OWL and relational databases (2007, methodology): “Such a model can be constructed, for example, using the model-constructionmethod used to show the completeness of resolution [5].”
The design and implementation of VAMPIRE (2002, unknown): “It implements several versions of binary resolution and superposition with literal selection for logics with and without equality (see, e.g., [2,19]).”
Reasoning on UML class diagrams (2005, background): “One possibility would be to resort to a full FOL theorem prover [3, 35].”
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (2016, unknown): “We use resolution with free selection (Bachmair and Ganzinger, 2001).”