Disjunctive Bases: Normal Forms for Modal Logics

Authors Sebastian Enqvist, Yde Venema

Thumbnail PDF


  • Filesize: 0.59 MB
  • 16 pages

Document Identifiers

Author Details

Sebastian Enqvist
Yde Venema

Cite AsGet BibTex

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)


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.
  • Modal logic
  • fixpoint logic
  • automata
  • coalgebra
  • graded modal logic
  • Lyndon theorem
  • uniform interpolation


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


  1. J. Bergfeld. Moss’s coalgebraic logic: Examples and completeness results. Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2009. Google Scholar
  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. Google Scholar
  3. G. D'Agostino and M. Hollenberg. Logical questions concerning the μ-calculus. Journal of Symbolic Logic, 65:310-332, 2000. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  9. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logic, and Infinite Games, volume 2500 of LNCS. Springer, 2002. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  13. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983. Google Scholar
  14. C. Kupke, A. Kurz, and Y. Venema. Completeness for the coalgebraic cover modality. Logical Methods in Computer Science, 8(3), 2010. Google Scholar
  15. A. Kurz and R. Leal. Modalities in the stone age: a comparison of coalgebraic logics. Theoretical Computer Science, 430:88-116, 2012. Google Scholar
  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). Google Scholar
  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. Google Scholar
  19. D. Pattinson. Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1-3):177-193, 2003. Google Scholar
  20. L. Schröder. Expressivity of coalgebraic modal logic: the limits and beyond. Theoretical Computer Science, pages 230-247, 2008. Google Scholar
  21. Y. Venema. Automata and fixed point logic: a coalgebraic perspective. Information and Computation, 204:637-678, 2006. Google Scholar
  22. Y. Venema. Lectures on the modal μ-calculus. Lecture Notes, ILLC, University of Amsterdam, 2012. Google Scholar
  23. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157:142-182, 2000. Google Scholar