© 1997 by Oxford University Press
Original Articles |
Relations between Propositional Normal Modal Logics: an Overview
1Automated Reasoning Project, Australian National University Canberra, Australia E-mail: rpg{at}arp.anu.edu.au
2IAM, University of Bern Switzerland E-mail: heinleheuerd{at}iam.unibe.ch
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 theorems.
Keywords: Modal logic; automated theorem proving; sequent calculi; Logics Workbench