Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-91-208

Rewrite-based equational theorem proving with selection and simplification

Bachmair, Leo and Ganzinger, Harald

MPI-I-91-208. September 1991, 24 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Note:
Revised version in the Journal of Logic and Computation 4, 3 (1994), pp.~217--247
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-91-208.pdfMPI-I-91-208.pdfMPI-I-91-208.dvi109 KBytes; 177 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1991-208
Hide details for BibTeXBibTeX
@TECHREPORT{BachmairGanzinger-91-mpii208,
  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},
}