Algorithmic correspondence and canonicity for distributive modal logic

Willem Conradie*, Alessandra Palmigiano

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


We define the algorithm ALBA for the language of the same distributive modal logic (DML) for which a Sahlqvist theorem was proved by Gehrke, Nagahashi, and Venema. Successful executions of ALBA compute the local first-order correspondents of input DML inequalities, and also guarantee their canonicity. The class of inequalities on which ALBA is successful is strictly larger than the newly introduced class of inductive inequalities, which in its turn properly extends the Sahlqvist inequalities of Gehrke etal. Evidence is given to the effect that, as their name suggests, inductive inequalities are the distributive counterparts of the inductive formulas of Goranko and Vakarelov in the classical setting.

Original languageEnglish
Pages (from-to)338-376
Number of pages39
JournalAnnals of Pure and Applied Logic
Issue number3
Publication statusPublished - 1 Mar 2012
Externally publishedYes


  • Algorithmic correspondence
  • Canonicity
  • Distributive lattices
  • Modal logic
  • Sahlqvist correspondence

Fingerprint Dive into the research topics of 'Algorithmic correspondence and canonicity for distributive modal logic'. Together they form a unique fingerprint.

Cite this