Dexter Kozen and Jerzy Tiuryn. Substructural Logic and Partial Correctness. Trans. Computational Logic, 4(3), July 2003, 355-378. (Subsumes Dexter Kozen and Jerzy Tiuryn. Intuitionistic Linear Logic and Partial Correctness. In Proc. 16th IEEE Symp. Logic in Comput. Sci. (LICS'01), June 2001, 259-268.)

We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary we obtain a complete sequent calculus for inclusion and equivalence of regular expressions.