Constructive canonicity for lattice-based fixed point logics

Willem Conradie; Andrew Craig; Alessandra Palmigiano; Zhiguang Zhao

doi:10.1007/978-3-662-55386-2_7

Constructive canonicity for lattice-based fixed point logics

Willem Conradie, Andrew Craig^*, Alessandra Palmigiano, Zhiguang Zhao

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

Original language	English
Title of host publication	Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings
Editors	Juliette Kennedy, Ruy J.G.B. de Queiroz
Publisher	Springer Verlag
Pages	92-109
Number of pages	18
ISBN (Print)	9783662553855
DOIs	https://doi.org/10.1007/978-3-662-55386-2_7
Publication status	Published - 1 Jan 2017
Externally published	Yes
Event	24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017 - London, United Kingdom Duration: 18 Jul 2017 → 21 Jul 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10388 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017
Country/Territory	United Kingdom
City	London
Period	18/07/17 → 21/07/17

Funding

The research of the first author has been funded by the National Research Foundation of South Africa, Grant number 81309. The research of the third and fourth author has been funded by the NWO Vidi grant 016.138.314, the NWO Aspasia grant 015.008.054, and a Delft Technology Fellowship awarded in 2013.

Funders	Funder number
National Research Foundation	81309
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	015.008.054, 016.138.314

Keywords

Canonicity
Lattice-based fixed point logics
Logics for categorization
Unified correspondence

Access to Document

10.1007/978-3-662-55386-2_7

Persistent URL (handle)

Copy link address

Cite this

Conradie, W., Craig, A., Palmigiano, A., & Zhao, Z. (2017). Constructive canonicity for lattice-based fixed point logics. In J. Kennedy, & R. J. G. B. de Queiroz (Eds.), Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings (pp. 92-109). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10388 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-55386-2_7

Conradie, Willem ; Craig, Andrew ; Palmigiano, Alessandra et al. / Constructive canonicity for lattice-based fixed point logics. Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. editor / Juliette Kennedy ; Ruy J.G.B. de Queiroz. Springer Verlag, 2017. pp. 92-109 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6b966a689d4342d6a07790cc343ff5a1,

title = "Constructive canonicity for lattice-based fixed point logics",

abstract = "In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.",

keywords = "Canonicity, Lattice-based fixed point logics, Logics for categorization, Unified correspondence",

author = "Willem Conradie and Andrew Craig and Alessandra Palmigiano and Zhiguang Zhao",

year = "2017",

month = jan,

day = "1",

doi = "10.1007/978-3-662-55386-2_7",

language = "English",

isbn = "9783662553855",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "92--109",

editor = "Juliette Kennedy and {de Queiroz}, {Ruy J.G.B.}",

booktitle = "Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings",

address = "Germany",

note = "24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017 ; Conference date: 18-07-2017 Through 21-07-2017",

}

Conradie, W, Craig, A, Palmigiano, A & Zhao, Z 2017, Constructive canonicity for lattice-based fixed point logics. in J Kennedy & RJGB de Queiroz (eds), Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10388 LNCS, Springer Verlag, pp. 92-109, 24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017, London, United Kingdom, 18/07/17. https://doi.org/10.1007/978-3-662-55386-2_7

Constructive canonicity for lattice-based fixed point logics. / Conradie, Willem; Craig, Andrew; Palmigiano, Alessandra et al.
Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. ed. / Juliette Kennedy; Ruy J.G.B. de Queiroz. Springer Verlag, 2017. p. 92-109 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10388 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Constructive canonicity for lattice-based fixed point logics

AU - Conradie, Willem

AU - Craig, Andrew

AU - Palmigiano, Alessandra

AU - Zhao, Zhiguang

PY - 2017/1/1

Y1 - 2017/1/1

N2 - In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

AB - In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

KW - Canonicity

KW - Lattice-based fixed point logics

KW - Logics for categorization

KW - Unified correspondence

UR - http://www.scopus.com/inward/record.url?scp=85026733894&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85026733894&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-55386-2_7

DO - 10.1007/978-3-662-55386-2_7

M3 - Conference contribution

AN - SCOPUS:85026733894

SN - 9783662553855

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 92

EP - 109

BT - Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings

A2 - Kennedy, Juliette

A2 - de Queiroz, Ruy J.G.B.

PB - Springer Verlag

T2 - 24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017

Y2 - 18 July 2017 through 21 July 2017

ER -

Conradie W, Craig A, Palmigiano A, Zhao Z. Constructive canonicity for lattice-based fixed point logics. In Kennedy J, de Queiroz RJGB, editors, Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. Springer Verlag. 2017. p. 92-109. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-55386-2_7

Constructive canonicity for lattice-based fixed point logics

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this