A Technique for Establishing Completeness Results in Theorem Proving with Equality
Gerald E. Peterson · SIAM Journal on Computing · 1983
It is proved that an automatic theorem proving system consisting of resolution, paramodulation, factoring, equality reversal, simplification, and subsumption removal is complete in first-order logic with equality. When restricted to equality units, the system is similar to the Knuth-Bendix procedure for deriving consequences from equalities. However, our proofs of completeness are restricted to the case in which the ordering on words (terms or atoms) that is required in this type of process is order-isomorphic to the positive integers. The completeness of resolution and paramodulation without the functionally reflexive axioms is a simple corollary of our result. The methods used are based upon the familiar ideas associated with semantic trees, and should be helpful in showing that other theorem proving systems with equality are complete.