LWB

Relations between propositional normal modal logics: An overview. In this short paper the authors give a useful overview of the most common propositional normal modal logics by first providing a catalogue of their axioms (and of the alternative names that have been considered in the standard textbooks, papers and reports), and then investigating the relationships between the logics; the equivalence between multiple axiomatizations of a logic is established by showing the interderivability of the different axioms. In doing so, the authors introduce the Logics Workbench LWB, a theorem prover for propositional modal and other nonclassical logics. A pleasant side effect of their work is the fact that their catalogue of axioms provides a database of theorems that can be used as a basic benchmark for testing and comparing the performance of different theorem provers for modal logics.