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

DOI10.1016/J.APAL.2010.01.003zbMATH Open1245.03027OpenAlexW2073214104MaRDI QIDQ636346FDOQ636346

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

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

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)

Cites Work

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

Cited In (31)

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

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)