de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

On evaluating decision procedures for modal logic

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44660

Hustadt,  Ullrich
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45401

Schmidt,  Renate A.
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

1997-2-003
(Any fulltext), 10KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Hustadt, U., & Schmidt, R. A.(1997). On evaluating decision procedures for modal logic (MPI-I-1997-2-003). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-9B6F-5
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 K\textsc{sat}, the tableaux-based system $\mathcal{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.