Proof Systems for Two-Way Modal Mu-Calculus

Journal of Symbolic Logic:1-50 (forthcoming)
  Copy   BIBTEX


We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.



    Upload a copy of this work     Papers currently archived: 94,439

External links

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

Through your library


Added to PP

14 (#1,013,076)

6 months
8 (#528,231)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Yde Venema
University of Amsterdam

Citations of this work

No citations found.

Add more citations