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