Constructive canonicity for lattice-based fixed point logics

Willem Conradie, Andrew Craig*, Alessandra Palmigiano, Zhiguang Zhao

*Corresponding author for this work

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

10 Citations (Scopus)

Abstract

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

Original languageEnglish
Title of host publicationProceedings of Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017
PublisherSpringer
Pages92-109
Number of pages18
Volume10388 LNCS
ISBN (Print)9783662553855
DOIs
Publication statusPublished - 2017
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)03029743
ISSN (Electronic)16113349

Conference

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

Keywords

  • Canonicity
  • Lattice-based fixed point logics
  • Logics for categorization
  • Unified correspondence

Fingerprint

Dive into the research topics of 'Constructive canonicity for lattice-based fixed point logics'. Together they form a unique fingerprint.

Cite this