Distributive residuated frames and generalized bunched implication algebras

DOI10.1007/s00012-017-0456-xzbMath1420.03139OpenAlexW2761182803MaRDI QIDQ1686325

Peter Jipsen, Nikolaos Galatos

Publication date: 21 December 2017

Published in: Algebra Universalis (Search for Journal in Brave)

Full work available at URL: https://digitalcommons.chapman.edu/scs_articles/547

zbMATH Keywords

cut eliminationdecidabilitysubstructural logicfinite model propertyresiduated latticeGentzen systemresiduated framefinite embeddability property

Mathematics Subject Classification ID

Lattices of varieties (08B15) Logical aspects of lattices and related structures (03G10) Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Related Items

The convolution algebra, Weakening Relation Algebras and FL$$^2$$-algebras, The FEP for some varieties of fully distributive knotted residuated lattices, Deciding Equations in the Time Warp Algebra, Representable and diagonally representable weakening relation algebras, An algebraic glimpse at bunched implications and separation logic, Unnamed Item, Join-completions of partially ordered algebras, Unnamed Item, Unnamed Item, Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids, The structure of generalized BI-algebras and weakening relation algebras

Cites Work

• Algebraic proof theory for substructural logics: cut-elimination and completions
• MacNeille completions of FL-algebras
• Generalized Kripke frames
• Residuated lattices. An algebraic glimpse at substructural logics
• Distributive full Lambek calculus has the finite model property
• The FEP for some varieties of fully distributive knotted residuated lattices
• Cayley's and Holland's theorems for idempotent semirings and their applications to residuated lattices
• The semantics and proof theory of the logic of bunched implications
• The semantics of BI and resource tableaux
• Residuated frames with applications to decidability
• On the finite embeddability property for residuated ordered groupoids