arXiv Analytics

Sign in

arXiv:1710.04628 [cs.LO]AbstractReferencesReviewsResources

Flat modal fixpoint logics with the converse modality

Sebastian Enqvist

Published 2017-10-12Version 1

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.

Related articles: Most relevant | Search more
arXiv:1002.0172 [cs.LO] (Published 2010-02-01, updated 2010-04-15)
Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
arXiv:0812.2390 [cs.LO] (Published 2008-12-12)
Completeness for Flat Modal Fixpoint Logics
arXiv:1401.7234 [cs.LO] (Published 2014-01-28)
Propositional dynamic logic for searching games with errors