@inproceedings{6ff02709cfe2438da64afa70aeb7f5c1,
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 = "Lattice logic, substructural logic, algebraic proof theory, sequent calculi, cut elimination, display calculi, multi-type calculi",
author = "G. Greco and Alessandra Palmigiano",
year = "2017",
doi = "10.1007/978-3-662-55386-2\_11",
language = "English",
isbn = "978-3-662-55385-5",
volume = "10388",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "153--169",
booktitle = "Logic, Language, Information, and Computation (WoLLIC 2017)",
edition = "LNCS",
}