Relations between Propositional Normal Modal Logics: an Overview

The modal logic literature is notorious for multiple axiomatizations of the same logic and for conflicting overloading of axiom names. Many of the interesting interderivability results are still scattered over the often hard to obtain classics. We catalogue the most interesting axioms, their numerous variants, and explore the relationships between them in terms of interderivability as both axiom (schema) and as simple formulae. In doing so we introduce the Logics Workbench (LWB, see http://lwbwww.uniba.ch:8080/LWBinfo.html), a versatile tool for proving theorems in numerous propositional (nonclassical) logics. As a side-effect we fulfill a call from the modal theorem proving community for a database of known theorem