A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- 1 July 1970
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 17 (3) , 525-534
- https://doi.org/10.1145/321592.321603
Abstract
A new technique is given for establishing the completeness of resolution-based deductive systems for first-order logic (with or without equality) and several new completeness results are proved using this technique. The technique leads to very simple and clear completeness proofs and can be used to establish the completeness of most resolution-based deductive systems reported in the literature. The main new result obtained by means of this technique is that a linear format for resolution with merging and set of support and with several further restrictions is a complete deductive system for the first-order predicate calculus.Keywords
This publication has 3 references indexed in Scilit:
- Resolution With MergingJournal of the ACM, 1968
- Efficiency and Completeness of the Set of Support Strategy in Theorem ProvingJournal of the ACM, 1965
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965