A New Class of Automated Theorem-Proving Algorithms
- 1 April 1974
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 21 (2) , 191-200
- https://doi.org/10.1145/321812.321814
Abstract
A procedure is defined for deriving from any statementSan infinite sequence of statementsS0,S1,S2,S3, ··· such that: (a) if there exists anisuch thatSiis unsatisfiable, thenSis unsatisfiable; (b) ifSis unsatisfiable, then there exists anisuch thatSiis unsatisfiable; (c) for allithe Herbrand universe ofSiis finite; hence, for eachithe satisfiability ofSiis decidable. The new algorithms are then based on the idea of generating successiveSiin the sequence and testing eachSifor satisfiability. Each element in the class of new algorithms is complete.Keywords
This publication has 15 references indexed in Scilit:
- The Unit Proof and the Input Proof in Theorem ProvingJournal of the ACM, 1970
- A Linear Format for Resolution With Merging and a New Technique for Establishing CompletenessJournal of the ACM, 1970
- Resolution With MergingJournal of the ACM, 1968
- Mechanical Theorem-Proving by Model EliminationJournal of the ACM, 1968
- Automatic Theorem Proving With Renamable and Semantic ResolutionJournal of the ACM, 1967
- 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
- Theorem-Proving on the ComputerJournal of the ACM, 1963
- An improved proof procedure1Theoria, 1960
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960