Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Strict basic superposition and chaining


Bachmair,  Leo
Programming Logics, MPI for Informatics, Max Planck Society;


Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Any fulltext), 589KB

Supplementary Material (public)
There is no public supplementary material available

Bachmair, L., & Ganzinger, H.(1997). Strict basic superposition and chaining (MPI-I-1997-2-011). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-9A19-B
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.