On Evaluating Decision Procedures for Modal Logics

Hustadt, U. and Schmidt, R. A. (Feb. 1997)

Research Report MPI-I-97-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany. PostScript, BiBTeX

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 KSAT, the tableaux-based system KRIS, the sequent-based Logics Workbench, and a translation approach combined with the first-order theorem prover 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,1996b). 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.

The short version is to appear in the Proc. IJCAI'97.

Some pictures and the routines for the random generation of modal formulae, the functional translation and simplification can be found on the page: Empirical analysis of decision procedures for modal logic.

Renate A. Schmidt
Home | Publications | FM Group | School | Man Univ

Last modified: 27 Apr 2001
Copyright © 1996,7,8 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk