A Benchmark Method for the Propositional Modal Logics K, KT, S4

A lot of methods have been proposed -- and sometimes implemented -- for proof search in the propositional modal logics K, KT, and S4. It is difficult to compare the usefulness of these methods in practice, since in most cases no or only a few execution times have been published. We try to improve this unsatisfactory situation by presenting a set of benchmark formulas. Note that we do not just list formulas, but give a method that allows to compare different provers today and in the future. As a starting point we give the results we obtained when we applied this benchmark method to the Logics Workbench (LWB). We hope that the discussion of postulates concerning ATP benchmark helps to obtain improved benchmark methods for other logics, too.

• Type: Journal
• Year: 2000
• Where: JAR
• Authors: Peter Balsiger, Alain Heuerding, Stefan Schwendimann
• Keywords: Execution Times, JAR 2000, Proof Search, Propositional Modal Logics