LABELLED DEDUCTION

LABELLED DEDUCTION

Edited by

DAVID BASIN

University of Freiburg

MARCELLO D’AGOSTINO

University of Ferrara

DOV M. GABBAY

King’s College

SE � AN MATTHEWS

Max-Planck-Insitut f� ur Informatik

LUCA VIGAN � O

University of Freiburg

Kluwer Academic Publishers Boston/Dordrecht/London

Contributing Authors

Author 1 is an Associate Professor ... Author 2 is University Professor of ...

Introduction

David Basin, Marcello D’Agostino, Dov M. Gabbay, Se� an Matthews, Luca Vigan� o

TO BE WRITTEN

Chapter 1

LABELLED PROOF SYSTEMS FOR INTUITIONISTIC PROVABILITY

Vincent Balat

Ecole Normale Sup� erieure 45, rue d’Ulm 75005, Paris, France

Vincent.Balat@ens.fr

Didier Galmiche

LORIA UMR 7503 Universit� e Henri Poincar� e Campus scienti�que, BP 239 54506 Vand�uvre-l� es-Nancy, France

Didier.Galmiche@loria.fr

Abstract In this paper, we propose new labelled proof systems to analyse the intuitionistic provability in classical and linear logics. An important point is to understand how search in a non-classical logic can be viewed as a perturbation of search in classical logic. Therefore, suitable characterizations of intuitionistic provability and related labelled sequent calculi are de�ned for linear logic. An alternative approach, based on the notion of proof-net and on the de�nition of suitable labelled classical proof-nets, allows to directly study the intuitionistic provability by constructing intuitionistic proof-nets for sequents of classical linear logic.

Keywords: Proof theory, intuitionistic logic, linear logic, labelled sequent calculus, proofnets, automated deduction.

1. INTRODUCTION

Labelled Proof Systems for Intuitionistic Provability 3

Many proof-search methods (sequent calculus, tableaux, resolution, connections) have been naturally developed in classical logic (CL) with a view to avoiding the possible redundancies, unsuccessful explorations or loops, as illustrated by naive search in sequent calculi. Some of them have been adapted to intuitionistic logic (IL) that can be viewed, from a proof-theoretic point of view, as a specialization of classical logic. Let us recall that a sequent calculus for IL can be directly obtained from the classical one by restricting the sequent conclusions to a single formula. Another equivalent multi-conclusion sequent calculus for IL, that is a specialisation of CL multi-conclusion sequent calculus with so-called special rules, has been proposed to more ef�ciently deal with intuitionistic proof-search from classical proof-search [13]. Then classical logic plays a pivotal role in search calculi and an interesting point consists in understanding how search in a non-classical logic can be viewed as a perturbation on search in classical logic. It has been recently studied in [30] by considering a proof-theoretic approach, based on λμ-terms [29], where the terms permit an axiomatisation of the perturbation which yields the non-classical search and also some semantical explanations about embedding in classical logic. In this setting, some questions arise: can we conclude from a classical proof of a given sequent that there exists an intuitionistic proof of it ? can we extract such a proof from the classical one ? is it possible to consider the intuitionistic search as a perturbation of classical search and to have a completeness result, i.e., to determine the intuitionistic provability of a sequent from any classical proof ? This paper deals with these questions mainly in the context of classical linear logic (CLL) that can be seen as a resource-sensitive re�nement of CL [21, 22]. A central point is the choice of the proof systems to analyse the intuitionistic provability from classical search. We know that natural deduction is a suitable deduction system for IL but not for CL for which sequent calculus seems better suited. The Curry-Howard correspondence allows to annotate natural deductions with terms (for IL it yields to typed λ-calculus) but for sequent calculus, it is not clear what the appropriate notations are. For instance, Parigot has introduced a variant of multi-conclusion natural deduction and the related λμ-calculus, which seem suited for handling CL [29]. In the setting of linear logic, similar problems of representation arise, knowing that the speci�c notion of proof-net can moreover be seen as a counterpart of natural deduction. The relationships between classical linear logic (CLL) and intuitionistic linear logic (ILL) have to be studied from both proof-theoretic and proof-search points of view. Let us recall that ILL can be seen as a model of Petri nets [14, 16] and also as a foundation of functional and logic linear programming languages. Moreover recent speci�cation logics are based on fragments of ILL (like Lolli [25]) or CLL (like Forum [28]), the choice being motivated by speci�c operational aims, for instance sequentiality in ILL and concurrency in CLL. Therefore, the study of intuitionistic provability from classical provability in linear logic would have an important impact on proof-search and semantics analysis. In section 2, we study the intuitionistic provability from classical search by de�ning a new labelled proof system. This labelled sequent calculus for CL is an alternative to the based-on λμ-terms approach given in [30], being not type-theoretic but proof-search oriented. In both cases, there is no completeness result, i.e one cannot conclude the intuitionistic provability from any given classical proof. The main part of this paper deals with characterizations of the intuitionistic provability in the setting of linear logic. Therefore, in section 3, we summarize the main characteristics of classical and intuitionistic linear logics and focus on a particular intuitionistic system called (multiplicative) FILL (Full Intuitionistic Linear Logic) that simultaneously embodies features of concurrent logical computations, induced by the par connective and the sequential properties of intuitionistic linear implication [26]. In section 4, we then propose two labelled sequent calculi for (multiplicative) CLL with related characterizations of intuitionistic provability. The �rst one is a direct extension of the labelled CL sequent calculus to CLL but the provability characterization does not �t well from a logical point of view. The second one has a more suitable and useful de�nition of labels w.r.t. linear logic speci�cities. Moreover it can be independently considered as a new proof system for FILL without terms or pattern calculus [7, 26] that is more adapted to proof-search. As in the classical case, these systems do not give a positive answer to the above mentioned completeness problem. In section 5, we consider a new labelled proof system, based on the notion of proof-net and its possible use for proof-search. It allows to directly construct an intuitionistic proof, if there exits, from a classical search. For that, we de�ne (multiplicative) FILL proof-nets that are in fact classical proof-nets with labels that represent some so-called dependency paths. Then we design an algorithm that, for a given CLL initial sequent, builds a FILL proof-net and also a sequent proof, if they exist. Therefore, the intuitionistic provability question can be successfully studied from labelled proof-nets and the intrinsic completeness problem arising with the labelled sequent calculi is solved. Finally, section 6 presents some concluding remarks.

2. INTUITIONISTIC PROVABILITY IN CLASSICAL LOGIC

The relationships between CL and IL are strong and then one can try to use the classical proof-search to characterize the intuitionistic provability. The intuitionistic logic is studied because of its underlying constructivism and its connections with the λ-calculus and programming (Curry-Howard isomorphism). A sequent calculus for IL can be obtained from classical sequent calculus of CL (see appendix 1.) by restricting sequents to a single conclusion (see appendix 2.). It is important to recall that there exists a multi-conclusion sequent calculus for IL (see appendix 3.), that is well adapted to study ef�cient proof-search [13, 31, 32]. Such a calculus is in fact a restriction of classical sequent calculus including some particular rules called special rules. It allows to naturally consider the intuitionistic provability like a perturbation of classical provability. Thus, we can consider the following question: is it possible to conclude to the existence of an intuitionistic proof from the existence of a classical proof ? An analysis of this problem has been developed in [30] where classical proofs are encoded in the λμ-calculus [29] that is an extension of λcalculus related to the classical logic. Therefore, in a type-theoretic approach, a classical proof is represented with a λμ-term and a characterization of terms representing classical proofs that include an intuitionistic proof is given. But such a characterization is not complete, i.e., a sequent can be provable in IL but one cannot observe it from any classical proof. Another approach is the one of [11] with a tableau system that distinguishes classical and intuitionistic logics by comparing semantic labels after a proof is constructed. Is the analysis easier using λμ-terms, semantics labels or initial classical proofs ? Because we are more interested on proof-search than on provability, we propose to directly analyse the classical proofs to detect the existence of an underlying intuitionistic proof. Then we de�ne a sequent calculus with labels that allows to memorize the necessary information to analyse intuitionistic provability.

2.1 A LABELLED SEQUENT CALCULUS FOR CL

We now present a new labelled system for classical proofs that is used to detect their intuitionistic character, with a very simple criterion^{1}. The principle consists in annotating each formula with a speci�c label (or word), to keep a trace of the construction of the classical sequent proof. From a given labelled classical proof, the labels of the sequent axioms allow to characterize the intuitionistic provability. Considering its multi-conclusion (propositional) version IL differs from CL only because of the so-called special rules →_{R} and ¬_{R} [13, 32]. Let us analyse the →_{R} rule, respectively in multi-conclusion CL and IL versions :

{Γ, A ⊢ B, Δ \atop Γ ⊢ A → B, Δ}  {Γ, A ⊢ B \atop Γ ⊢ A → B, Δ}

For each application of the →_{R} rule, we mark all formulae of Δ with the 0 symbol and the A and B formulae with the x symbol. The positions of the symbols in the labels memorize the different applications of such a special rule. In fact, we forbid a (sub)formula of A and a (sub)formula of one formula of Δ to meet in an axiom sequent. We apply the same principle to the ¬_{R} rule. We thus consider the alphabet Σ = {1, x, 0} and the sequents have the following

1The initial version of this system was discussed and developed with G. Delzanno, when he visited LORIA in Nancy during the year 1996/97.

