An Algorithm for Reasoning About Equality

A simple technique for reasoning about equalities
that is fast and complete for ground formulas 
with function symbols and equality is presented.
 A proof of correctness is given as well. 

CACM July, 1978

Shostak, R.

Theorem proving, deduction, program verification, equality

3.64 3.66 5.21

CA780709 DH February 7, 1979  3:41 PM

3079	5	3079
3079	5	3079
3079	5	3079