Modal Tableaux Based on Residuation

  • Heinrich Wansing
Part of the Trends in Logic book series (TREN, volume 3)


We consider the extent to which an analogue of the familiar notion of clause can be used for modal tableaux, and show that in DL a straightforward anlogue of the ordinary notion of clause rather than a notion of modal clause can be used in complete tableau calculi for the modal logic Kf (= KDA1t1) the modal logic of functional accessibility relations, and PDL , deterministic propositional dynamic logic without Kleene-star. As a corollary, we obtain a decision procedure for Kf and PDL .


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 1998

Authors and Affiliations

  • Heinrich Wansing
    • 1
  1. 1.Institute of Logic and Philosophy of ScienceUniversity of LeipzigLeipzigGermany

Personalised recommendations