Relations and non-commutative linear logic Original Research Article

We present a sequent calculus for non-commutative intuitionistic linear logic. We prove cut elimination for this calculus and introduce rules for the modality ! (of course). We use a representation theorem for quantales to show that our calculus with ! is sound and complete with respect to a natural class of models, relational quantales. A relational quantale is a quantale whose elements are relations on a set A, ordered by inclusion and forming a monoid under relational composition. Such quantales have been studied in several areas of theoretical computer science, and so an understanding of the logic associated with them has considerable practical application.