Γ, A^{v} ⊢ A^{w}, Δ ax  Γ ⊢ A, Δ Γ′, A ⊢ Δ′ Γ, Γ′ ⊢ Δ, Δ′ cut
{Γ, A^{v}, A^{v} ⊢ Δ \atop Γ, A^{v} ⊢ Δ} c_{L} {Γ ⊢ Δ, A^{v}, A^{v} \atop Γ ⊢ Δ, A^{v}} c_{R}
\begin{matrix}Γ ⊢ A^{v}, Δ & Γ, B^{v} ⊢ Δ \\ Γ, (A → B)^{v} ⊢ Δ \end{matrix} →_{L}  {Γ^{1u}, A^{xv} ⊢ B^{xv}, Δ^{0w} \atop Γ^{u} ⊢ (A → B)^{v}, Δ^{w}} →_{R}
\begin{matrix}Γ, A^{v} ⊢ Δ & Γ, B^{v} ⊢ Δ \\ Γ, (A ∨ B)^{v} ⊢ Δ \end{matrix} ∨_{L}  {Γ ⊢ A^{v}, Δ \atop Γ ⊢ (A ∨ B)^{v}, Δ} ∨_{R1} {Γ ⊢ B^{v}, Δ \atop Γ ⊢ (A ∨ B)^{v}, Δ} ∨_{R2}
{Γ, A^{v}, B^{v} ⊢ Δ \atop Γ, (A ∧ B)^{v} ⊢ Δ} ∧_{L}  \begin{matrix}Γ ⊢ A^{v}, Δ & Γ ⊢ B^{v}, Δ \\ Γ ⊢ (A ∧ B)^{v}, Δ \end{matrix} ∧_{R}
{Γ ⊢ A^{v}, Δ \atop Γ, ¬A^{v} ⊢ Δ} ¬_{L}  {Γ^{1u}, A^{xv} ⊢ Δ^{0w} \atop Γ^{u} ⊢ ¬A^{v}, Δ^{w}} ¬_{R}

Figure 1.1 Labelled sequent calculus for CL

form A_{1}^{v_{1}}, ...A_{k}^{v_{k}} ⊢ B_{1}^{w_{1}}, ...B_{m}^{w_{m}} where v_{1}, ...v_{k}, w_{1}, ..., w_{m} are words of same length on Σ.

Notation 1 u[p] denotes the letter of the word u at position p, the letters being annotated from 1, from right-hand side to left-hand side. |u| denotes the length of the word u and ε denotes the empty word. If a ∈ Σ and v = v[n]...v[1] ∈ Σ^{∗}, then av denotes the word av[n]...v[1]. If Γ = A_{1}, ..., A_{k} is a list of formulae and v = v_{1}, ..., v_{k} is a list of words, Γ^{v} denotes the set of labelled formulae A_{1}^{v_{1}}, ...A_{k}^{v_{k}}, and Γ^{av} denotes A_{1}^{av_{1}}, ...A_{k}^{av_{k}}.

At the beginning, the formulae of the sequent to prove are labelled with the empty word. The labelled sequent calculus for CL is given in Figure 1.1. When labels are omitted it means that they are unchanged.

De�nition 2 Let Γ ⊢ Δ be a labelled sequent, A^{u} (resp. A^{v}) a labelled formula of Γ (resp. Δ), and p an integer such that 0 < p ≤ min(|u|, |v|), the pair (u[p], v[p]) is called a correspondence at position p on the sequent.

De�nition 3 A set of axiom sequents is said to be intuitionistic if, for any position p, there is no correspondence of the form (x, 0) or (0, x).

Theorem 4 If a sequent Γ ⊢ Δ has a proof (in the system Figure 1.1) such that the set of axiom sequents is intuitionistic, then there exists an intuitionistic proof of the sequent.

Proof It is a direct consequence of the relationships between what a correspondence of the form (x, 0) or (0, x) means and the application of so-called special rules in the multi-conclusion sequent calculus of IL (see appendix 3.). ■

Then, this characterization of intuitionistic provability depends on syntactic labels (that are words) and mainly on the notion of position in such labels.

2.2 THE COMPLETENESS PROBLEM

Let us �rst consider a classical proof that includes an intuitionistic proof.

\begin{matrix}\begin{matrix}Γ^{1}, A^{x} ⊢ A^{1}, B^{x}, B^{0} ax & Γ^{1}, A^{x}, B^{1} ⊢ B^{x}, B^{0} ax \\ Γ^{1}, A^{x}, \underline{A → B}^{1} ⊢ B^{x}, B^{0} \end{matrix} ; →_{L} ; Γ, A → B ⊢ \underline{A → B}, B ; →_{R} & Γ, A → B, B ⊢ B ax \\ Γ, A → B, \underline{(A → B) → B} ⊢ B \end{matrix} ; →_{L}

Let us notice that if the inference rules are applied in another order, it is no more possible to claim, by application of the previous criterion, that there exists an intuitionistic proof of such a sequent (because of a (x, 0) correspondence on the formula A of one axiom sequent).

\begin{matrix}\begin{matrix}\begin{matrix}Γ^{1}, A^{x} ⊢ B^{x}, A^{0}, B^{0} & ax \\ Γ ⊢ \underline{A → B}, A, B \end{matrix} ; →_{R} & Γ, B ⊢ A, B ax \\ Γ, \underline{(A → B) → B} ⊢ A, B \end{matrix} ; →_{L} & Γ, (A → B) → B, B ⊢ B ax \\ Γ, \underline{A → B}, (A → B) → B ⊢ B \end{matrix} ; →_{L}

We have no completeness result, i.e, for a given sequent, we cannot conclude from any classical proof if it is also provable in IL. It is well illustrated with both previous proofs. It is also the case in the type-theoretic approach proposed in [30] where classical logic can be viewed as a type theory based on an extension of the Parigot’s λμ-calculus [29]. Conditions for intuitionistic provability are expressed on classical λμ-terms and are also equivalent to admissible conditions on pre�x uni�ers in [32]. The use of such terms for the axiomatisation of the perturbation which yields non-classical search, allows to have semantical explanations of syntactic tricks to embed non-classical search in classical systems. Our equivalent approach, based on syntactic labels in a sequent calculus, is nevertheless simple and readable from both algorithmic and proof-search points of view. When a classical proof contains an intuitionistic proof, we can use the information given by the labels to extract an intuitionistic proof. The principle consists in detecting the needless formulae in the classical proof by an analysis of the labels and then in erasing them. A simple algorithm can be proposed for this operation. The main advantages and limits of using such labelled systems will be illustrated in the case of linear logic, for which the based-on λμ-calculus approach could be also used at �rst to devise a natural deduction formulation of classical linear logic [8].

3. LINEAR LOGIC

Linear logic is a resource-sensitive logic that can be seen as a re�nement of classical logic sequent calculus where contraction and weakening rules are forbidden [22]. Both classical linear logic (CLL) and its intuitionistic fragment, called intuitionistic linear logic (ILL), are studied as models of computation [2] and of semantics of parallelism [20].

3.1 CLASSICAL LINEAR LOGIC

The usual presentation of CLL consists in starting from the CL sequent calculus with suppression of the contraction and weakening rules. Then the equivalence between the additive and multiplicative presentations of the ∨ and ∧ connectives disappears and then leads to distinguish a multiplicative ∨ (�par�, denoted ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ), an additive ∨ (�with�, denoted &), a multiplicative ∧ (�times�, denoted ⊗), and an additive ∧ (�plus�, denoted ⊕). The atoms have the form A or A^{⊥}. The de�nition of the negation ()^{⊥}, that is involutive, is extended to all formulae from the following rules: (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} = (A^{⊥} ⊗ B^{⊥}), (A ⊗ B)^{⊥} = (A^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B^{⊥}), (A ⊕ B)^{⊥} = (A^{⊥}&B^{⊥}) and (A&B)^{⊥} = (A^{⊥} ⊕ B^{⊥}). The symbols 1, 0, ⊤ and ⊥ respectively represent the neutrals of the ⊗, ⊕, & and^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connectives. The linear implication (−∘) is de�ned by A−∘B = A^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B. The ! (�of course�) and ? (�why not�) connectives (called exponentials) are used to reintroduce in a controlled way the weakening and the contraction rules (but as logical rules). Let us mention that the intuitionistic implication A → B can be, with such operators, decomposed into two operations, i.e. !A −∘ B. See appendix 4. to have the rules of propositional CLL. The Multiplicative Linear Logic (only with the multiplicative connectives) without constants, is denoted MLL.

3.2 INTUITIONISTIC LINEAR LOGIC

In linear logic, compared to classical logic, the de�nition of an intuitionistic fragment is not so natural and direct from the initial sequent calculus. The Intuitionistic Linear Logic (ILL) has a mono-conclusion sequent calculus (see appendix 5.). Compared to the non-linear case, ILL is de�ned with a formula grammar that is different from the CLL one. In fact, the rules corresponding to^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , its neutral element ⊥, the negation^{⊥} and to ? led to consider a multi-conclusion representation. Then the grammar of formulae in ILL is ϕ ::= p | ϕ ⊗ ϕ | ϕ −∘ ϕ | ϕ&ϕ | ϕ ⊕ ϕ | !ϕ, where p is an atomic formula or a constant ⊤, 0 or 1. In [24], Girard and Lafont illustrate the interest of linear logic, compared to IL to represent types of functions and linear λ-terms have been de�ned in this context [27]. Therefore, the ⊗ connective is a strict ∧ while the & connective is a lazy ∧. In this setting, the real meaning of the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connective is not clear with this interpretation of proofs as functions. The relationship between CLL and ILL can be expressed through the following result

Theorem 5 Let be S a sequent built from the ILL (without constants) grammar, if S is provable in CLL then it is provable in ILL.

Proof Let us consider a sequent provable in CLL, that only uses the ILL grammar. We �rst show that all sequents, in such a CLL proof, have a single formula as conclusion. For that, we observe that the axioms are monoconclusion and then for each rule of CLL, if the premises are mono-conclusion then the conclusion is also mono-conclusion. Secondly, we show that a CLL rule applied to a mono-conclusion sequent gives the same result than the ILL corresponding rule. ■

Let us note that if we consider a version of CLL including the rules for the −∘ connective then the ILL proof will be identical to the CLL proof. Works on ILL have been developed from linear λ-calculus [6, 8, 24], but the lack of the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connective seems more motivated by technical reasons and then we could ask for an intuitionistic fragment of linear logic including it. In this context, the semantics of ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} has to be clari�ed even if a natural interpretation seems to be connected to the concurrent execution of processes [1, 9].

