max planck institut
informatik
informatik
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
provability.
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
orderings.
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.
Acknowledgement:
References to related material:
http://www.mpi-sb.mpg.de/~hg/pra.html#MPI-I-97-2-011
| To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
|---|---|
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 | |
BibTeX