Algebraic proof theory: hypersequents and hypercompletions

DOI10.1016/J.APAL.2016.10.012zbMATH Open1422.03038OpenAlexW2534514413MaRDI QIDQ730091FDOQ730091

Nikolaos Galatos, Kazushige Terui, Agata Ciabattoni

Publication date: 23 December 2016

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2016.10.012

Recommendations

• Algebraic proof theory for substructural logics: cut-elimination and completions
• scientific article; zbMATH DE number 2196598
• Algebraic aspects of cut elimination
• MacNeille completions of FL-algebras
• Cut elimination and strong separation for substructural logics: an algebraic approach

zbMATH Keywords

substructural logicresiduated latticesubstructural hierarchyhypersequent calculusalgebraic completionresiduated frame

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25)

Cites Work

• Display logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• A unified semantic framework for fully structural propositional sequent systems
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Residuated frames with applications to decidability
• Substructural fuzzy logics
• MacNeille completions of FL-algebras
• Zur Kennzeichnung der Dedekind-MacNeilleschen Hülle einer geordneten Menge
• Residuated lattices. An algebraic glimpse at substructural logics
• THE STRUCTURE OF RESIDUATED LATTICES
• The proof by cases property and its variants in structural consequence relations
• Title not available (Why is that?)
• Bounded Proofs and Step Frames
• Logic Programming with Focusing Proofs in Linear Logic
• From Frame Properties to Hypersequent Rules in Modal Logics
• Title not available (Why is that?)
• The bounded proof property via step algebras and step frames
• Towards a semantic characterization of cut-elimination
• Equational bases for joins of residuated-lattice varieties
• Title not available (Why is that?)
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Algorithmic correspondence and canonicity for distributive modal logic
• Hypersequents, logical consequence and intermediate logics for concurrency
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• Algebraic aspects of cut elimination
• MacNeille completions of lattice expansions
• Title not available (Why is that?)
• A constructive analysis of RM
• Title not available (Why is that?)
• Completions of GBL-algebras: negative results
• A note on the substructural hierarchy
• Power and Limits of Structural Display Rules

Cited In (12)

• Intermediate logics admitting a structural hypersequent calculus
• Unilinear residuated lattices: axiomatization, varieties and FEP
• Densification of FL chains via residuated frames
• Join-completions of partially ordered algebras
• FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION
• MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics
• BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS
• Hypersequent and display calculi -- a unified perspective
• Hyper-MacNeille completions of Heyting algebras
• Residuated structures and orthomodular lattices
• Expanding the Realm of Systematic Proof Theory
• Semiconic idempotent logic. I: Structure and local deduction theorems.

This page was built for publication: Algebraic proof theory: hypersequents and hypercompletions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q730091)