Flat modal fixpoint logics with the converse modality
Abstract
We prove a generic completeness result for a class of modal fixpoint logics corresponding to flat fragments of the two-way mu-calculus, extending earlier work by Santocanale and Venema. We observe that Santocanale and Venema's proof that least fixpoints in the Lindenbaum-Tarski algebra of certain flat fixpoint logics are constructive, using finitary adjoints, no longer works when the converse modality is introduced. Instead, our completeness proof directly constructs a model for a consistent formula, using the induction rule in a way that is similar to the standard completeness proof for propositional dynamic logic. This approach is combined with the concept of a focus, which has previously been used in tableau based reasoning for modal fixpoint logics.
Keywords
Cite
@article{arxiv.1710.04628,
title = {Flat modal fixpoint logics with the converse modality},
author = {Sebastian Enqvist},
journal= {arXiv preprint arXiv:1710.04628},
year = {2017}
}