@INPROCEEDING{HustadtSchmidt97b,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
MONTH = {August},
YEAR = {1997},
TITLE = {On Evaluating Decision Procedures for Modal Logics},
EDITOR = {Pollack, M.},
BOOKTITLE = {Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97)},
VOLUME = {1},
PUBLISHER = {Morgan Kaufmann},
PAGES = {202--207},
NOTE = {The long version is available as Research Report
MPI-I-97-2-003, Max-Planck-Institut f{\"u}r Informatik,
Saarbr{\"u}cken, Germany.},
ABSRTACT = {This paper investigates the evaluation method of decision procedures
for multi-modal logic proposed by Giunchiglia and
Sebastiani as an adaptation 
from the evaluation method of Mitchell {\em et al.}\ of 
decision procedures for propositional logic. 
We compare three different theorem proving approaches, namely,
the Davis-Putnam-based procedure \KSAT\@, the tableaux-based
system $\cal KRIS$
and a translation approach combined with first-order resolution. 
Our
results do not support the claims of Giunchiglia and Sebastiani 
concerning the computational superiority of {\sc Ksat} 
over $\cal KRIS$,
and an easy-hard-easy pattern for randomly generated modal formulae.},
}