3.3 FULL INTUITIONISTIC LINEAR LOGIC

A multi-conclusion intuitionistic multiplicative linear logic, called Full Intuitionistic Linear Logic (FILL) has been proposed by Hyland and de Paiva in [26]. That is a variant of intuitionistic linear logic whose logical connectives are all independent, i.e., not inter-derivable as they are in multiplicative CLL. It is analogous to the situation concerning the relationship between IL and CL. The interest of FILL is that it simultaneously embodies features of concurrent logical computations, induced by the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connective, and the sequential properties of intuitionistic linear implication. In FILL the negation A^{⊥} is de�ned as A −∘ ⊥ and it is not an involution. This system, that includes the multiplicative disjunction ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , is a subsystem of CLL and a proof in FILL is a proof in CLL with a certain intuitionistic property. For instance, one has A^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ A −∘ B in FILL but not the converse. Moreover, the excluded middle ⊢ A^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A cannot be proved in FILL. It is the same for A^{⊥⊥} ⊢ A and for ⊢ (A^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A)^{⊥⊥}. This last remark illustrates the difference from the situation in IL where ⊢ ¬A ∨ A is not provable but ¬¬(¬A ∨ A)) is provable. It comes from the use of contraction in IL and the effective difference between the ∨_{R} and^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{R} rules. Moreover, (A⊗B)−∘(C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D) ⊢ (A−∘C) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B−∘D) is an example of a sequent provable in CLL but not in FILL (see [10] for more details). Let us mention also that the interaction between ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and the linear implication −∘ is such that cut-elimination failed outright for some intuitive formulation of FILL. This problem has motivated, from the term assignment system in [26], some alternative presentations as the ones of Bierman [7] and Bra�ner and de Paiva [10]. The latter is based on a notion of dependency to capture, with a side condition of −∘_{R}, the underlying notion of intuitionistic implication and to make the cut-elimination to go through in a straightforward manner. In fact, one de�nes, given a proof of Γ, B ⊢ A, Δ in CLL, when the succedent formula occurrence A depends on the antecedent formula occurrence B. This notion of dependency between formulae occurrences allows to express the intuitionistic property that characterizes FILL [10]. The corresponding sequent calculus is given in Figure 1.2. Let τ be a CLL proof, for each formula C at the righthand side of the sequents in τ, one de�nes the set Dep_{τ} (C) of the formulae of left-hand side on which it depends. In the rules, τ represents the proof-tree, the root of which is the conclusion of the rule, τ_{1} (resp. τ_{2}) is the sub-proof, the root of which is the �rst (resp. second) premise, if it exists. Moreover the set of formulae occurrences Γ[Δ ↦ Δ′] is de�ned as (Γ \ Δ) ∪ Δ′ if Γ ∩ Δ ≠ ∅ and as Γ otherwise. This notion of dependency allows a de�nition of FILL proof.

De�nition 6 A FILL proof is a proof of CLL such that, for any −∘_{R} rule and any formula C of Δ, we have A ∉ Dep_{τ_{1}}(C) [10].

Let us now consider the following proof:

\begin{matrix}\begin{matrix}C ⊢ C ax & B ⊢ B ax \\ \underline{C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B} ⊢ B, C \end{matrix}_{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} L} & A ⊢ A ax \\ C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, \underline{B −∘ A} ⊢ C, A \end{matrix} ; ^{−∘^{L}} ; B −∘ A ⊢ \underline{(C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) −∘ C}, A ; ^{−∘^{R}}

that is not a FILL proof. Here, the formula A in the right-hand side of the sequent C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, B −∘ A ⊢ C, A depends on C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B. In fact we have Dep(A) = {C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, B −∘ A}. The presentation of this system does not include a term assignment decorating the usual sequent calculus proofs like in [7, 26]. In the next section, we consider the relationships between CLL and FILL from both proof-theoretic and proof-search points of view. Then we propose new formulations of FILL with sequent calculi with labels that re�ect the dependency conditions inside the inference rules of CLL.

4. INTUITIONISTIC PROVABILITY IN LINEAR LOGIC

Let us now consider the intuitionistic provability from classical search in the case of linear logic. With a proof in ILL, we can propose a simple criterion

A ⊢ A ax  Dep_{τ} (A) = A
Γ ⊢ A, Δ Γ′, A ⊢ Δ′ Γ, Γ′ ⊢ Δ, Δ′ cut Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C) & if C ∈ Δ \\ Dep_{τ_{2}}(C)[A ↦ Dep_{τ_{1}}(A)] & if C ∈ Δ′ \end{matrix}

{Γ, A ⊢ B, Δ \atop Γ ⊢ A −∘ B, Δ} ^{−∘^{R}}  Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C)[A ↦ ∅] & if C ∈ Δ \\ Dep_{τ_{1}}(B)[A ↦ ∅] & if C = A −∘ B \end{matrix}

Γ ⊢ A, Δ Γ′, B ⊢ Δ′ Γ, Γ′, A −∘ B ⊢ Δ, Δ′ ^{−∘^{L}} Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C) & if C ∈ Δ \\ Dep_{τ_{2}}(C)[B ↦ (Dep_{τ_{1}}(A) ∪ (A −∘ B))] & if C ∈ Δ′ \end{matrix}

Γ, A ⊢ Δ Γ′, B ⊢ Δ′ Γ, Γ′, A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ Δ, Δ′ ^{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} L} Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C)[A ↦ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)] & if C ∈ Δ \\ Dep_{τ_{2}}(C)[B ↦ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)] & if C ∈ Δ′ \end{matrix}

{Γ ⊢ A, B, Δ \atop Γ ⊢ A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, Δ} ^{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} R}  Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C) & if C ∈ Δ \\ Dep_{τ_{1}}(A) ∪ Dep_{τ_{1}}(B) & if C = A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B \end{matrix}

{Γ, A, B ⊢ Δ \atop Γ, A ⊗ B ⊢ Δ} ⊗_{L}  Dep_{τ} (C) = Dep_{τ_{1}}(C)[A, B ↦ A ⊗ B]
Γ ⊢ A, Δ Γ′ ⊢ B, Δ′ Γ, Γ′ ⊢ A ⊗ B, Δ, Δ′ ⊗_{R} Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C) & if C ∈ Δ \\ Dep_{τ_{2}}(C) & if C ∈ Δ′ \\ Dep_{τ_{1}}(A) ∪ Dep_{τ_{2}}(B) & if C = A ⊗ B \end{matrix}

{Γ ⊢ Δ \atop Γ, 1 ⊢ Δ} 1_{L}  Dep_{τ} (C) = Dep_{τ_{1}}(C)
⊢ 1 1_{R}  Dep_{τ} (1) = ∅
⊥ ⊢ ⊥_{R}  nothing to de�ne
{Γ ⊢ Δ \atop Γ ⊢ ⊥, Δ} ⊥_{L}  Dep_{τ} (C) = \{ \begin{matrix}Dep_{τ_{1}}(C) & if C ∈ Δ \\ ∅ & if C = ⊥ \end{matrix}

Figure 1.2 a FILL sequent calculus

that corresponds to observe the presence of the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and ? connectives and to test if the sequents have a single conclusion (see theorem 5). In FILL, the structure of the proofs is exactly the same than in CLL but we have to take into account the dependency relations. Compared to the previous study, we do not try to determine if a CLL proof contains a FILL proof but if it is a FILL proof. Among the different presentations of multiplicative FILL [7, 10, 26], mainly motivated by semantics analysis and by simple and readable cut-elimination proofs, the one of Bra�ner and de Paiva [10] appears to be the more related to our approach. In fact, our proposals can be seen as new proof systems for FILL that could be useful for further works based on objects or processes [9]. We now present labelled proof systems for multiplicative CLL. The �rst one is a direct extension of the criterion de�ned for CL and the second one is more simple and appropriate to the case of linear logic. From now, we only consider the multiplicative part of the logical fragments.

4.1 A LABELLED SEQUENT CALCULUS

In this �rst proposal, the formulae are labelled with words but we have not only to simulate the use of special rules where some formulae are erased but also to effectively test the dependencies between formulae. As we consider transitive dependency chains that can have arbitrary length, we then use an in�nite alphabet Σ including the 1, x, and 0 symbols. The position in the word is also used to determine where special rules have been applied. A formula is labelled by a list of words that allows several correspondences at the same position between two formulae.

Notation 7 We denote u :: l a list with u as head and l as tail. Lists are presented in extension with ; and for instance the list with the words u, v and w as elements is denoted u; v; w. Moreover ∅ denotes the empty list.

At the beginning, each formula of the sequent to prove is labelled with the ε :: ∅ list (the empty word is the only element). The labelled sequent calculus is given in Figure 1.3, where labels are omitted when they are unchanged and n is the length of the head word for any conclusion formula. Let us note that, for a given n, the words a^{n} and 1^{n} allow to guarantee that the head words have all the same length. Moreover, in −∘_{R} we pad out the label of A with a safe number of 1. The notion of correspondence of de�nition 2 is extended to this new sequent calculus and leads to a suitable de�nition of dependency chain on sequences^{2} of sequents.

De�nition 8 Let E be a sequence of sequents, a dependency chain on E at position p between the letters α and β is a sequence of pairs of the form (α, α_{1}), (α_{1}, α_{2}), ..., (α_{n}, β) (n ∈ ℕ^{∗}), the elements of which are correspondences at position p in one of the sequents of E.

De�nition 9 A sequence of sequents is said to be intuitionistic if for any sequent there exists no position p with a dependency chain between x and 0.

Theorem 10 Let P be a proof (in the system Figure 1.3), P is a FILL proof if and only if the sequence of its axiom sequents is intuitionistic.

2We prefer to deal with sequences and not with sets mainly because of the further management of axiom sequents extracted from proofs.

{Γ^{1u::l_{1}}, A^{x1^{n}::∅} ⊢ B^{1v::l_{2}}, Δ^{0w::l_{3}} \atop Γ^{u::l_{1}} ⊢ (A −∘ B)^{v::l_{2}}, Δ^{w::l_{3}}} ^{−∘^{R}}
Γ ⊢ A^{a^{n}::∅}, Δ Γ′, A^{a^{n}::∅} ⊢ Δ′
Γ, Γ′ ⊢ Δ, Δ′

cut with a fresh letter

Γ ⊢ A^{a^{n}::∅}, Δ Γ′, B^{v::a^{n}::l} ⊢ Δ′
Γ, Γ′, (A −∘ B)^{v::l} ⊢ Δ, Δ′

−∘^{L}  with a fresh letter
A^{l_{1}} ⊢ A^{l_{2}} ax
{Γ ⊢ Δ \atop Γ, 1^{l} ⊢ Δ} 1_{L} ⊢ 1^{l} 1_{R} ⊥^{l} ⊢ ⊥_{L} {Γ ⊢ Δ \atop Γ ⊢ ⊥^{l}, Δ} ⊥_{R}
Γ, A^{l} ⊢ Δ Γ′, B^{l} ⊢ Δ′ Γ, Γ′, (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{l} ⊢ Δ, Δ′ ^{...............................................................................................} L  {Γ ⊢ A^{l}, B^{l}, Δ \atop Γ ⊢ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{l}, Δ} ^{...............................................................................................} R
{Γ, A^{l}, B^{l} ⊢ Δ \atop Γ, (A ⊗ B)^{l} ⊢ Δ} ⊗_{L}  Γ ⊢ A^{l}, Δ Γ′ ⊢ B^{l}, Δ′ Γ, Γ′ ⊢ (A ⊗ B)^{l}, Δ, Δ′ ⊗_{R}

Figure 1.3 A labelled sequent calculus for CLL.

Proof The proof of this theorem is a directed adaptation of the proof we will develop in the next section for the second and main characterization. ■

We now present a proof in CLL of the sequent C−∘B, D−∘A ⊢ (C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)−∘B, A, that is not a FILL proof, because of a dependency chain (x, y), (y, 0).

\begin{matrix}\begin{matrix}\begin{matrix}C^{x} ⊢ C^{z} ax & D^{x} ⊢ D^{y} ax \\ \underline{(C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)^{x}} ⊢ C^{z}, D^{y} \end{matrix}_{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} L} & B^{1;z} ⊢ B^{1} ax \\ \underline{(C −∘ B)^{1}}, (C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)^{x} ⊢ D^{y}, B^{1} \end{matrix} ; ^{−∘^{L}} & A^{1;y} ⊢ A^{0} ax \\ (C −∘ B)^{1}, \underline{(D −∘ A)^{1}}, (C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)^{x} ⊢ B^{1}, A^{0} \end{matrix} ; ^{−∘^{L}} ; C −∘ B, D −∘ A ⊢ \underline{(C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D) −∘ B}, A ; ^{−∘^{R}}

In our �rst criterion, the position p in a word is used to know for which applications of the −∘_{R} the letters appeared. It avoids to mix the dependency chains. But this principle has the disadvantages to complicate the system presentation by keeping several words for each formula and by creating words of the form y^{n} because we do not know at which position the y will be used. This proposal is then based on the notion of position but in several words.

4.2 ANOTHER LABELLED SEQUENT CALCULUS

An alternative, not directly connected to our initial criterion, consists in using a different marking for each special rule. In this case, the position p in a label has no more importance, the words can have different lengths and we only need one word per formula. The alphabet is then Σ = Σ_{1} ∪ Σ_{2}, with Σ_{1}

{Γ, A^{x} ⊢ B^{v}, Δ^{xw} \atop Γ ⊢ (A −∘ B)^{v}, Δ^{w}} ^{−∘^{R}  with x fresh letter of Σ_{1}}
Γ ⊢ A^{y}, Δ Γ′, A^{y} ⊢ Δ′
Γ, Γ′ ⊢ Δ, Δ′

cut with y fresh letter of Σ_{2}

Γ ⊢ A^{y}, Δ Γ′, B^{yv} ⊢ Δ′ Γ, Γ′, (A −∘ B)^{v} ⊢ Δ, Δ′

−∘^{L}  with y fresh letter of Σ_{2}
A^{v} ⊢ A^{w} ax
{Γ ⊢ Δ \atop Γ, 1^{v} ⊢ Δ} 1_{L} ⊢ 1^{v} 1_{R} ⊥^{v} ⊢ ⊥_{L} {Γ ⊢ Δ \atop Γ ⊢ ⊥^{v}, Δ} ⊥_{R}
Γ, A^{v} ⊢ Δ Γ′, B^{v} ⊢ Δ′ Γ, Γ′, (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{v} ⊢ Δ, Δ′ ^{...............................................................................................} L  {Γ ⊢ A^{v}, B^{v}, Δ \atop Γ ⊢ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{v}, Δ} ^{...............................................................................................} R
{Γ, A^{v}, B^{v} ⊢ Δ \atop Γ, (A ⊗ B)^{v} ⊢ Δ} ⊗_{L}  Γ ⊢ A^{v}, Δ Γ′ ⊢ B^{v}, Δ′ Γ, Γ′ ⊢ (A ⊗ B)^{v}, Δ, Δ′ ⊗_{R}

Figure 1.4 Another labelled sequent calculus for CLL.

and Σ_{2} being disjoint. In fact, Σ_{1} is used for the extremities of the dependency chains and Σ_{2} for the intermediate symbols. We begin with the empty word on each formula of the given sequent. The rules of this new labelled sequent calculus are given in Figure 1.4. As before, labels are omitted when they are unchanged. As the notion of position has no more signi�cance here, then the appropriate notions of correspondence and of dependency chains are de�ned in the following way:

De�nition 11 A correspondence on a sequent Γ ⊢ Δ is a pair (α, β), where α is a letter in a label of a formula in Γ and β a letter of a label of the same formula in Δ.

De�nition 12 Let E be a sequence of sequents, and let S_{0}, ..., S_{n} be a subsequence of E, a dependency chain on E between α and β is a sequence of pairs of the form (α_{0}, α_{1}), (α_{1}, α_{2}),...,(α_{n}, α_{n+1}) (n ∈ ℕ^{∗}) such that α_{0} = α, α_{n+1} = β, and (α_{i}, α_{i+1}) is a correspondence on S_{i}.

4.2.1 Some properties. Let us begin to prove some properties that are useful to understand the behaviour of the labels in this setting.

Property 13 Let P be a proof (in the system of Figure 1.4) of Γ ⊢ Δ, if the conclusion of a subproof contains a letter α ∈ Σ_{2} then α is always on the same side in all sequents of P.

Let us also mention that if (α, β) is a correspondence on a sequent S inside a proof then all symbols in a dependency chain between α and β are in fact introduced in the subproof, the conclusion of which is S.

Property 14 Let P be a proof (in the system of Figure 1.4) of Γ ⊢ Δ with a dependency chain between α and β on the axiom sequents; for any subproof that contains this chain, if its conclusion has a correspondence (α, β) then the formula labelled with β depends (in the sense of 1.2) on the one labelled with α.

Proof By induction on the depth of the proof tree. Base case: n = 1; the property is veri�ed for the axiom rules. Induction case: Let us assume that the property is veri�ed for n and consider the last inference rule applied in the proof.

- For the rules with one premise, it is trivial.

- For the rules with two premises, we have the following cases:

i) for the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{L} and ⊗_{R} rules, we verify that the dependency chain is completely included in one of the subtrees. ii) for the cut and −∘_{L}, it is the same proof argument if the new introduced letter y is not in the dependency chain. Else if it appears in the chain and if there is a correspondence (α, β) at the root, then the subchain between α and y (resp. y and β) is completely included in the left (resp. right) subtree. By the induction hypothesis we have dependencies between the formulae labelled by α and y in the left-hand side premise and by y and β in the right-hand side premise. The result is then deduced from an analysis of the rule of the dependencies calculus. ■

Property 15 Let P be a proof (in the system of Figure 1.4) of Γ, E ⊢ F, Δ, such that E ∈ Dep(F); if the formulae E and F are in a correspondence (α, β), then there exists a dependency chain between α and β (on the sequence of axiom sequents).

Proof By induction on the depth of the proof tree, with veri�cation of the property for each rule. ■

From these properties, we can deduce the following results:

Lemma 16 Let P be a proof (in the system of Figure 1.4) of a sequent Γ ⊢ Δ,

(i) If there exists a dependency chain on the axiom sequents between two occurrences of the same letter of Σ_{1}, then the dependency condition (of de�nition 6) is not veri�ed where this letter appears. (ii) Let SP be a subproof, the last rule of which is −∘_{R}, and such that there exists A ∈ Δ verifying B ∈ Dep(A), then SP has a dependency chain between two occurrences of the same letter of Σ_{2}.

Proof Both results are direct consequences of the previous properties. ■

4.2.2 The intuitionistic characterization. These preliminary results are necessary to prove the next theorem. Its proof is based on the equivalence between the criteria we de�ne and the calculus of dependencies of the multiplicative FILL system.

De�nition 17 A sequence of sequents is said to be intuitionistic if there is no dependency chain between two occurrences of the same letter of Σ_{1}.

Theorem 18 A proof P (in the system of Figure 1.4) is a FILL proof if and only if the sequence of axiom sequents, ordered from left to right, is intuitionistic.

Proof The proof is a direct consequence of the previous lemma. ■

This proof that corresponds to the criterion of section 4.2, can be easily adapted to the one of section 4.1. Let us note that the order of premises in each rule of Figure 1.4 has to be respected during the proof construction. Let us consider again the example of section 4.1 with this new characterization. The proof is CLL but not FILL because of a dependency chain (x, y), (y, x). Here x ∈ Σ_{1} and (y, z) ∈ Σ_{2}^{2}.

\begin{matrix}\begin{matrix}\begin{matrix}C^{x} ⊢ C^{z} ax & D^{x} ⊢ D^{y} ax \\ \underline{(C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)^{x}} ⊢ C^{z}, D^{y} \end{matrix}_{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} L} & B^{z} ⊢ B ax \\ \underline{C −∘ B}, (C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)^{x} ⊢ D^{y}, B \end{matrix} ; ^{−∘^{L}} & A^{y} ⊢ A^{x} ax \\ C −∘ B, \underline{D −∘ A}, (C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D)^{x} ⊢ B, A^{x} \end{matrix} ; ^{−∘^{L}} ; C −∘ B, D −∘ A ⊢ \underline{(C ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D) −∘ B}, A ; ^{−∘^{R}}

Let us now present an example that illustrates that a sequent can have a CLL proof that is a FILL proof but also another one that is not a FILL proof. Here, we only use one atomic formula A, the different occurrences of which that are distinguished with indices. Therefore we present two labelled proofs of the following sequent: A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}, A_{8} ⊢ A_{1} −∘ (A_{6} ⊗ A_{7}), A_{2} ⊗ A_{3}. The �rst proof is not a FILL proof because of a correspondence (x, x) in one of the axioms.

\begin{matrix}\begin{matrix}\begin{matrix}A_{1}^{x} ⊢ A_{2}^{x} ax & A_{4} ⊢ A_{3}^{x} ax \\ A_{1}^{x}, A_{4} ⊢ \underline{(A_{2} ⊗ A_{3})^{x}} \end{matrix} ; ⊗_{R−2,3} & A_{5} ⊢ A_{6} ax \\ A_{1}^{x}, \underline{A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}} ⊢ A_{6}, (A_{2} ⊗ A_{3})^{x} \end{matrix}_{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} L} & A_{8} ⊢ A_{7} ax \\ A_{1}^{x}, A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}, A_{8} ⊢ \underline{A_{6} ⊗ A_{7}}, (A_{2} ⊗ A_{3})^{x} \end{matrix} ; ⊗_{R−6,7} ; A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}, A_{8} ⊢ \underline{A_{1} −∘ (A_{6} ⊗ A_{7})}, A_{2} ⊗ A_{3} ; ^{−∘^{R}}

One can easily verify that A_{1} ∈ Dep(A_{2} ⊗ A_{3}) in the premise of the −∘_{R} rule. In the following proof

\begin{matrix}\begin{matrix}\begin{matrix}A_{1}^{x} ⊢ A_{6} ax & A_{5} ⊢ A_{7} ax \\ A_{1}^{x}, A_{5} ⊢ \underline{A_{6} ⊗ A_{7}} \end{matrix} ; ⊗_{R−6,7} & A_{4} ⊢ A_{3}^{x} ax \\ A_{1}^{x}, \underline{A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}} ⊢ A_{3}^{x}, A_{6} ⊗ A_{7} \end{matrix}_{^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} L} & A_{8} ⊢ A_{2}^{x} ax \\ A_{1}^{x}, A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}, A_{8} ⊢ \underline{(A_{2} ⊗ A_{3})^{x}}, A_{6} ⊗ A_{7} \end{matrix} ; ⊗_{R−2,3} ; A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}, A_{8} ⊢ \underline{A_{1} −∘ (A_{6} ⊗ A_{7})}, A_{2} ⊗ A_{3} ; ^{−∘^{R}}

there is no correspondence in the axiom sequents and consequently no dependency chain. Thus it is a FILL proof.

4.3 AN ALGORITHM FOR PROOF CONSTRUCTION

From the theorem 18 and this intuitionistic characterization, we can easily derive a corresponding algorithm. In fact, if we have a CLL proof built with the labelled sequent calculus then it is suf�cient to analyse the labels of the axiom sequents and to do the test of the dependency chains. Such an algorithm could be presented in the following way:

For each sequent S in which a x ∈ Σ_{1} is a label of a left-hand side formula, one call the procedure Search chain(x,S,x) that is de�ned as by Procedure Search chain(origin,sequent,current letter) For all correspondences (current letter , α),

- if α = origin then FAILURE

- else, for all axiom sequents S′ on the right-hand side of sequent, call Search chain(origin, S′, α)

It returns a failure message if and only if the given proof is not a FILL proof. In general, with the current examples, the size of the word is not too big and then the number of cases the algorithm has to deal with is reasonable. A study of the complexity could be interesting but would need some choices about implementation. Such investigations are out of the purposes of this paper.

4.4 SOME REMARKS

In fact, such a method allows to verify if a given CLL proof is also a FILL proof. An interesting point could be to analyse, in case of failure, how the labels can be used to propose some heuristics or proof transformations, to obtain more directly and ef�ciently some FILL proofs, if they exist, by classical search. For instance, in the proofs of section 4.2.2, we observe that the application of the ⊗_{R} rule on a marked formula allows to eliminate one possibility of correspondence. Bierman has analysed with Parigot’s techniques the relationships between ILL and CLL to propose a classical linear λ-calculus. This work appears fruitful from the resulting programming language point of view and of more use than such a similar language based on proof-nets [8]. Therefore we could consider an approach similar to [30] by using a linear λ-calculus to encode the proofs and then analyse if they are �intuitionistic�. This approach seems dif�cult to implement and to effectively use. Anyway, an alternative could be based on the notion of proof-net that can be seen as a counterpart of natural deduction in linear logic [23]. It could be an appropriate semantical and syntactical representation of proof-objects (or terms) for the analysis of intuitionistic provability.

5. PROOF-NETS AND INTUITIONISTIC PROVABILITY

We now propose an alternative approach to consider the intuitionistic provability in CLL. It is based on a speci�c structure of linear logic, i.e. proof-net, that was naturally introduced by Girard as a counterpart of natural deduction in linear logic [21].

5.1 SOME DEFINITIONS

A proof-net is a particular graph, the nodes of which are formulae of linear logic [23]. It is naturally de�ned for the multiplicative linear logic MLL (without constants) as recalled in this subsection and can be seen as an ef�cient tool for automated deduction in such a fragment [15]. There are also proof-nets de�nitions for other CLL fragments, like MALL (Multiplicative and Additive Linear Logic) [23] but they are more complicated to handle.

De�nition 19 A proof-structure is a graph, the vertices of which are formulae, inductively built from the following substructures (called links) :

A  A^{⊥}  \begin{matrix}A B \\ ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} \\ A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B \end{matrix}  \begin{matrix}A B \\ ⊗ \\ A ⊗ B \end{matrix}  A  A^{⊥}

where A and B are formulae. In such a graph, any formula is the premise of at least one link and the conclusion of exactly one link.

A proof-structure can be also seen as the set of the subformulae of the formula or sequent to prove (represented as a decomposition tree) plus a set of axiom-links such that each atom of the tree is the conclusion of exactly one axiom-link. A proof-net, for a given sequent, is in fact a proof-structure that corresponds to legal proofs [21]. There are several equivalent de�nitions of what a proof-net is, that are generally based on criteria that characterize the proof-structures that are proof-nets [21], like for instance the Danos-Regnier characterization [12]. The construction of a proof-net can be seen as the search of the connections (axiom-links) that characterize the provability of a given sequent [15].

To simplify the different representations, we often omit the formulae labelling the nodes and only represents the connectives. Here we recall the inductive de�nition of proof-net, introduced by Bellin [5].

De�nition 20 A MLL proof-net and its set of conclusions are inductively de�ned in the following way:

- If A is any multiplicative formula, A A^{⊥}is a proof-net, with A and A^{⊥} as conclusions (axiom-link)

- If Π_{1} (resp. Π_{2}) is a proof-net with Γ_{1} ∪ {A} (resp. Γ_{2} ∪ {A^{⊥}}) as conclusions, and if Π_{1} and Π_{2} are disjoint (not connected), then

Π_{1} A Γ_{1}  Π_{2} A^{⊥} Γ_{2} is a proof-net with Γ_{1} ∪ Γ_{2} as conclusions (cut-

link).

- If Π_{1} (resp. Π_{2}) is a proof-net with Γ_{1} ∪ {A} (resp. Γ_{2} ∪ {B}) as conclusions, and if Π_{1} and Π_{2} are disjoint (not connected), then

Π_{1} A Γ_{1}  ⊗  Π_{2} B  Γ_{2} is a proof-net with Γ_{1} ∪ Γ_{2} ∪ {A ⊗ B} as con-

clusions (⊗-link).

- If Π is a proof-net with Γ ∪ {A, B} as conclusions, then  Π B A Γ  _{_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}} is a

proof-net with Γ ∪ {A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B} as conclusions (^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link).

Some reductions operations can be de�ned on proof-nets that correspond to the notion of reduction in λ-calculus. There exists a theorem of cut-elimination for the proof-nets [23] and from now we only consider proof-nets without cut-links. Our goal is to de�ne intuitionistic proof-nets from the classical proof-nets. Let us recall that the order of the premises in the proof-nets is only essential in the non-commutative logic [18].

5.2 ORIENTED PROOF-NETS

The construction of proof-nets from a given formula or sequent, is based on the use of negation and on the following equivalences: (E ⊗F)^{⊥} = E^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F^{⊥}, (E ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F)^{⊥} = E^{⊥} ⊗F^{⊥}, and E −∘F = E^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F. In ILL the linear implication cannot be de�ned from the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connective because of the lack of negation. But in the spirit of using a classical proof to analyse the intuitionistic provability, it is interesting to keep the classical de�nition (and these equivalences) and to de�ne the intuitionistic one from it. It is done by the introduction of a

Figure 1.5 An oriented proof-net for ⊢ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ C)) −∘ A, B ⊗ C.

corresponding orientation to annotate each node of the structure with either the label I (for Input) or the label O (for Output) [5]. It allows to consider the classical structure and to add through some labels necessary information to detect, during the construction, if a proof-net is intuitionistic or not.

De�nition 21 Let Γ ⊢ Δ be a ILL sequent, the orientation of the formula tree is de�ned in the following way:

i) the formulae of Γ (resp. Δ) are labelled with I (resp. O). ii) a formula that is premise of a^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} or ⊗ connective that does not come from an implication transformation, has the same label as the formula conclusion. iii) a formula on the right-hand (resp. left-hand) side of a ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} or ⊗ connective that comes from an implication transformation, has the same (resp. opposite) label as the formula conclusion.

Then a proof-net with such labels or annotations is called an oriented proofnet. The example of Figure 1.5 presents an oriented proof-net corresponding to the sequent ⊢ (A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ C)) −∘ A, B ⊗ C. If we transform the −∘ connective and annotate the formulae then we obtain the following sequent, that is classically equivalent to the initial one: ⊢ ((A_{I}^{⊥} ⊗ (B_{I}^{⊥} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C_{I}^{⊥})_{I})_{I} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{O})_{O}, (B_{O} ⊗ C_{O})_{O}.

Property 22 An oriented proof-net has at least one conclusion with label O.

Proof By induction from the proof-nets de�nition. ■

Let us remark that there are proof-nets without conclusions labelled with I, for instance for provable sequents having no formula on the left-hand side.

De�nition 23 A ILL proof-net is an oriented proof-net without nodes of the

following form: \begin{matrix}O O \\ ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} \\ O \end{matrix} or \begin{matrix}I I \\ ⊗ \\ I \end{matrix}

Theorem 24 A sequent is provable in ILL if and only if its associated oriented proof-net is a ILL proof-net.

Proof It is a direct consequence of theorem 5. ■

5.3 FILL PROOF-NETS

The orientation de�ned in the previous section can be used to give a de�nition of a multiplicative FILL proof-net. The de�nition we propose is adapted from the one of Bellin for the multiplicative FILL + MIX [4].

De�nition 25 A dependency path is a path between a conclusion labelled with I and a conclusion labelled with O in a proof-net, that veri�es that one always go upwards (resp. downwards) through I- (resp.O-) oriented nodes.

The possible dependency subpaths, for each type of node, are given in Figure 1.6. Let us recall that a substructure S′ of a proof-structure S is a proof-structure that is a subgraph. Then a subnet of a proof-net is a substructure that is a proofnet [5]. Moreover, let P_{n} be a proof-net and A be one of its nodes, the empire of A is the largest subnet of P_{n} with A as conclusion.

De�nition 26 A FILL proof-net is an oriented proof-net such that for any node

A_{I} B_{O}_{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}...............^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} O} , there is no dependency path between A and a conclusion of the

empire of A that is different from this occurrence of B.

The Figure 1.7 presents two different proof-nets that correspond to the sequent proofs of section 4.2.2. The atomic formulae, that are A (resp. A^{⊥}) for the atoms labelled with O (resp. I), are not displayed. The �rst proof-net is not FILL because of the existence of a dependency path between the premise of the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} labelled with I and a node labelled with O which is not a premise of the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connective.

5.4 FILL PROOF-NETS CONSTRUCTION

We have previously studied the problem of automated construction of proofnets in different fragments of CLL like MLL, MALL or Non-Commutative MLL [17, 18, 19]. Some of the underlying principles could be applied for the case of multiplicative FILL fragment.

5.4.1 Principles for construction. We recall here the principles of our approach of proof-nets construction, taking the MLL fragment as illustration. More details can be found in [17, 19]. The construction is based on the inductive de�nition of proof-nets (see previous section) and instead of constructing

Figure 1.6 Dependency subpaths in FILL proof-nets

Figure 1.7 Proof-nets for A_{4} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A_{5}, A_{8} ⊢ A_{1} −∘ (A_{6} ⊗ A_{7}), A_{2} ⊗ A_{3}

a proof-structure and verifying with some criteria if it is a proof-net or not, subnets are built step by step to �nally obtain a proof-net. Let us consider a MLL sequent of the form ⊢ Δ. At �rst, we decompose the formulae to obtain a decomposition tree of the sequent. The construction of a proof-net corresponds to the construction of axiom-links that added to the decomposition tree forms a proof-structure that is in fact a proof-net. But how to �nd the suitable axiom-links (or connections) ? To �nd and justify the appropriate axiom-links, if they exist, we try to build, from some axiom-links (that are elementary proof-nets), some subnets that also are proof-nets, and to assemble them in the right way to �nally obtain a proof-net, by using three procedures: one to select, in the decomposition tree, a leaf to treat; one to treat the leaves, of the decomposition tree, by constructing some axiom-links; one to extend the existing structures (by assembling subnets) with links. As we aim to reduce the number of disjoint subnets during this construction process, we choose the formula to treat in branches, some leaves of which have already been treated. Another strategy, based on permutability results and on the inductive de�nition of proof-nets consists in always dealing with the ⊗ connective before the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connective, if possible, either to search the next leaf to treat or to assemble subnets. The search (-construction) of a proof-net follows these principles. To start we have to choose a branch and the successive nodes to �nally obtain a leaf and we consider the ⊗-nodes as a priority. Having selected such a leaf, we construct an initial subnet by construction of an axiom-link with a dual formula. Each time a new subnet is created, we want to assemble some of the subnets by extension with links in the following way: if the node under the current formula is a

- ⊗-node, both premises of which belong to disjoint subnets, then mix them into one new net with an extension with this node.

- ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -node, both premises of which belong to the same subnet, then add the node to this subnet.

- ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -node, both premises of which belong to disjoint subnets, then keep this node in a waiting position.

- ⊗-node, only one of the premises being treated, then treat the other premise as a priority. We go on by choosing a new formula to deal with, treating at �rst the ⊗ connectives and then the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connectives and trying to assemble subnets with the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} connectives being in the waiting position. At the end, if the proof-net exists then all formulae are treated and the resulting structure (or net) is the �nal proof-net. More details that are not necessary here can be found in [17, 18, 19]. Such an algorithm can be used to de�ne a connection-based proof-search method [15].

5.4.2 FILL vs CLL proof-nets. To take into account the criteria on paths in FILL proof-nets, we add a piece of information during the creation of each new node of the CLL net to memorize all the dependency chains between a conclusion with label I and a conclusion with label O of the current subnet. For that, we have to follow the construction rules given in Figure 1.6. It leads

Figure 1.8 Update of dependency paths for FILL proof-nets.

to the following algorithm, the essential points of which being summarized in Figure 1.8, where the dashed arrows are replaced by the plain arrows. Thus the intuitionistic provability is considered as a perturbation of classical proof-net construction.

During the creation of axiom-links: there exists a dependency path between the formula with label I and the one with label O.

During the creation of \begin{matrix}I I \\ ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} \\ I \end{matrix} or \begin{matrix}I I \\ ⊗ \\ I \end{matrix} links: the dependency paths be-

tween one of the premises and a conclusion labelled with O are all replaced by dependency paths between the new conclusion labelled with I and the same conclusion labelled with O.

During the creation of \begin{matrix}O O \\ ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} \\ O \end{matrix} or \begin{matrix}O O \\ ⊗ \\ O \end{matrix} links: the dependency paths be-

tween a conclusion labelled with I and one of the premises are all replaced by dependency paths between the same conclusion labelled with I and the new conclusion labelled with O.

During the creation of \begin{matrix}I O \\ ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} & ^{.} \\ O \end{matrix} link: if there exists a dependency path be-

tween the premise labelled with I and a conclusion O, different from the premise labelled with O, the proof-net is not FILL. Else, the dependency paths between a conclusion labelled with I and the premise labelled with O are all replaced by dependency paths between the same conclusion labelled with I and the new conclusion labelled with O; moreover the dependency paths, the origin of which being labelled with I, are suppressed.

During the creation of \begin{matrix}I O \\ ⊗ \\ I \end{matrix} : the dependency paths between a conclu-

sion labelled with I and a premise labelled with O are all replaced by the paths of same origin but extended with the paths starting from the premise labelled with I; the dependency paths starting of the premise labelled with I are replaced by paths starting from the new conclusion labelled with I.

During the construction of classical MLL proof-nets, we memorize the information about dependency paths between labelled occurrences of formulae and we then dynamically verify the condition of de�nition 26 characterizing a multiplicative FILL proof-net. The algorithm always build such a proof-net if there exists.

5.4.3 An example. Let us come back to the examples of Figure 1.7. The algorithm builds the decomposition tree and then develops the proof-net from the leaves (or axiom-links), in a top-down approach. It tries to create an axiom-link between a node labelled with I (that corresponds to A^{⊥}) and a node labelled with O (that corresponds to A). Then it memorizes a path between these formulae respectively labelled with I and O. Let us assume that there is an axiom-link between the formulae 1 and 2 (see the �rst example). We go on with a ⊗ connective linked to one of these treated formulae and decide to consider the other premise. We then create the axiom-link between formulae 3 and 4 and a path from 4 to 3. Moreover, we can construct the ⊗-link and the two paths memorized are modi�ed to point out on this ⊗-link. Therefore, the algorithm constructs the axiom-links and the ⊗-links and concludes with the construction of the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link. In this �rst example, the situation at the moment of the creation of ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link is presented in Figure 1.9. In fact, it is impossible to create this link because of the existence of the bold arrow and this proof-net is not FILL. Then by backtracking there are other attempts of axiom-links construction leading to a proposal that allows to construct the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link and then

Figure 1.9 Dependency paths before the creation of the^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link in Figure 1.7.

to a FILL proof-net (see the second example). Let us mention that, in general, the number of possibilities for the axiom-links is limited.

5.4.4 Main results. To prove the correction of the algorithm, it is necessary to consider two main properties.

Property 27 The algorithm memorizes all the dependency paths between a conclusion labelled with I and a conclusion labelled with O, and only these ones.

Proof The property is veri�ed, case by case, for each type of node. ■

