Non-commutative proof construction: A constraint-based approach

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.