Automatic deduction and equality
Vincent J. Digricoli · 1979
This paper defines rules of inference which incorporate the axioms of equality into a new definition of binary resolution which is based on equality as well as unification. These inference rules are complete to prove E-unsatisfiability and lead to much shorter proofs than those using the equality axioms.