Let us mention now a lemma about the existence of dependency path.

Lemma 28 Let P_{n} be a proof-net and A a node of P_{n} labelled with I, there exists a dependency path between A and a conclusion of P_{n}, labelled with O.

Proof The property 22 indicates that there always exists a conclusion labelled with O. This lemma is proved in a similar way, by induction on the proof-net de�nition. The axiom-link case is trivial. For the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} - and ⊗-links we can distinguish the case where the node I is the new one that has just been introduced. The signi�cative case is the one of ⊗, when the induction hypothesis gives a path between a node labelled with I and the unique premise of this ⊗-link that is labelled with O. A second use of the induction hypothesis (on the other net) allows the resulting path to be connected to the previous one. ■

This result leads to the following property:

Property 29 Let us consider a node A_{I} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B_{O} in a proof-net; then the existence of a dependency path between A_{I} and a conclusion labelled with O (different from B_{O}) is equivalent to the existence of a dependency path between A_{I} and a conclusion of the empire of A in the �nal proof-net, labelled with O.

Proof The proof uses classical properties of proof-nets, that are not detailed here (see [21]). It follows a schema similar to the proof of property 27 and uses the lemma 28 to deal with the case of the ⊗-link, the premises of which do not have the same orientation. ■

Theorem 30 Let Γ ⊢ Δ be a CLL sequent, the algorithm builds a FILL proof-net for it iff it is provable in FILL.

Proof It is a consequence of the algorithm properties and also of the previous properties and lemmas. ■

5.5 SOME REMARKS

The proof-nets construction algorithm for the multiplicative FILL has the property to simultaneously construct a sequent proof in a top-down (from axioms to �nal sequent) approach [17, 18]. Then we obtain an algorithm to directly construct a FILL proof if there exists and not only some criteria to verify if a CLL proof is also a FILL proof. As the previous algorithm �nds a FILL proof if there exists, the use of proof-nets allows to solve the completeness problem w.r.t. intuitionistic provability we have mentioned in previous sections. This signi�cant point illustrates, in the setting of linear logic, the interest of proof-net as an alternative tool for ef�cient automated deduction. We also observe the importance of the de�nition of labels for such a characterization. It appears from the works of Asperti on logical analysis of distributed systems that MLL plus the MIX rule might be more suitable for the representation of concurrent logical computations [3]. This rule

\begin{matrix}⊢ Γ & ⊢ Δ \\ ⊢ Γ, Δ \end{matrix} Mix

added to MLL has been also studied from the proof-net point of view by showing that the veri�cation of correctness for proof-nets in this logic is equivalent to a successful termination of a concurrent game in the style of Petri nets [3]. Re�nements and relationships with term assignments are proposed in [4] where a system of proof-nets for MLL (without constants) + MIX is given. From such a study of (multiplicative) classical linear logic, [4] has also proposed a proof-nets system for (multiplicative) FILL + MIX(without constants). Our results about intuitionistic provability can be extended and adapted to study the intuitionistic provability in MLL + MIX. It means that we can analyse it from the construction of a classical MLL + MIX proof-net with labels to detect the existence of a FILL + MIX proof-net. Such works could be signi�cant for ef�cient proof-search in the context of analysis and proofs in concurrent and distributed systems.

6. CONCLUSION

In this paper, we have de�ned labelled sequent calculi to analyse and characterize the intuitionistic provability from proof-search in classical logic. Our �rst approach, in CL and CLL, is based on characterizations of the axiom sequents of a given labelled sequent proof. It does not use speci�c terms as classical or linear λ-terms to represent proofs (coming from natural deduction systems) as in [30]. We could argue that such sequent calculi seem more suitable from both proof-theoretic and proof-search points of view. In case of CLL, a recent study has de�ned a classical linear λ-calculus [8] and similar calculi could be potentially used to encode CLL proofs and to characterize the intuitionistic proofs, but it could be hard to handle mainly if provability is the main interest. Anyway, we cannot have a completeness result, i.e. the intuitionistic provability cannot be claimed from any given classical proof. Our labelled proof systems can be seen as new formulations, based-on labels, on the FILL system and could be independently interesting from the proof-theoretic point of view. We have proposed an alternative to this characterization in CLL that is based on the proof-net notion, that can be seen as a counterpart of natural deduction in linear logic. For that, we give a new labelled proof system and an algorithm that allow to build an intuitionistic proof-net (and a sequent proof) from a classical proof-net search, for which we have well-de�ned principles. With such a structure we obtain the completeness result missing with the other systems. This point illustrates the interest of the proof-net notion as an ef�cient tool for proof analysis and proof-search in linear logic. Because of the relationships between proof-nets and some term assignments systems [1] and also because of possible choices between intuitionistic or classical logical fragments to consider some programming paradigms, like proofs-as-programs or proofs-as-processes, our results and their possible extensions, for instance with the MIX rule or with the additive connectives, could be very fruitful. The result, in terms of proof-nets, is particular to linear logic but could encourage us to have similar structures or some graph-theoretic characterizations of provability in other substructural logics and therefore to derive new methods to analyse and search proofs. Signi�cant points about the connected algorithmic and implementation problems will be studied in further work.

References

[1] S. Abramsky. Computational interpretations of Linear Logic. Theoretical Computer Science, 111(1-2):3�58, 1993.

[2] V. Alexiev. Applications of Linear Logic to Computation: An Overview. Bulletin of the IGPL, 2(1):77�107, 1994.

[3] A. Asperti. Causal dependencies in multiplicative linear logic with MIX. Math. Struct. in Comp. Science, 5:351�380, 1995.

[4] G. Bellin. Subnets of proof-nets in multiplicative linear logic with MIX. Math. Struct. in Comp. Science, 7:663�699, 1997.

[5] G. Bellin and J. van de Wiele. Subnets of proof-nets in MLL^{−}. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 249�260. Cambridge University Press, 1995.

[6] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In Int. Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 75�90, Utrecht, The Netherlands, March 1993.

[7] G.M. Bierman. A note on Full Intuitionistic Linear Logic. Annals of Pure and Applied Logic, 79:281�287, 1996.

[8] G.M. Bierman. Towards a classical linear λ-calculus (preliminary report). Electronic Notes in Theoretical Computer Science, 3, 1996.

[9] E. Boudinet and D. Galmiche. Proofs, concurrent objects and computations in a FILL framework. In Workshop on Object-based Parallel and Distributed Computation, OBPDC’95, LNCS 1107, pages 148�167, Tokyo, Japan, 1996.

[10] T. Bra�ner and V. De Paiva. Cut elimination for Full Intuitionnistic Linear Logic. Unpublished draft, 1996.

[11] M. D’Agostino and D.M. Gabbay. A Generalization of Analytic Deduction via Labelled Deductive Systems. Part I: Basic substructural logics. Journal of Automated Reasoning, 13:243�281, 1994.

[12] V. Danos and L. Regnier. The structures of multiplicatives. Arch. Math. Logic, 28:181�203, 1989.

[13] R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57:795�807, 1992.

[14] U. Engberg and G. Winskel. Completeness results for linear logic on Petri nets. Annals of Pure and Applied Logic, 86:101�135, 1997.

[15] D. Galmiche. Connection methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 1999. Accepted for publication.

[16] D. Galmiche and D. Larchey-Wendling. Provability in intuitionistic linear logic from a new interpretation on Petri nets - extended abstract. Electronic Notes in Theoretical Computer Science, 17, 1998.

[17] D. Galmiche and B. Martin. Proof search and proof nets construction in linear logic. In 4th Workshop on Logic, Language, Information and Computation, Wollic’97, Fortaleza, Brasil, August 1997. Logic Journal of IGPL, vol. 5-6, pp 883-885.

[18] D. Galmiche and B. Martin. Proof nets construction and automated deduction in non-commutative linear logic - extended abstract. Electronic Notes in Theoretical Computer Science, 17, 1998.

[19] D. Galmiche and G. Perrier. A procedure for automatic proof nets construction. In International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 42�53, St. Petersburg, Russia, July 1992.

[20] J.Y. Girard. Linear logic and parallelism. In Mathematical Models for the Semantics of Parallelism, LNCS 280, pages 166�182, Roma, Italia, October 1986.

[21] J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1�102, 1987.

[22] J.Y. Girard. Linear logic: its syntax and semantics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1�42. Cambridge University Press, 1995.

[23] J.Y. Girard. Proof nets: the parallel syntax for proof theory. In Ursini and Agliano, editors, Logic and Algebra, New York, 1995. M. Dekker.

[24] J.Y. Girard and Y. Lafont. Linear logic and lazy computation. In TAPSOFT 87, LNCS 250, pages 52�66, Pisa, Italia, March 1987.

[25] J. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Journal of Information and Computation, 110:327�365, 1994.

[26] M. Hyland and V. de Paiva. Full Intuitionistic Linear Logic (extended abstract). Annals of Pure and Applied Logic, 64:273�291, 1993.

[27] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In 7th IEEE Symposium on Logic in Computer Science, pages 235�246, Santa-Cruz, California, 1992.

[28] D. Miller. Forum: A multiple-conclusion speci�cation logic. Theoretical Computer Science, 165(1):201�232, 1996.

[29] M. Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 190�201, St. Petersburg, Russia, July 1992.

[30] E. Ritter, D. Pym, and L. Wallen. On the intuitionistic force of classical search. In 5th Int. Workshop TABLEAUX’96, LNAI 1071, pages 294�313, Terrasini, Palermo, Italy, May 1996.

[31] H. Schellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1(4):537�559, 1991.

[32] L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990.

30 LABELLED DEDUCTION

Appendix

1. A SEQUENT CALCULUS FOR CL

