A comparison of modal theorem provers: Sorting

The following pictures show the percentile graphs for the Logics Workbench, KRIS*, and KsatLISP and KsatC enhanced by the sorting techniques described before on the parameter setting PS0.

Percentile graphs for LWB* with reordering on PS0 Percentile graphs for KRIS* with reordering on PS0
Percentile graphs for KsatLISP with reordering on PS0 Percentile graphs for KsatC with reordering on PS0
Note the significantly improved performance of the Logics Workbench and KRIS*. These experiments illustrate that the major causes for the bad performance of decision procedures based on analytic tableaux calculi and Gentzen-style calculi for modal logic we observe on the randomly generated modal formulae are

It is worthwile to point out that for ratios L/N between 6 and 20 the median CPU time performance of KsatC is worse than the median CPU time performance of the Logic Workbench with reordering. For L/N=19, the ratio for which about 50% of the sample formulae are satisfiable, the Logics Workbench is about nine times faster than KsatC, that is, almost one order of magnitude.
Top: Contents | Previous: A comparison of modal theorem provers | Next: Generating more challenging problems
[an error occurred while processing this directive]