An Empirical Analysis of Modal Theorem Provers

Hustadt, Ullrich; Schmidt, Renate A.

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Journal Article

An Empirical Analysis of Modal Theorem Provers

MPS-Authors

/persons/resource/persons44660

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

/persons/resource/persons45401

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Hustadt, U., & Schmidt, R. A. (1999). An Empirical Analysis of Modal Theorem Provers. Journal of Applied Non-Classical Logics, 9(4), 479-522.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-3622-5

Abstract

This paper reports on an 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~[CADE96,KR96]. 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 provides a viable alternative to the other approaches.