Comparison of theorem provers for modal logics - Introduction and summary

Abstract

The Tableaux 98 conference included a comparison of automated theorem provers for some modal logics. Our aim was to make the existing provers better known and to show what possibilities they offer. This comparison included benchmarks for the propositional modal logics K, KT and S4. Although efficiency is an important aspect, depending on the intended application other qualities can be as important, such as portability, construction of counter-models, user-friendliness, or small size. We first discuss our aims in more detail, explain the applied benchmark method, and finally give a short summary of the results. The submissions of the participants follow in alphabetic order. © Springer-Verlag Berlin Heidelberg 1998.