inear Logic has raised a lot of interest in computer research, especially because of its resource sensitive nature. One line of research studies proof construction procedures and their interpretation as computational models, in the “Logic Programming” tradition. An efficient proof search procedure, based on a proof normalization result called “Focusing”, has been described in [2]. Focusing is described in terms of the sequent system of commutative Linear Logic, which it refines in two steps. It is shown here that Focusing can also be interpreted in the proof-net formalism, where it appears, at least in the multiplicative fragment, to be a simple refinement of the “Splitting lemma” for proof-nets. This change of perspective allows to generalize the Focusing result to (the multiplicative fragment of) any logic where the “Splitting lemma” holds. This is, in particular, the case of the Non-Commutative logic of [ 1 ], and all the computational exploitation of Focusing which has been performed in the commutative case can thus be revised and adapted to the non commutative case.

Maieli, R., J. M., A. (1999). Focusing and proof-nets in linear and non commutative logic. In Logic for Programming and Automated Reasoning (pp.320-336). BERLIN HEIDELBERG : Springer-Verlag [10.1007/3-540-48242-3_20].

Focusing and proof-nets in linear and non commutative logic

MAIELI, ROBERTO
;
1999-01-01

Abstract

inear Logic has raised a lot of interest in computer research, especially because of its resource sensitive nature. One line of research studies proof construction procedures and their interpretation as computational models, in the “Logic Programming” tradition. An efficient proof search procedure, based on a proof normalization result called “Focusing”, has been described in [2]. Focusing is described in terms of the sequent system of commutative Linear Logic, which it refines in two steps. It is shown here that Focusing can also be interpreted in the proof-net formalism, where it appears, at least in the multiplicative fragment, to be a simple refinement of the “Splitting lemma” for proof-nets. This change of perspective allows to generalize the Focusing result to (the multiplicative fragment of) any logic where the “Splitting lemma” holds. This is, in particular, the case of the Non-Commutative logic of [ 1 ], and all the computational exploitation of Focusing which has been performed in the commutative case can thus be revised and adapted to the non commutative case.
1999
978-3-540-66492-5
Maieli, R., J. M., A. (1999). Focusing and proof-nets in linear and non commutative logic. In Logic for Programming and Automated Reasoning (pp.320-336). BERLIN HEIDELBERG : Springer-Verlag [10.1007/3-540-48242-3_20].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11590/166050
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact