Flat modal fixpoint logics with the converse modality

DOI10.1093/LOGCOM/EXY016zbMATH Open1444.03051arXiv1710.04628OpenAlexW2964150129WikidataQ129836157 ScholiaQ129836157MaRDI QIDQ4612435FDOQ4612435

Authors: Sebastian Enqvist 

Publication date: 31 January 2019

Published in: Journal Of Logic And Computation (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1710.04628

Recommendations

• Completeness for flat modal fixpoint logics
• Completeness for Flat Modal Fixpoint Logics
• Modal fixed point logics

zbMATH Keywords

networkcompletenessmu-calculusconverse modalitymodal fixpoint logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70)

Cited In (3)

• Completeness for Flat Modal Fixpoint Logics
• Completeness for flat modal fixpoint logics
• The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games

This page was built for publication: Flat modal fixpoint logics with the converse modality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4612435)