Lattice logic properly displayed

Giuseppe Greco*, Alessandra Palmigiano

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationLogic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings
EditorsJuliette Kennedy, Ruy J.G.B. de Queiroz
PublisherSpringer Verlag
Pages153-169
Number of pages17
ISBN (Print)9783662553855
DOIs
Publication statusPublished - 1 Jan 2017
Externally publishedYes
Event24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017 - London, United Kingdom
Duration: 18 Jul 201721 Jul 2017

Publication series

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

Conference

Conference24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017
CountryUnited Kingdom
CityLondon
Period18/07/1721/07/17

Keywords

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

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

Cite this