Publications
Authors:
  • Jean-Marc Andreoli , Roberto Maieli
Citation:
Proc. of 6th Int'l conference on Logic in Programming and Automated Reasoning (LPAR'99), Tbilisi, Rep. of Georgia, Sept. 6-10, 1999
Abstract:
Linear 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 a previous paper by the first author. 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 Abrusci and Ruet's Non-Commutative logic, 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.
Year:
1999
Report number:
1999/210
Attachments: