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).

Percentile graphs for ModLeanTAP on PS0 Percentile graphs for LWB* on PS0
Percentile graphs for KRIS* on PS0 Percentile graphs for KSAT on PS0
Percentile graphs for TA* on PS0 Percentile graphs for FaCT on PS0

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
[an error occurred while processing this directive]