Weak Focusing for Ordered Linear Logic (CMU-CS-10-147)

Ever since Andreoli’s pioneering work in linear logic, it has been understood that the technique of focusing can be used to obtain the operational semantics of a logic programming language from a logic. In previous work, Polakow presented ordered linear logic and gave a backward-chaining operational semantics semantics for the uniform fragment of the logic, and the authors have previously presented a fragment of ordered linear logic suitable to a forward-chaining operational semantics. In this report we give a so-called weakly focused sequent calculus for a polarized firstorder ordered linear logic with equality assumptions, generalizing and extending both of these previous proposals. The polarized sequent calculus and the cut admissibility theorem for this logic are standard, but the proof of the identity theorem requires a new technique. We show how the cut and identity theorem can be used in a straightforward manner to establish the completeness of the weakly focused sequent calculus with respect to an non-focused sequent calculus for ordered linear logic.