Lattice logic properly displayed

Giuseppe Greco; Alessandra Palmigiano

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

Lattice logic properly displayed

Giuseppe Greco^*, Alessandra Palmigiano

^*Corresponding author for this work

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

Abstract

We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination, and for the most comprehensive account of axiomatic extensions and expansions of Lattice Logic in a single overarching framework. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.

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	153-169
Number of pages	17
ISBN (Print)	9783662553855
DOIs	https://doi.org/10.1007/978-3-662-55386-2_11
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	United Kingdom
City	London
Period	18/07/17 → 21/07/17

Keywords

Algebraic proof theory
Cut elimination
Display calculi
Lattice logic
Multi-type calculi
Sequent calculi
Substructural logics

Access to Document

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

Fingerprint Dive into the research topics of 'Lattice logic properly displayed'. Together they form a unique fingerprint.

Cite this

Greco, G., & Palmigiano, A. (2017). Lattice logic properly displayed. In J. Kennedy, & R. J. G. B. de Queiroz (Eds.), Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings (pp. 153-169). (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_11

Greco, Giuseppe ; Palmigiano, Alessandra. / Lattice logic properly displayed. Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. editor / Juliette Kennedy ; Ruy J.G.B. de Queiroz. Springer Verlag, 2017. pp. 153-169 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6a6021e8f0224fde867841eb92d9ee6f,

title = "Lattice logic properly displayed",

abstract = "We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination, and for the most comprehensive account of axiomatic extensions and expansions of Lattice Logic in a single overarching framework. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.",

keywords = "Algebraic proof theory, Cut elimination, Display calculi, Lattice logic, Multi-type calculi, Sequent calculi, Substructural logics",

author = "Giuseppe Greco and Alessandra Palmigiano",

year = "2017",

month = jan,

day = "1",

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

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 = "153--169",

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",

}

Greco, G & Palmigiano, A 2017, Lattice logic properly displayed. 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. 153-169, 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_11

Lattice logic properly displayed. / Greco, Giuseppe ; Palmigiano, Alessandra.

Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. ed. / Juliette Kennedy; Ruy J.G.B. de Queiroz. Springer Verlag, 2017. p. 153-169 (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 - Lattice logic properly displayed

AU - Greco, Giuseppe

AU - Palmigiano, Alessandra

PY - 2017/1/1

Y1 - 2017/1/1

N2 - We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination, and for the most comprehensive account of axiomatic extensions and expansions of Lattice Logic in a single overarching framework. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.

AB - We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and subformula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination, and for the most comprehensive account of axiomatic extensions and expansions of Lattice Logic in a single overarching framework. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.

KW - Algebraic proof theory

KW - Cut elimination

KW - Display calculi

KW - Lattice logic

KW - Multi-type calculi

KW - Sequent calculi

KW - Substructural logics

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

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

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

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

M3 - Conference contribution

AN - SCOPUS:85026736775

SN - 9783662553855

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

SP - 153

EP - 169

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 -

Greco G , Palmigiano A. Lattice logic properly displayed. In Kennedy J, de Queiroz RJGB, editors, Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings. Springer Verlag. 2017. p. 153-169. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-55386-2_11