Resolution Strategies as Decision Procedures

The resolution principle, an automatic inference technique, is studied as a possible decision procedure for certain classes of first-order formulas. It is shown that most previous resolution strategies do not decide satisfiability even for “simple” solvable classes. Two new resolution procedures are described and are shown to be complete (i.e. semidecision procedures) in the general case and, in addition, to be decision procedures for successively wider classes of first-order formulas. These include many previously studied solvable classes. The proofs that a complete resolution procedure will always halt (without producing the empty clause) when applied to satisfiable formulas in certain classes provide new, and in some cases more enlightening, demonstrations of the solvability of these classes. A technique for constructing a model for a formula shown satisfiable in this way is also described. © 1976, ACM. All rights reserved.