Publications

E. Lusk and R. A. Overbeek, "Reasoning about Equality," Journal of Automated Reasoning, vol. 1, no. 2, 1969, pp. 209-228, . [pdf]

This note contains a set of six theorems that can be used to assess the ability of a theorem-proving system to reason about equality. The six theorems are graduated in terms of difficulty: they range from fairly trivial to quite difficult. They do not cover all aspects of equality reasoning, but they have proved useful to us in developing our system.