Strict basic superposition and chaining

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