@TECHREPORT{HustadtSchmidt97,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
MONTH = {February},
YEAR = {1997},
TITLE = {On Evaluating Decision Procedures for Modal Logics},
TYPE = {Technical Report},
NUMBER = {MPI-I-97-2-003},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken, Germany},
NOTE = {The short version is to apear in \emph{Proc.\ IJCAI'97}.},
ABSTRACT = {This paper reports on empirical performance analysis of four modal
theorem provers on benchmark suites of randomly generated formulae. 
The theorem provers tested are
the Davis-Putnam-based procedure \textsc{ksat}, the
tableaux-based system $\cal KRIS$,
the sequent-based Logics Workbench, 
and a translation approach combined with the first-order theorem
prover \textsc{spass}.

Our benchmark suites are sets of multi-modal formulae in a certain
normal form randomly generated according to the scheme of 
Giunchiglia and Sebastiani~(1996a,b).
We investigate the quality of the random modal formulae and show that
the scheme has some shortcomings, which may lead to mistaken conclusions.
We propose improvements to the evaluation method 
and show that the translation approach has superior
computational behaviour compared to the other three approaches.}
}