Volume 7: January - December 1997

Issue 5: October 1997


Relations between propositional normal modal logics: an overview

  • Relations between propositional normal modal logics: an overview
  • R. Gore, W. Heinle1 and A. Heuerding1

    Automated Reasoning Project, Australian National University, Canberra, Australia. E-mail: rpg@arp.anu.edu.au and 1IAM, University of Bern, Switzerland. E-mail: heinle,heuerd@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.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

    Pages: 649 - 658

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    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.