de Mathématiques de Luminy
Andreoli Jean-Marc, Maieli
Roberto and Ruet Paul.
Constraint based proof construction in non-commutative logic.
This work presents a computational interpretation of the construction process for cyclic (CyLL) and non- commutative (NL) sequential proofs. We assume a proof construction paradigm, based on a normalization procedure, known as focussing which manages eAEciently the non-determinism of the construction.
Similarly to the linear case, a new formulation of focussing for NL is used to introduce a general constraint- based technique in order to deal with partial information during proof construction. In particular, the procedure develops through construction steps building "intermediate objects" called abstract proofs, similar to the designs of ludics.