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 -