@INCOLLECTION{FLHT01,
 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},
}