- Algorithmic correspondence for intuitionistic modal mu-caculus
- Theoretical Computer Science
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
In the present paper, the algorithmic correspondence theory developed in Conradie and Palmigiano  is extended to mu-calculi with a non-classical base. We focus in particular on the language of bi-intuitionistic modal mu-calculus. We enhance the algorithm ALBA introduced in Conradie and Palmigiano  so as to guarantee its success on the class of recursive mu-inequalities, which we introduce in this paper. Key to the soundness of this enhancement are the order-theoretic properties of the algebraic interpretation of the fixed point operators. We show that, when restricted to the Boolean setting, the recursive mu-inequalities coincide with the “Sahlqvist mu-formulas” defined in van Benthem, Bezhanishvili and Hodkinson .
- go to publisher's site
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.