Deciding the unguarded modal -calculus

Journal of Applied Non-Classical Logics 23 (4):353-371 (2013)
  Copy   BIBTEX

Abstract

The modal -calculus extends basic modal logic with second-order quantification in terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete. Decision procedures for the modal -calculus are not easy to obtain though since the arbitrary nesting of fixpoint constructs requires some combinatorial arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g., explicitly require formulas to be in guarded normal form. In this paper we present a tableau calculus for deciding satisfiability of arbitrary, i.e., not necessarily guarded -calculus formulas. It is based on a new unfolding rule for greatest fixpoint formulas which allows unguarded formulas to be handled without an explicit transformation into guarded form, thus avoiding a exponential blow-up in formula size. We prove soundness and completeness of the calculus, and compare it empirically to using guarded transformation instead. The new unfolding rule can also be used to handle nested star operators in PDL formulas correctly.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The modal object calculus and its interpretation.Edward N. Zalta - 1997 - In M. de Rijke (ed.), Advances in Intensional Logic. Kluwer Academic Publishers. pp. 249--279.
The Situation Calculus: A Case for Modal Logic. [REVIEW]Gerhard Lakemeyer - 2010 - Journal of Logic, Language and Information 19 (4):431-450.
Probability: A new logico-semantical approach. [REVIEW]Christina Schneider - 1994 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 25 (1):107 - 124.
Power and weakness of the modal display calculus.Marcus Kracht - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers. pp. 93--121.

Analytics

Added to PP
2013-11-27

Downloads
17 (#742,366)

6 months
1 (#1,042,085)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations