MPI-I-97-2-003

On evaluating decision procedures for modal logic

Hustadt, Ullrich and Schmidt, Renate A.

MPI-I-97-2-003. February 1997, 50 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.

Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.	Attachement Size(s):
	878 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-003

BibTeX
@TECHREPORT{HustadtSchmidt97, AUTHOR = {Hustadt, Ullrich and Schmidt, Renate A.}, TITLE = {On evaluating decision procedures for modal logic}, TYPE = {Research Report}, INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik}, ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany}, NUMBER = {MPI-I-97-2-003}, MONTH = {February}, YEAR = {1997}, ISSN = {0946-011X},}