Document

# Disjunctive Bases: Normal Forms for Modal Logics

## File

LIPIcs.CALCO.2017.11.pdf
• Filesize: 0.59 MB
• 16 pages

## Cite As

Sebastian Enqvist and Yde Venema. Disjunctive Bases: Normal Forms for Modal Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CALCO.2017.11

## 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 mu-calculi. 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 "one-step" level entails a number of good properties for a coalgebraic mu-calculus, 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 fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free 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 category-theoretic formulation of disjunctive bases, and provide a partial solution.
##### Keywords
• Modal logic
• fixpoint logic
• automata
• coalgebra
• Lyndon theorem
• uniform interpolation

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. J. Bergfeld. Moss’s coalgebraic logic: Examples and completeness results. Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2009.
2. C. Cîrstea, C. Kupke, and D. Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus. In E. Grädel and R. Kahle, editors, Computer Science Logic (CSL 2009), volume 5771 of Lecture Notes in Computer Science, pages 179-193. Springer, 2009.
3. G. D'Agostino and M. Hollenberg. Logical questions concerning the μ-calculus. Journal of Symbolic Logic, 65:310-332, 2000.
4. S. Enqvist, F. Seifan, and Y. Venema. Completeness for coalgebraic fixpoint logic. In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of LIPIcs, pages 7:1-7:19, 2016.
5. S. Enqvist, F. Seifan, and Y. Venema. Completeness for μ-calculi: a coalgebraic approach. Technical Report PP-2017-04, Institute for Logic, Language and Computation, Universiteit van Amsterdam, 2017.
6. S. Enqvist and Y. Venema. Disjunctive bases: Normal forms for modal logics. Technical Report PP-2017-05, Institute for Logic, Language and Computation, Universiteit van Amsterdam, 2017. URL: http://www.illc.uva.nl/Research/Publications/Reports/PP-2017-05.text.pdf.
7. G. Fontaine, R. Leal, and Y. Venema. Automata for coalgebras: An approach using predicate liftings. In Automata, Languages and Programming: 37th International Colloquium ICALP'10, volume 6199 of LNCS, pages 381-392. Springer, 2010.
8. G. Fontaine and T. Place. Frame definability for classes of trees in the mu-calculus. In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010), pages 381-392. Springer, 2010.
9. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logic, and Infinite Games, volume 2500 of LNCS. Springer, 2002.
10. D. Janin and G. Lenzi. Relating levels of the mu-calculus hierarchy and levels of the monadic hierarchy. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pages 347-356, 2001.
11. D. Janin and I. Walukiewicz. Automata for the modal μ-calculus and related results. In J. Wiedermann and P. Hájek, editors, Mathematical Foundations of Computer Science 1995, 20th International Symposium (MFCS'95), volume 969 of LNCS, pages 552-562. Springer, 1995.
12. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional μ-calculus w.r.t. monadic second-order logic. In Proceedings of the Seventh International Conference on Concurrency Theory, CONCUR '96, volume 1119 of LNCS, pages 263-277, 1996.
13. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983.
14. C. Kupke, A. Kurz, and Y. Venema. Completeness for the coalgebraic cover modality. Logical Methods in Computer Science, 8(3), 2010.
15. A. Kurz and R. Leal. Modalities in the stone age: a comparison of coalgebraic logics. Theoretical Computer Science, 430:88-116, 2012.
16. J. Marti, F. Seifan, and Y. Venema. Uniform interpolation for coalgebraic fixpoint logic. In Lawrence S. Moss and Pawel Sobocinski, editors, Proceedings of the Sixth Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), volume 35 of LIPIcs, pages 238-252. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://www.dagstuhl.de/dagpub/978-3-939897-84-2.
17. L. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96:277-317, 1999. (Erratum published APAL 99:241-259, 1999).
18. E. Pacuit and S. Salame. Majority logic. In Proceedings of the Ninth International Conference on Principles of Knowledge Representation and Reasoning (KR2004), pages 598-605, 2004.
19. D. Pattinson. Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1-3):177-193, 2003.
20. L. Schröder. Expressivity of coalgebraic modal logic: the limits and beyond. Theoretical Computer Science, pages 230-247, 2008.
21. Y. Venema. Automata and fixed point logic: a coalgebraic perspective. Information and Computation, 204:637-678, 2006.
22. Y. Venema. Lectures on the modal μ-calculus. Lecture Notes, ILLC, University of Amsterdam, 2012.
23. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157:142-182, 2000.
X

Feedback for Dagstuhl Publishing