Enqvist, Sebastian ;
Venema, Yde
Disjunctive Bases: Normal Forms for Modal Logics
Abstract
We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mucalculi. Believing the concept has a much wider significance, here
we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "onestep" level entails a number of good properties for a coalgebraic mucalculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full
fixpoint logic, its fixpointfree fragment and its onestep fragment, and a Uniform Interpolation result, for both the full mucalculus and its fixpointfree fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. Finally, we consider the problem of giving a categorytheoretic formulation of disjunctive
bases, and provide a partial solution.
BibTeX  Entry
@InProceedings{enqvist_et_al:LIPIcs:2017:8035,
author = {Sebastian Enqvist and Yde Venema},
title = {{Disjunctive Bases: Normal Forms for Modal Logics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {11:111:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770330},
ISSN = {18688969},
year = {2017},
volume = {72},
editor = {Filippo Bonchi and Barbara K{\"o}nig},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/8035},
URN = {urn:nbn:de:0030drops80357},
doi = {10.4230/LIPIcs.CALCO.2017.11},
annote = {Keywords: Modal logic, fixpoint logic, automata, coalgebra, graded modal logic, Lyndon theorem, uniform interpolation}
}
17.11.2017
Keywords: 

Modal logic, fixpoint logic, automata, coalgebra, graded modal logic, Lyndon theorem, uniform interpolation 
Seminar: 

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Issue date: 

2017 
Date of publication: 

17.11.2017 