Algebraic proof theory: hypersequents and hypercompletions

DOI10.1016/j.apal.2016.10.012zbMath1422.03038OpenAlexW2534514413MaRDI 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 logicresiduated latticesubstructural hierarchyhypersequent calculusalgebraic completionresiduated frame

Mathematics Subject Classification ID

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

Related Items

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

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