A New Class of Automated Theorem-Proving Algorithms
Ross Overbeek · Journal of the ACM · 1974
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.