|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 7, Issue 6: December 1997.
Modal tableaux based on residuation
University of Leipzig, Institute of Logic and Philosophy of Science, Augustusplatz 9, 04109 Leipzig, Germany. E-mail: firstname.lastname@example.org
We show that (an analogue 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(=KDAlt1), the modal logic of functional accessibility relations, and PDL-, deterministic propositional dynamic logic without Kleene-star. The method is based on the observation that the tense logical operations [F] (alias [squ]) and [P] form a residuated pair. As a corollary, we obtain a decision procedure for Kf and PDL-.