Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 7, Issue 6: December 1997.

Modal tableaux based on residuation

H Wansing

University of Leipzig, Institute of Logic and Philosophy of Science, Augustusplatz 9, 04109 Leipzig, Germany. E-mail: wansing@rz.uni-leipzig.de

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-.

Pages 719-731


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_07/Issue_06/070719.sgm.abs.html
Last modification: 16 April 1998.
Copyright© Oxford University Press, 1998.