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.
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
- the absence of the simplification preprocessing routine and
- the absence of suitable heuristics for the application of their branching rule.
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
