The following exposition is concerned with the empirical analysis of decision procedure for basic modal logic. One can roughly distinguish five constituents which contribute to the design of a theorem prover procedure

- Calculus,
- Refinement of the calculus,
- Search strategy,
- Heuristic,
- Datastructures and algorithms,

The order of the constituents in this list is derived from their conceptual level. However, the order does not necessarily correspond to the importance of these constituents with respect to the performance of a theorem prover on a particular problem or a particular class of problems.

In the MPII research report 97-2-003 we report on a 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 does not produce challenging unsatisfiable modal formulae. We propose improvements to the random generator and show that the computational behaviour compares favourably with the other three approaches.

The following sections provide a more detailed overview of our results.KSAT versus KRIS: Simplification

Trival satisfiable and trivial unsatisfiable formulae

KSAT versus KRIS: Sorting

A comparison of modal theorem provers

A comparison of modal theorem provers: Sorting

Generating more challenging problems

Guidelines for generating more challenging problems

Revised comparison of modal theorem provers

Semantic versus syntactic branching

References