Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 3 of 3
Full-Text Articles in Algebra
The Structure Of Generalized Bi-Algebras And Weakening Relation Algebras, Nikolaos Galatos, Peter Jipsen
The Structure Of Generalized Bi-Algebras And Weakening Relation Algebras, Nikolaos Galatos, Peter Jipsen
Mathematics, Physics, and Computer Science Faculty Articles and Research
Generalized bunched implication algebras (GBI-algebras) are defined as residuated lattices with a Heyting implication, and are positioned between Boolean algebras with operators and lattices with operators. We characterize congruences on GBI-algebras by filters that are closed under Gumm–Ursini terms, and for involutive GBI-algebras these terms simplify to a dual version of the congruence term for relation algebras together with two more terms. We prove that representable weakening relation algebras form a variety of cyclic involutive GBI-algebras, denoted by RWkRA, containing the variety of representable relation algebras. We describe a double-division conucleus construction on residuated lattices and on (cyclic involutive) GBI-algebras …
Distributive Residuated Frames And Generalized Bunched Implication Algebras, Nikolaos Galatos, Peter Jipsen
Distributive Residuated Frames And Generalized Bunched Implication Algebras, Nikolaos Galatos, Peter Jipsen
Mathematics, Physics, and Computer Science Faculty Articles and Research
We show that all extensions of the (non-associative) Gentzen system for distributive full Lambek calculus by simple structural rules have the cut elimination property. Also, extensions by such rules that do not increase complexity have the finite model property, hence many subvarieties of the variety of distributive residuated lattices have decidable equational theories. For some other extensions, we prove the finite embeddability property, which implies the decidability of the universal theory, and we show that our results also apply to generalized bunched implication algebras. Our analysis is conducted in the general setting of residuated frames.
Residuated Frames With Applications To Decidability, Nikolaos Galatos, Peter Jipsen
Residuated Frames With Applications To Decidability, Nikolaos Galatos, Peter Jipsen
Mathematics, Physics, and Computer Science Faculty Articles and Research
Residuated frames provide relational semantics for substructural logics and are a natural generalization of Kripke frames in intuitionistic and modal logic, and of phase spaces in linear logic. We explore the connection between Gentzen systems and residuated frames and illustrate how frames provide a uniform treatment for semantic proofs of cut-elimination, the finite model property and the finite embeddability property, which imply the decidability of the equational/universal theories of the associated residuated lattice-ordered groupoids. In particular these techniques allow us to prove that the variety of involutive FL-algebras and several related varieties have the finite model property.