Residuated frames with applications to decidability

By Nikolaos Galatos, Peter Jipsen. 2012

86 citations recorded by the source corpus.

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. We use our results to prove the decidability of the equational and/or universal theory of several varieties of residuated lattice-ordered groupoids, including the variety of involutive

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/732966a07d3a0044ff62d1fe4c12c1a18a2c5af8