@INCOLLECTION{Fermueller+Leitsch+Hustadt+Tammet@HAR2001,
 AUTHOR        = {Ferm{\"u}ller, Christian and Leitsch, Alexander and Hustadt, Ullrich and Tammet, Tanel},
 TITLE         = {Resolution Decision Procedures},
 EDITOR        = {Robinson, Alan and Voronkov, Andrei},
 BOOKTITLE     = {Handbook of Automated Reasoning},
 PUBLISHER     = {Elsevier}, 
 YEAR          = {2001},
 PAGES         = {1791-1850},
 CHAPTER       = {25},
 URL           = {Fermueller+Leitsch+Hustadt+Tammet@HAR2001},
 ABSTRACT      = {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.}
}