Basic superposition is complete
Document typeResearch report
Rights accessOpen Access
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.
CitationNieuwenhuis, R.; Rubio, A. Basic superposition is complete. 1991.
Is part ofLSI-91-42