Reasoning about Equality
|Title||Reasoning about Equality|
|Publication Type||Journal Article|
|Year of Publication||1985|
|Authors||Lusk, EL, Overbeek, RA|
|Journal||Journal of Automated Reasoning|
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.