A ⊢ A ax  Γ ⊢ A, Δ Γ′, A ⊢ Δ′ Γ, Γ′ ⊢ Δ, Δ′ cut
{Γ ⊢ Δ \atop Γ, A ⊢ Δ} w_{L}  {Γ ⊢ Δ \atop Γ ⊢ Δ, A} w_{R} {Γ, A, A ⊢ Δ \atop Γ, A ⊢ Δ} c_{L}  {Γ ⊢ Δ, A, A \atop Γ ⊢ Δ, A} c_{R}
\begin{matrix}Γ ⊢ A, Δ & Γ, B ⊢ Δ \\ Γ, A → B ⊢ Δ \end{matrix} →_{L}  {Γ, A ⊢ B, Δ \atop Γ ⊢ A → B, Δ} →_{R}
\begin{matrix}Γ, A ⊢ Δ & Γ, B ⊢ Δ \\ Γ, A ∨ B ⊢ Δ \end{matrix} ∨_{L}  {Γ ⊢ A, Δ \atop Γ ⊢ A ∨ B, Δ} ∨_{R1} {Γ ⊢ B, Δ \atop Γ ⊢ A ∨ B, Δ} ∨_{R2}
{Γ, A, B ⊢ Δ \atop Γ, A ∧ B ⊢ Δ} ∧_{L}  \begin{matrix}Γ ⊢ A, Δ & Γ ⊢ B, Δ \\ Γ ⊢ A ∧ B, Δ \end{matrix} ∧_{R}
{Γ ⊢ A, Δ \atop Γ, ¬A ⊢ Δ} ¬_{L}  {Γ, A ⊢ Δ \atop Γ ⊢ ¬A, Δ} ¬_{R}

In the paper we use an equivalent presentation, without weakening rules (w_{L} and w_{R}) and where the axiom rule is replaced by Γ, A ⊢ A, Δ ^{ax}.

2. A SEQUENT CALCULUS FOR IL

A ⊢ A ax  {Γ ⊢ A Γ′, A ⊢ B \atop Γ, Γ′ ⊢ B} cut
{Γ, A, A ⊢ B \atop Γ, A ⊢ B} c {Γ ⊢ B \atop Γ, A ⊢ B} w ⊥ ⊢ A ⊥_{L}
\begin{matrix}Γ ⊢ A & Γ, B ⊢ C \\ Γ, A → B ⊢ C \end{matrix} →_{L}  {Γ, A ⊢ B \atop Γ ⊢ A → B} →_{R}
\begin{matrix}Γ, A ⊢ C & Γ, B ⊢ C \\ Γ, A ∨ B ⊢ C \end{matrix} ∨_{L}  {Γ ⊢ A \atop Γ ⊢ A ∨ B} ∨_{R1} {Γ ⊢ B \atop Γ ⊢ A ∨ B} ∨_{R2}
{Γ, A, B ⊢ C \atop Γ, A ∧ B ⊢ C} ∧_{L}  \begin{matrix}Γ ⊢ A & Γ ⊢ B \\ Γ ⊢ A ∧ B \end{matrix} ∧_{R}

3. ANOTHER SEQUENT CALCULUS FOR IL

A ⊢ A ax  Γ ⊢ A, Δ Γ′, A ⊢ Δ′ Γ, Γ′ ⊢ Δ, Δ′ cut
{Γ ⊢ Δ \atop Γ, A ⊢ Δ} w_{L}  {Γ ⊢ Δ \atop Γ ⊢ Δ, A} w_{R}  {Γ, A, A ⊢ Δ \atop Γ, A ⊢ Δ} c_{L}  {Γ ⊢ Δ, A, A \atop Γ ⊢ Δ, A} c_{R}
\begin{matrix}Γ ⊢ A, Δ & Γ, B ⊢ Δ \\ Γ, A → B ⊢ Δ \end{matrix} →_{L}  {Γ, A ⊢ B \atop Γ ⊢ A → B, Δ} →_{R}
\begin{matrix}Γ, A ⊢ Δ & Γ, B ⊢ Δ \\ Γ, A ∨ B ⊢ Δ \end{matrix} ∨_{L}  {Γ ⊢ A, Δ \atop Γ ⊢ A ∨ B, Δ} ∨_{R} {Γ ⊢ B, Δ \atop Γ ⊢ A ∨ B, Δ} ∨_{R}
{Γ, A, B ⊢ Δ \atop Γ, A ∧ B ⊢ Δ} ∧_{L}  \begin{matrix}Γ ⊢ A, Δ & Γ ⊢ B, Δ \\ Γ ⊢ A ∧ B, Δ \end{matrix} ∧_{R}
{Γ ⊢ A, Δ \atop Γ, ¬A ⊢ Δ} ¬_{L}  {Γ, A ⊢ \atop Γ ⊢ ¬A, Δ} ¬_{R}

Labelled Proof Systems for Intuitionistic Provability 31

4. A SEQUENT CALCULUS FOR CLL

A ⊢ A ax  Γ ⊢ A, Δ Γ′, A ⊢ Δ′ Γ, Γ′ ⊢ Δ, Δ′ cut
{Γ ⊢ Δ \atop Γ, 1 ⊢ Δ} 1_{L} ⊢ 1 1_{R} ⊥ ⊢ ⊥_{L} {Γ ⊢ Δ \atop Γ ⊢ ⊥, Δ} ⊥_{R} Γ, 0 ⊢ Δ 0_{L} Γ ⊢ ⊤, Δ ⊤_{R}
Γ ⊢ A, Δ Γ′, B ⊢ Δ′ Γ, Γ′, A −∘ B, ⊢ Δ, Δ′ ^{−∘^{L}}  {Γ, A ⊢ B, Δ \atop Γ ⊢ A −∘ B, Δ} ^{−∘^{R}}
Γ, A ⊢ Δ Γ′, B ⊢ Δ′ Γ, Γ′, A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ Δ, Δ′ ^{...............................................................................................} L  {Γ ⊢ A, B, Δ \atop Γ ⊢ A ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, Δ} ^{...............................................................................................} R
{Γ, A, B ⊢ Δ \atop Γ, A ⊗ B ⊢ Δ} ⊗_{L}  Γ ⊢ A, Δ Γ′ ⊢ B, Δ′ Γ, Γ′ ⊢ A ⊗ B, Δ, Δ′ ⊗_{R}
{Γ, A ⊢ Δ \atop Γ, A&B ⊢ Δ} &_{L1}  {Γ, B ⊢ Δ \atop Γ, A&B ⊢ Δ} &_{L2}  \begin{matrix}Γ ⊢ A, Δ & Γ ⊢ B, Δ \\ Γ ⊢ A&B, Δ \end{matrix} &_{R}
\begin{matrix}Γ, A ⊢ Δ & Γ, B ⊢ Δ \\ Γ, A ⊕ B ⊢ Δ \end{matrix} ⊕_{L}  {Γ ⊢ A, Δ \atop Γ ⊢ A ⊕ B, Δ} ⊕_{R1}  {Γ ⊢ B, Δ \atop Γ ⊢ A ⊕ B, Δ} ⊕_{R2}
{Γ ⊢ A, Δ \atop Γ, A^{⊥} ⊢ Δ} neg_{L}  {Γ, A ⊢ Δ \atop Γ ⊢ A^{⊥}, Δ} neg_{R}
{Γ ⊢ Δ \atop Γ,!A ⊢ Δ} ^{w^{L}} {Γ ⊢ Δ \atop Γ ⊢?A, Δ} ^{w^{R}} {Γ,!A,!A ⊢ Δ \atop Γ,!A ⊢ Δ} ^{c^{L}} {Γ ⊢?A,?A, Δ \atop Γ ⊢?A, Δ} ^{c^{R}}
{Γ, A ⊢ Δ \atop Γ,!A ⊢ Δ} ^{dir^{L}} {Γ ⊢ A, Δ \atop Γ ⊢?A, Δ} ^{dir^{R}} {!Γ, A ⊢?Δ \atop !Γ,?A ⊢?Δ} ^{pro^{L}} {!Γ ⊢ A,?Δ \atop !Γ ⊢!A,?Δ} ^{pro^{R}}

5. A SEQUENT CALCULUS FOR ILL

A ⊢ A ax  \begin{matrix}Γ ⊢ A & Γ′, A ⊢ B \\ Γ, Γ′ ⊢ B \end{matrix} cut
{Γ ⊢ A \atop Γ, 1 ⊢ A} 1_{L} ⊢ 1 1_{R} Γ, 0 ⊢ A 0_{L} Γ ⊢ ⊤ ⊤_{R}
\begin{matrix}Γ ⊢ A & Γ′, B ⊢ C \\ Γ, Γ′, A −∘ B, ⊢ C \end{matrix} ^{−∘^{L}}  {Γ, A ⊢ B \atop Γ ⊢ A −∘ B} ^{−∘^{R}}
{Γ, A ⊢ C \atop Γ, A&B ⊢ C} &_{L1}  {Γ, B ⊢ C \atop Γ, A&B ⊢ C} &_{L2}  \begin{matrix}Γ ⊢ A & Γ ⊢ B \\ Γ ⊢ A&B \end{matrix} &_{R}
\begin{matrix}Γ, A ⊢ C & Γ, B ⊢ C \\ Γ, A ⊕ B ⊢ C \end{matrix} ⊕_{L}  {Γ ⊢ A \atop Γ ⊢ A ⊕ B} ⊕_{R1}  {Γ ⊢ B \atop Γ ⊢ A ⊕ B} ⊕_{R2}
{Γ, A, B ⊢ C \atop Γ, A ⊗ B ⊢ C} ⊗_{L}  \begin{matrix}Γ ⊢ A & Γ′ ⊢ B \\ Γ, Γ′ ⊢ A ⊗ B \end{matrix} ⊗_{R}
{Γ ⊢ B \atop Γ,!A ⊢ B} ^{w^{L}} {Γ,!A,!A ⊢ B \atop Γ,!A ⊢ B} ^{c^{L}} {Γ, A ⊢ B \atop Γ,!A ⊢ B} dir {!Γ ⊢ A \atop !Γ ⊢!A} pro