Algebraic proof theory: hypersequents and hypercompletions

DOI10.1016/j.apal.2016.10.012zbMath1422.03038MaRDI QIDQ730091

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

zbMATH Keywords

substructural logic; residuated lattice; substructural hierarchy; hypersequent calculus; algebraic completion; residuated frame

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03G25: Other algebras related to logic

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

03F03: Proof theory in general (including proof-theoretic semantics)

Related Items

FIBRED ALGEBRAIC SEMANTICS FOR A VARIETY OF NON-CLASSICAL FIRST-ORDER LOGICS AND TOPOLOGICAL LOGICAL TRANSLATION, BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS, MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics, Densification of FL chains via residuated frames, Join-completions of partially ordered algebras, Residuated structures and orthomodular lattices, Hyper-MacNeille completions of Heyting algebras, Hypersequent and display calculi -- a unified perspective, Intermediate logics admitting a structural hypersequent calculus

Cites Work

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