From the authors’ introduction: “In this paper we introduce residuated frames and show that they provide relational semantics for substructural logics and representations for residuated structures. Our approach is driven by the applications of the theory. As is the case with Kripke frames for modal logics, residuated frames provide a valuable tool for solving both algebraic and logical problems. Moreover, we show that there is a direct link between Gentzen-style sequent calculi and our residuated frames, which gives insight into the connection between a cut-free proof system and the finite embeddability property for the corresponding variety of algebras.”
Residuated frames are a natural generalisation of such tools as Kripke frames and phase spaces.
The authors present a common generalization of various known results on the cut-elimination property for several logical systems, decidability, the finite model property and the finite embeddability property, and use their generalization to obtain new results concerning the two latter properties. They apply the techniques of residuated frames also to prove new positive results about involutive residuated structures.