Algebraic proof theory: hypersequents and hypercompletions

DOI10.1016/J.APAL.2016.10.012MaRDI QIDQ730091zbMATH OpenOpenAlexFDO

Authors Agata Ciabattoni, Nikolaos Galatos, Kazushige Terui

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

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)

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

Cites work

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

Cited in

(13)

• Intermediate logics admitting a structural hypersequent calculus
• Unilinear residuated lattices: axiomatization, varieties and FEP
• Densification of FL chains via residuated frames
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Join-completions of partially ordered algebras
• 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
• Fibred algebraic semantics for a variety of non-classical first-order logics and topological logical translation
• 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)