Cut elimination and strong separation for substructural logics: an algebraic approach
From MaRDI portal
Publication:636346
DOI10.1016/j.apal.2010.01.003zbMath1245.03027MaRDI QIDQ636346
Hiroakira Ono, Nikolaos Galatos
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
Hilbert system; cut elimination; MacNeille completion; substructural logic; residuated lattice; Gentzen system; strong separation
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)
Related Items
Residuated frames with applications to decidability, Unnamed Item, One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity, Extensions of Lambek Calculi, Weakening Relation Algebras and FL$$^2$$-algebras, Some Syntactic Interpretations in Different Systems of Full Lambek Calculus, NONASSOCIATIVE SUBSTRUCTURAL LOGICS AND THEIR SEMILINEAR EXTENSIONS: AXIOMATIZATION AND COMPLETENESS PROPERTIES, The Monotone Lambek Calculus Is NP-Complete, UNDECIDABILITY OF CONSEQUENCE RELATION IN FULL NON-ASSOCIATIVE LAMBEK CALCULUS, A SUBSTRUCTURAL GENTZEN CALCULUS FOR ORTHOMODULAR QUANTUM LOGIC, An algebraic glimpse at bunched implications and separation logic, The atomic theory of left division of two-sided ideals of semirings with unit, Algebraic proof theory for substructural logics: cut-elimination and completions, Basic substructural core fuzzy logics and their extensions: mianorm-based logics, Completion and finite embeddability property for residuated ordered algebras., Weakening-free, non-associative fuzzy logics: micanorm-based logics, Involutive basic substructural core fuzzy logics: involutive mianorm-based logics, The completions of multi-posets and quantum B-algebras, Residuated structures and orthomodular lattices, Hyper-MacNeille completions of Heyting algebras, Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids, Prelinear algebras in relatively regular quasivarieties, Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL, Residuated expansions of lattice-ordered structures
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Residuated lattices. An algebraic glimpse at substructural logics
- Sequent-systems and groupoid models. I
- Lattice-valued representation of the cut-elimination theorem
- Relative pseudo-complements, join-extensions, and meet-retractions
- Closure operators and complete embeddings of residuated lattices
- A survey of abstract algebraic logic
- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- Generalized MV-algebras
- Algebraic aspects of cut elimination
- The finite embeddability property for residuated lattices, pocrims and BCK-algebras.
- Rule separation and embedding theorems for logics without weakening
- Untersuchungen über das logische Schliessen. I
- Fuzzy logics from substructural perspective
- Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
- The finite model property for BCI and related systems
- Finite Models of Some Substructural Logics
- THE STRUCTURE OF RESIDUATED LATTICES
- Equivalence of consequence relations: an order-theoretic and categorical perspective
- Glivenko theorems for substructural logics over FL
- On Action Logic: Equational Theories of Action Algebras
- Logics without the contraction rule
- Algebraizable logics
- Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
- The finite model property for various fragments of intuitionistic linear logic
- Residuated frames with applications to decidability
- Which structural rules admit cut elimination? An algebraic criterion
- On the finite embeddability property for residuated ordered groupoids