Cut elimination and strong separation for substructural logics: an algebraic approach

DOI10.1016/J.APAL.2010.01.003MaRDI QIDQ636346zbMATHOpenAlexFDO

Authors Nikolaos Galatos, Hiroakira Ono

Publication date 26 August 2011

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.2010.01.003

zbMATH Keywords

substructural logiccut eliminationresiduated latticeMacNeille completionGentzen systemHilbert systemstrong separation

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25)

Recommendations

• Algebraic proof theory for substructural logics: cut-elimination and completions
• Nonassociative substructural logics and their semilinear extensions: axiomatization and completeness properties
• scientific article; zbMATH DE number 2070197
• scientific article; zbMATH DE number 1138593
• Logics without the contraction rule and residuated lattices

Cites work

• scientific article; zbMATH DE number 440121 (Why is no real title available?)
• scientific article; zbMATH DE number 3751028 (Why is no real title available?)
• scientific article; zbMATH DE number 46487 (Why is no real title available?)
• scientific article; zbMATH DE number 3470465 (Why is no real title available?)
• scientific article; zbMATH DE number 2070197 (Why is no real title available?)
• scientific article; zbMATH DE number 218501 (Why is no real title available?)
• scientific article; zbMATH DE number 1361537 (Why is no real title available?)
• scientific article; zbMATH DE number 1406811 (Why is no real title available?)
• scientific article; zbMATH DE number 1415870 (Why is no real title available?)
• scientific article; zbMATH DE number 2208113 (Why is no real title available?)
• A survey of abstract algebraic logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Algebraic aspects of cut elimination
• Algebraizable logics
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Closure operators and complete embeddings of residuated lattices
• Equivalence of consequence relations: an order-theoretic and categorical perspective
• Finite models of some substructural logics
• Fuzzy logics from substructural perspective
• Generalized MV-algebras
• Glivenko theorems for substructural logics over FL
• Lattice-valued representation of the cut-elimination theorem
• Linear logic
• Logics without the contraction rule
• On Action Logic: Equational Theories of Action Algebras
• On the finite embeddability property for residuated lattices, pocrims and BCK-algebras
• On the finite embeddability property for residuated ordered groupoids
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Relative pseudo-complements, join-extensions, and meet-retractions
• Residuated frames with applications to decidability
• Residuated lattices. An algebraic glimpse at substructural logics
• Rule separation and embedding theorems for logics without weakening
• Sequent-systems and groupoid models. I
• THE STRUCTURE OF RESIDUATED LATTICES
• The finite embeddability property for residuated lattices, pocrims and BCK-algebras.
• The finite model property for BCI and related systems
• The finite model property for various fragments of intuitionistic linear logic
• Untersuchungen über das logische Schliessen. I
• Which structural rules admit cut elimination? An algebraic criterion

Cited in

(31)

• A SUBSTRUCTURAL GENTZEN CALCULUS FOR ORTHOMODULAR QUANTUM LOGIC
• Prelinear algebras in relatively regular quasivarieties
• Hyper-MacNeille completions of Heyting algebras
• Residuated structures and orthomodular lattices
• One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
• The completions of multi-posets and quantum B-algebras
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Residuated expansions of lattice-ordered structures
• Involutive basic substructural core fuzzy logics: involutive mianorm-based logics
• Algebraic proof theory for LE-logics
• An algebraic glimpse at bunched implications and separation logic
• Basic substructural core fuzzy logics and their extensions: mianorm-based logics
• The atomic theory of left division of two-sided ideals of semirings with unit
• Algebraic proof theory: hypersequents and hypercompletions
• An algebraic approach to the disjunction property of substructural logics
• scientific article; zbMATH DE number 2015401 (Why is no real title available?)
• Which structural rules admit cut elimination? An algebraic criterion
• Weakening Relation Algebras and FL$$^2$$-algebras
• Substructural nuclear (image-based) logics and operational Kripke-style semantics
• Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids
• Sequent-systems and groupoid models. I
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Completion and finite embeddability property for residuated ordered algebras.
• Weakening-free, non-associative fuzzy logics: micanorm-based logics
• Some syntactic interpretations in different systems of full Lambek calculus
• Extensions of Lambek calculi
• Undecidability of consequence relation in full non-associative Lambek calculus
• Nonassociative substructural logics and their semilinear extensions: axiomatization and completeness properties
• The monotone Lambek calculus is NP-complete
• Residuated frames with applications to decidability
• scientific article; zbMATH DE number 7547163 (Why is no real title available?)

This page was built for publication: Cut elimination and strong separation for substructural logics: an algebraic approach

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