, R. Gore and W. Heinle 1 A. Heuerding 1 Automated Reasoning Project, Australian National University,and Canberra, Australia. E-mail: email@example.com 1IAM, University of Bern, Switzerland. E-mail: heinle,firstname.lastname@example.org
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.unibe.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
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Part of the OUP Journals World Wide Web service.
Last modification: 24 Oct 1997
Copyright© Oxford University Press, 1997.