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


Strict basic superposition and chaining

Bachmair, Leo and Ganzinger, Harald

MPI-I-97-2-011. December 1997, 22 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
The most efficient techniques that have been developed
to date for equality handling in first-order theorem proving
are based on superposition calculi.
Superposition is a refinement of paramodulation in that
various ordering constraints are imposed on inferences.
For practical purposes, a key aspect of superposition is
its compatibility with powerful simplification techniques.
In this paper we solve a long-standing open problem
by showing that strict superposition---that is,
superposition without equality factoring---is refutationally complete.
The difficulty of the problem arises from the fact that the strict calculus,
in contrast to the standard calculus with equality factoring,
is not compatible with arbitrary removal of tautologies,
so that the usual techniques for proving the (refutational) completeness
of paramodulation calculi are not directly applicable.
We deal with the problem by introducing a suitable notion
of {\em direct rewrite proof\/} and
modifying proof techniques based on candidate models
and counterexamples in that we define these concepts,
not in terms of semantic truth, but in terms of direct
We also introduce a corresponding concept of redundancy
with which strict superposition is compatible and that
covers most simplification techniques, though not, of course,
removal of {\em all\/} tautologies.
Reasoning about the strict calculus,
it turns out, requires techniques known from the
more advanced {\em basic\/} variant of superposition.
Superposition calculi, in general, are parametrized by (well-founded) literal
We prove refutational completeness of strict basic
superposition for a large class of such orderings.
For certain orderings, positive top-level superposition inferences {\em from\
/} variables
turn out to be redundant---a result that is relevant, surprisingly, in
the context of equality elimination methods.
The results are also extended to chaining calculi for non-symmetric transitiv
e relations.

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-97-2-011.pdf.gz

Please read the following errata file. It contains important additional information.
303 KBytes; 588 KBytes; 8 KBytes; 239 KBytes; 113 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:
Hide details for BibTeXBibTeX
  AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
  TITLE = {Strict basic superposition and chaining},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-97-2-011},
  MONTH = {December},
  YEAR = {1997},
  ISSN = {0946-011X},