Resolution by Unification and Equality

Candidate: Digricoli,Vincent Joseph

Abstract

In resolution by unification and equality, we recast the theory of binary resolution on the basis of the properties of the equality relationship as stated by the equality axioms. In standard binary resolution as introduced by J. A. Robinson in 1965, complete and strict unification is the sole basis for resolving complementary literals leading to exceptionally long proofs for even simple theorems involving equality. In RUE resolution implicit use of the equality axioms is made through their incorporation into two rules of inference which are sound and complete to prove E-unsatisfiability. Proofs by RUE resolution are significantly shorter and more transparent than standard refutations with the equality axioms. These qualities permit more effective application of heuristics to guide the search for refutations. We here present the complete theory of RUE resolution, with proofs of lemmas and theorems in support of the theory. We define RUE hyperresolution as a restriction strategy and develop a heuristic theory to order the search for refutations. We have implemented an RUE theorem prover and performed experiments in the fields of Boolean algebra, Ring theory and Group theory. We present a careful comparison with the work of McCharen, Overbeek and Wos, whose theorem prover using unification resolution with the equality axioms and paramodulation represents one of the most successful uses of unification resolution. The comparison of results presents major evidence that RUE resolution is a significant advance over unification resolution.