Algorithmic correspondence and canonicity for distributive modal logic

Willem Conradie; Alessandra Palmigiano

doi:10.1016/j.apal.2011.10.004

Algorithmic correspondence and canonicity for distributive modal logic

Willem Conradie^*
, Alessandra Palmigiano

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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 language	English
Pages (from-to)	338-376
Number of pages	39
Journal	Annals of Pure and Applied Logic
Volume	163
Issue number	3
DOIs	https://doi.org/10.1016/j.apal.2011.10.004
Publication status	Published - 1 Mar 2012
Externally published	Yes

Funding

The research of the first author was supported by grant number 70554 of the National Research Foundation of South Africa. The research of the second author was supported by the VENI grant 639.031.726 of the Netherlands Organization for Scientific Research (NWO). We would also like to thank the anonymous reviewer for a very thorough reading and insightful comments which led to improvement of the paper.

Keywords

Algorithmic correspondence
Canonicity
Distributive lattices
Modal logic
Sahlqvist correspondence

Access to Document

10.1016/j.apal.2011.10.004

Persistent URL (handle)

Persistent link

Cite this

@article{02c32d97b92e404397e4400c4e9c9c12,

title = "Algorithmic correspondence and canonicity for distributive modal logic",

abstract = "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.",

keywords = "Algorithmic correspondence, Canonicity, Distributive lattices, Modal logic, Sahlqvist correspondence",

author = "Willem Conradie and Alessandra Palmigiano",

year = "2012",

month = mar,

day = "1",

doi = "10.1016/j.apal.2011.10.004",

language = "English",

volume = "163",

pages = "338--376",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier B.V.",

number = "3",

}

TY - JOUR

T1 - Algorithmic correspondence and canonicity for distributive modal logic

AU - Conradie, Willem

AU - Palmigiano, Alessandra

PY - 2012/3/1

Y1 - 2012/3/1

N2 - 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.

AB - 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.

KW - Algorithmic correspondence

KW - Canonicity

KW - Distributive lattices

KW - Modal logic

KW - Sahlqvist correspondence

UR - https://www.scopus.com/pages/publications/84855211208

UR - https://www.scopus.com/pages/publications/84855211208#tab=citedBy

U2 - 10.1016/j.apal.2011.10.004

DO - 10.1016/j.apal.2011.10.004

M3 - Article

AN - SCOPUS:84855211208

SN - 0168-0072

VL - 163

SP - 338

EP - 376

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 3

ER -

Algorithmic correspondence and canonicity for distributive modal logic

Abstract

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this