Modal Tableaux Based on Residuation
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.