No label defined (Q4942004)

The author presents a proof-theoretic approach to the decision problem based on the resolution principle. It is the purpose of the paper to show that resolution-based theorem provers can be used not only for producing proofs for sentences but they can also be used as decision procedures. The author shows that \(A\)-ordering refinement is a decision procedure for the one-variable class and the monadic class. Most of the classical decidable classes (Maslov's Krom class, Skolem class etc.) can be decided in a similar way. Another refinement of the resolution principle is hyperresolution. The author shows that for any positively \(\alpha\)-dominated class (where \(\alpha\) is some atom complexity measure), hyperresolution is a decision procedure. For the entire collection see [Zbl 0927.00020].