Comparison of various modal theorem provers
In the previous sections we presented only median CPU time graphs for
KSAT and KRIS. In this section we extend our comparison to include
ModLeanTAP, the Logics Workbench, and the translation approach using SPASS.
Furthermore, we present percentile graphs which provide additional insight
into the behaviour of the theorem provers on more difficult formulae.
The following picture show the percentile graphs for
ModLeanTAP*, LWB*, KRIS*, KSAT, the translation approach using SPASS, and
FaCT on the parameter setting PS0 (N=5, M=1, K=3, D=2, P=0.5).
Note that the Logics Workbench, KRIS*, KSAT, and the translation approach
were not allowed to reorder the subformulae of the input formulae in these
experiments.
Top: Contents |
Previous: KSAT versus KRIS: Sorting |
Next: A comparison of modal theorem provers: Sorting
