Another Generalization of Resolution
- 1 July 1978
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 25 (3) , 341-351
- https://doi.org/10.1145/322077.322078
Abstract
This paper defines a generahzatmn of the resolutton prmctple for theorem-proving, which permRs a hterarchtcal orgamzatton within the theorem-prover The generahzatton corresponds to an cxtenston of the usual umficatmn procedures A graph-theoreUc categonzaUon of sets of clauses with input or umt refutatmns is given, and completeness theorems are proved m th~s category In the case of sets of clauses which include the equahty predicate, the generahzatmn gives a new techmque for treating equahty, for which a completeness theorem Ls proved An maplementatmn of these tdeas gives results which suggest that this ~s a more efficient method for treating equahty than prewously proposed schemesKeywords
This publication has 7 references indexed in Scilit:
- Refutation graphsArtificial Intelligence, 1976
- Unit Refutations and Horn SetsJournal of the ACM, 1974
- Z-Resolution: Theorem-Proving with Compiled AxiomsJournal of the ACM, 1973
- The Unit Proof and the Input Proof in Theorem ProvingJournal of the ACM, 1970
- Axiom systems in automatic theorem provingPublished by Springer Nature ,1970
- Resolution With MergingJournal of the ACM, 1968
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965