MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Rewrite-based equational theorem proving with selection and simplification

Bachmair, Leo and Ganzinger, Harald

September 1991, 24 pages.

Status: available - back from printing

We present various refutationally complete calculi for first-order clauses with equality that allow for arbitrary selection of negative atoms in clauses. Refutation completeness is established via the use of well-founded orderings on clauses for defining a Herbrand model for a consistent set of clauses. We also formulate an abstract notion of redundancy and show that the deletion of redundant clauses during the theorem proving process preserves refutation completeness. It is often possible to compute the closure of nontrivial sets of clauses under application of non-redundant inferences. The refutation of goals for such complete sets of clauses is simpler than for arbitrary sets of clauses, in particular one can restrict attention to proofs that have support from the goals without compromising refutation completeness. Additional syntactic properties allow to restrict the search space even further, as we demonstrate for so-called quasi-Horn clauses. The results in this paper contain as special cases or generalize many known results about Knuth-Bendix-like completion procedures (for equations, Horn clauses, and Horn clauses over built-in Booleans), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.
Revised version in the Journal of Logic and Computation 4, 3 (1994), pp.~217--247

  • MPI-I-91-208.pdfMPI-I-91-208.pdfMPI-I-91-208.dvi
  • Attachement: MPI-I-91-208.dvi (109 KBytes); MPI-I-91-208.pdf (177 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
  TITLE = {Rewrite-based equational theorem proving with selection and simplification},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-91-208},
  MONTH = {September},
  YEAR = {1991},
  ISSN = {0946-011X},
  NOTE = {Revised version in the Journal of Logic and Computation 4, 3 (1994), pp.~217--247},