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.
Maieli, R., ANDREOLI Jean, M., Ruet, P. (2006). Non-commutative proof construction: a constraint-based approach. ANNALS OF PURE AND APPLIED LOGIC, 142(1-3), 212-244 [10.1016/j.apal.2006.01.002].
Non-commutative proof construction: a constraint-based approach
MAIELI, ROBERTO
;
2006-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
