Automatic theorem-proving and the decision problem

This paper investigates the possibilities of the resolution method of J.A. Robinson [12] as a decision procedure for classes of first-order formulas. It is shown here that resolution, a machine-oriented inference procedure, can be modified to be a method which decides whether certain kinds of quantificational formulas are satisfiable or unsatisfiable. A new complete resolution technique is presented and is demonstrated to be a decision procedure for satisfiability for many previously studied solvable classes. Most proofs are omitted, but may be found in [6].