Residuated frames with applications to decidability

DOI10.1090/S0002-9947-2012-05573-5zbMath1285.03077MaRDI QIDQ4913809

Nikolaos Galatos, Peter Jipsen

Publication date: 16 April 2013

Published in: Transactions of the American Mathematical Society (Search for Journal in Brave)

zbMATH Keywords

cut eliminationdecidabilitysubstructural logicfinite model propertyresiduated latticeGentzen systemresiduated framefinite embeddability propertyinvolutive residuated structures

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25) Ordered semigroups and monoids (06F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Varieties of lattices (06B20)

Related Items (38)

Canonical formulas for \(k\)-potent commutative, integral, residuated lattices ⋮ Densification of FL chains via residuated frames ⋮ On square-increasing ordered monoids and idempotent semirings ⋮ Relation Algebras, Idempotent Semirings and Generalized Bunched Implication Algebras ⋮ Integrally closed residuated lattices ⋮ The distributivity on bi-approximation semantics ⋮ Changing a Semantics: Opportunism or Courage? ⋮ Categories of Algebraic Contexts Equivalent to Idempotent Semirings and Domain Semirings ⋮ Strong negation in intuitionistic style sequent systems for residuated lattices ⋮ MOST SIMPLE EXTENSIONS OF ARE UNDECIDABLE ⋮ Distributive residuated frames and generalized bunched implication algebras ⋮ The FEP for some varieties of fully distributive knotted residuated lattices ⋮ Relation algebras as expanded FL-algebras ⋮ Algebraic proof theory for substructural logics: cut-elimination and completions ⋮ On involutive nonassociative Lambek calculus ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Finite embeddability property for residuated lattices via regular languages ⋮ Order-dual relational semantics for non-distributive propositional logics: a general framework ⋮ Complemented MacNeille completions and algebras of fractions ⋮ Cut elimination and strong separation for substructural logics: an algebraic approach ⋮ Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity ⋮ Cayley's and Holland's theorems for idempotent semirings and their applications to residuated lattices ⋮ Unnamed Item ⋮ Densification via polynomials, languages, and frames ⋮ From cut-free calculi to automated deduction: the case of bounded contraction ⋮ Implicit and explicit stances in logic ⋮ Word problem for knotted residuated lattices. ⋮ Join-completions of partially ordered algebras ⋮ Completion and finite embeddability property for residuated ordered algebras. ⋮ Algebraic proof theory: hypersequents and hypercompletions ⋮ The completions of multi-posets and quantum B-algebras ⋮ MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics ⋮ Modal translation of substructural logics ⋮ Hyper-MacNeille completions of Heyting algebras ⋮ The structure of generalized BI-algebras and weakening relation algebras ⋮ One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity ⋮ Splittings in varieties of logic ⋮ The finite embeddability property for noncommutative knotted extensions of RL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cut elimination and strong separation for substructural logics: an algebraic approach
• MacNeille completions of FL-algebras
• A Gentzen system for involutive residuated lattices
• Generalized Kripke frames
• Residuated lattices. An algebraic glimpse at substructural logics
• Relative pseudo-complements, join-extensions, and meet-retractions
• 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
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Interpolation and FEP for logics of residuated algebras
• THE STRUCTURE OF RESIDUATED LATTICES
• The finite model property for knotted extensions of propositional linear logic
• Quantales and (noncommutative) linear logic
• Logics without the contraction rule
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• The finite model property for various fragments of intuitionistic linear logic
• Which structural rules admit cut elimination? An algebraic criterion
• On the finite embeddability property for residuated ordered groupoids
• Canonical extensions and relational completeness of some substructural logics

This page was built for publication: Residuated frames with applications to decidability