Equality-based binary resolution
- 1 April 1986
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 33 (2) , 253-289
- https://doi.org/10.1145/5383.5389
Abstract
A major event in automated reasoning was the introduction by Robinson of resolution as an inference principle that is complete for the first-order predicate calculus. Here the theory of binary resolution, based strictly on unification, is recast to incorporate the axioms of equality. Equality-based binary resolution is complete without making use of paramodulation and leads to refutations that are less than half as long as standard refutations with the equality axioms. A detailed discussion is given of the first major use of a theorem prover based on this new method.Keywords
This publication has 8 references indexed in Scilit:
- Universal unification and a classification of equational theoriesPublished by Springer Nature ,2005
- Variable elimination and chaining in a resolution-based prover for inequalitiesPublished by Springer Nature ,1980
- Automatic deduction and equalityPublished by Association for Computing Machinery (ACM) ,1979
- An algorithm for reasoning about equalityCommunications of the ACM, 1978
- Another Generalization of ResolutionJournal of the ACM, 1978
- Unit Refutations and Horn SetsJournal of the ACM, 1974
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960