Paramodulation-Based Theorem Proving

By Robert Nieuwenhuis, A. Rubio. Handbook of Automated Reasoning, 2001

433 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.

E – a brainiac theorem prover (2002, neutral): “See [2] for an introduction to rewriting and [5,16] for equational theorem proving.”
The design and implementation of VAMPIRE (2002, positive): “It implements several versions of binary resolution and superposition with literal selection for logics with and without equality (see, e.g., [2,19]).”
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]).”
Handbook of Satisfiability (2021, background): “Another approach for building theory solvers relies on the power and flexibility of modern automated theorem provers, in particular, provers based on the superposition calculus [115], a modern version of the resolution calculus for first-order logic with equality.”