Modal tableaux based on residuation
Heinrich Wansing · Journal of Logic and Computation · 1997
We show that (an 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 (= KDAltl), the modal logic of functional accessibility relations, and PDL-, deterministic prepositional dynamic logic without Kleene-star. The method is based on the observation that the tense logical operations [F] (alias □) and (P) form a residuated pair. As a corollary, we obtain a decision procedure for Kf and PDL-.