Lattice Logic Properly Displayed
Giuseppe Greco, Alessandra Palmigiano

TL;DR
This paper presents a new display calculus for non-distributive Lattice Logic that ensures soundness, completeness, and cut-elimination, leveraging algebraic and order-theoretic insights with a multi-type approach.
Contribution
It introduces a proper display calculus with closure under uniform substitution, facilitating a Belnap-style proof of cut-elimination for lattice logic.
Findings
The calculus is sound and complete.
It enjoys cut-elimination and sub-formula property.
Properness allows for smooth proof transformations.
Abstract
We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and sub-formula 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. 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies · Advanced Database Systems and Queries · Logic, Reasoning, and Knowledge
