Abstract   This work presents a computational interpretation of the construction process for cyclic linear logic (CyLL) and non-commutative logic (NL) sequential proofs. We assume a proof construction paradigm, based on a normalisation procedure known as  focussing , which efficiently manages the non-determinism of the construction.  Similarly to the commutative case, a new formulation of focussing for NL is used to introduce a general constraint-based technique in order to dealwith partial information during proof construction. In particular, the procedure develops through construction steps propagating constraints in intermediate objects called  abstract proofs .
['Jean-Marc Andreoli', 'Roberto Maieli', 'Paul Ruet']
Non-commutative proof construction: A constraint-based approach