Basic superposition is complete

Abstract

We define a formalism of equality constraints and use it to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not originated in previous inferences is superposed upon. We first apply our results to the equational case and to unfailing Knuth-Bendix completion. Second, we extend the techniques to the case of full first-order clauses with equality, proving the refutational completeness of a new simple inference system. Finally, it is briefly outlined how this method can be applied to further restrict inference systems by the use of ordering constraints.