C. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet (2001): ``Resolution decision procedures.'' In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pp. 1791-1850. Elsevier.
Abstract, BibTeX, PDF (© Elsevier).

J. H. Joyner [1973] showed in his thesis that resolution an be turned into a decision procedure for many classes of clause sets that correspond to classical solvable classes. On the basis of Joyner's approach we present resolution as decision procedure; that means we systematically investigate resolution refinements with respect to their potential as decision proedures.