Automatic deduction and equality
- 1 January 1979
- proceedings article
- Published by Association for Computing Machinery (ACM)
- p. 240-250
- https://doi.org/10.1145/800177.810076
Abstract
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.Keywords
This publication has 0 references indexed in Scilit: