Algorithmic correspondence for intuitionistic modal mu-calculus, Part 1

5 pages•Published: July 28, 2014

Willem Conradie, Yves Fomatati, Alessandra Palmigiano and Sumit Sourabh

Abstract

The algorithmic correspondence theory is extended to mu-calculi with a non-classical base. We focus in particular on the language of bi-intuitionistic modal mu-calculus, and we enhance the algorithm, or calculus for correspondence, ALBA for the elimination of monadic second order variables, so as to guarantee its success over a class including the Sahlqvist mu-formulas. Key to the soundness of this enhancement are the order-theoretic properties of the algebraic interpretation of the fixed point operators.

Keyphrases: algorithmic correspondence, intuitionistic logic, modal mu calculus, sahlqvist correspondence

In: Nikolaos Galatos, Alexander Kurz and Constantine Tsinakis (editors). TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic, vol 25, pages 52-56.

Links:	https://easychair.org/publications/paper/Hw
	https://doi.org/10.29007/vpww

BibTeX entry

@inproceedings{TACL2013:Algorithmic_correspondence_intuitionistic_modal,
  author    = {Willem Conradie and Yves Fomatati and Alessandra Palmigiano and Sumit Sourabh},
  title     = {Algorithmic correspondence for intuitionistic modal mu-calculus, Part 1},
  booktitle = {TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic},
  editor    = {Nikolaos Galatos and Alexander Kurz and Constantine Tsinakis},
  series    = {EPiC Series in Computing},
  volume    = {25},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/Hw},
  doi       = {10.29007/vpww},
  pages     = {52-56},
  year      = {2014}}

Download PDF Open PDF in browser