A procedure for automatic proof nets construction^{⋆}

Didier Galmiche and Guy Perrier

CRIN - CNRS - INRIA Lorraine Campus Scientifique - B.P. 239 54506 Vandœuvre-les-Nancy Cedex France e-mail: galmiche{perrier}@loria.crin.fr

Abstract. In this paper, we consider the multiplicative fragment of linear logic (MLL) from an automated deduction point of view. Before to use this new logic to make logic programming or to program with proofs, a better comprehension of the proof construction process in this framework is necessary. We propose a new algorithm to construct automatically a proof net for a given sequent in MLL and its proofs of termination, correctness and completeness. It can be seen as an implementation oriented way to consider automated deduction in linear logic.

1 Introduction

Computer scientists can consider logic with two points of view: it can be an external reference to which they report during their activity, for example, to make correctness proofs of programs or it can be integrated as an internal tool for programming. In this work, we consider the second one. Intuitionism [16] has given at first a logical tool to approach programming in this connection. Centered around a constructive vision of truth, it allows to consider proofs as functions, lambda-calculus being a good framework to code them as programs. Considering the Curry-Howard correspondence [11] for which a proof is a λ-term (or a program) and a formula is a type (or a specification), the automatic program synthesis can be viewed as issued from automatic deduction: for a given specification, we construct a proof to extract a program from it [7]. But because of the unsymmetry of intuitionism it can be difficult to consider concurrency and reactive systems in this framework. The linear logic (LL) [9, 10] is a logic for actions introducing notions like controlled and strict management and resource consumption. It conserves a constructive character without having the default of absence of symmetry. A first step to consider the proofs as programs paradigm in LL can be to study automated deduction in this logic, knowing that the computational interpretation of LL can lead to a process paradigm opening up a new approach of parallel implementation of functional languages and of typed concurrent programming [1]. The point is to better understand what a proof is in LL consisting in a particular graph named proof net [6, 9]. But before considering the computational aspect and the synthesis of programs from proof nets using, for example, an adequate refinement of typed λ-calculus [15], one should be able to mechanize the construction of proofs, having in mind that propositional linear logic is undecidable [13]. In this paper, we give an algorithm to mechanize the construction of a proof net for a given sequent in multiplicative linear logic

⋆ International Conference LPAR’92, Logic Programming and Automated Reasoning, LNAI 624, pp 42-53

(MLL) sequent calculus. From this point, it will be able to study from an automated deduction point of view the application of deduction in linear logic in different fields as programming logic [2, 12] or plans generation [14]. In section 2, we give a concise presentation of linear logic and introduce in section 3 the concepts of logical structure and of proof net. In section 4, we focus on MLL and present the principle of automatic construction of proof nets. Section 5 includes an example to illustrate it. Section 6 contains the algorithm presentation and the main ideas about its proofs and section 7 presents some conclusions and perspectives.

2 Linear logic

Linear logic (LL) has been introduced by Girard [9] as a logic of actions. Born from the semantics of second order lambda-calculus, linear logic is more expressive than traditional logic (classical or intuitionistic ones). Characterized by the absence of structural rules and by a specific treatment of the negation, LL has proofs that can be considered as actions and introduces a dynamical resource management in these proofs without directional character. We refer the reader to [9, 10] for a broad explanation of the purpose and the meaning of LL.

2.1 The language The multiplicative linear logic (MLL) system language contains the propositional constants 1, ⊥, the unary connective ()^{⊥} (linear negation), the binary connectives ⊗ (times) and ℘ (par) with the axioms: A^{⊥⊥} = A, 1^{⊥} =⊥, ⊥^{⊥} = 1, (A ⊗ B)^{⊥} = A^{⊥}℘B^{⊥} and (A℘B)^{⊥} = A^{⊥} ⊗ B^{⊥}. The system AMLL extends the previous fragment to additive linear logic with the new constants ⊤ and 0, the new connectives & (with) and ⊕ (plus) satisfying ⊤^{⊥} = 0, 0^{⊥} = ⊤, (A&B)^{⊥} = A^{⊥} ⊕ B^{⊥} and (A ⊕ B)^{⊥} = A^{⊥}&B^{⊥}. The language for the propositional fragment of linear logic contains, in addition, the operator ! (of course!) and the operator ? (why not?) called modalities or exponentials, with the axioms (!A)^{⊥} =?A^{⊥} and (?A)^{⊥} =!A^{⊥}. The language for LL is defined using the quantifiers ∀ (every) and ∃ (some) with the axioms (∀xA)^{⊥} = ∃xA^{⊥} and (∃xA)^{⊥} = ∀xA^{⊥}.

2.2 The linear sequent calculus

\overline{⊢ A, A^{⊥}} Id  \frac{⊢ Γ, A ⊢ A^{⊥}, Δ}{⊢ Γ, Δ} Cut  \frac{⊢ Γ, B, A, Δ}{⊢ Γ, A, B, Δ} Ex

\frac{⊢ Γ}{⊢ Γ, ⊥} ⊥  \overline{⊢ ⊤, Δ} ⊤_{ax}  \overline{⊢ 1} 1_{ax}

Multiplicative rules

\frac{⊢ Γ_{1}, A_{1} ⊢ A_{2}, Γ_{2}}{⊢ Γ_{1}, A_{1} ⊗ A_{2}, Γ_{2}} ⊗  \frac{⊢ Γ, A_{1}, A_{2}}{⊢ Γ, A_{1}℘A_{2}} ℘

Additive rules

\frac{⊢ Γ, A_{1} ⊢ Γ, A_{2}}{⊢ Γ, A_{1}&A_{2}} &  \frac{⊢ Γ, A_{1}}{⊢ Γ, A_{1} ⊕ A_{2}} ⊕_{1}  \frac{⊢ Γ, A_{2}}{⊢ Γ, A_{1} ⊕ A_{2}} ⊕_{2}
\frac{⊢?Γ, A}{⊢?Γ,!A} ! \frac{⊢ Γ, A}{⊢ Γ,?A} d? \frac{⊢ Γ}{⊢ Γ,?A} w? \frac{⊢ Γ,?A,?A}{⊢ Γ,?A} c?

Exponential rules

3 The proof nets

We give here a precise and little different (compared to the classical one) presentation of the proof net concept. It corresponds in MLL to the double worry of machine implementation and study of information circulation in such structure. Here the nodes correspond to the information processors and the edges to channels for information circulation.

3.1 Proofs in LL

Considering the following proof (Π_{1}) of the sequent ⊢ A ⊗ B, B^{⊥} ⊗ C^{⊥}, A^{⊥}℘ C,

\frac{\frac{\frac{\overline{⊢ A, A^{⊥}} Id \overline{⊢ B, B^{⊥}} Id}{⊢ A ⊗ B, A^{⊥}, B^{⊥}} ⊗ \overline{⊢ C, C^{⊥}} Id}{⊢ A ⊗ B, B^{⊥} ⊗ C^{⊥}, A^{⊥}, C} ⊗}{⊢ A ⊗ B, B^{⊥} ⊗ C^{⊥}, A^{⊥}℘C} ℘

we observe that there is another one that differs only by the order in which rules are used. The idea is to represent a proof by a graph called proof net: A sequent ⊢ A_{1}, ..., A_{n} is represented by a box with n inputs-outputs labelled respectively A_{1}, ..., A_{n}. The internal structure of this box will represent a proof of the sequent and will constitute the proof net. A sequent being an axiom has, by definition, no proof associated. It will be represented by a black box only defined by its interface. Let us give at first the syntactic form of proofs named logical structure.

3.2 Logical structure

The edges are oriented and labelled by formulas of MLL. We have five node types, such a node determining the number of edges to which it is connected and the particular relationship linking formulas attached to these edges.

[figure: A; I/O] (in-out) [figure: A^{⊥}; A; Id] (id) [figure: A^{⊥}; A; Cut] (Cut)

[figure: A ⊗ B; B; A; ⊗] (times) [figure: A℘B; B; A; ℘] (par)

A graph respecting this syntactic form is a logical structure. Of course, a given logical structure does not represent necessarily a proof. It has to verify certain criteria to become a proof net. We will define it inductively from elementary proof nets associated with identity axioms. To each inference rule corresponds directly a rule for the proof net construction.

3.3 Proof nets

A sequent proof is inductively built from axioms by application of the inference rules. In a similar way, we can inductively construct the proof nets that correspond to proofs in LL.

Definition 1. A proof net for MLL (a PN) is defined inductively by:

(0) The logical structure [figure: A^{⊥}; A; Id; I/O; I/O]  is an elementary PN.

[figure: (1) If; A; I/O; \overline{Π_{1}}; and; A^{⊥}; I/O; \overline{Π_{2}}; are disjoint PN’s then]

[figure: A^{⊥}; A; Cut; \overline{Π_{2}}; \overline{Π_{1}}]  is a PN.

[figure: (2) If; A; I/O; \overline{Π_{1}}; and; A^{⊥}; I/O; \overline{Π_{2}}; are disjoint PN’s then]

[figure: ⊗; B; A; A ⊗ B; I/O; \overline{Π_{2}}; \overline{Π_{1}}]  is a PN.

[figure: (3) If; B; A; I/O; I/O; \overline{Π}; is a PN then; ℘; I/O; \overline{Π}; A; B; A℘B; is a PN.]

Remark. Moreover, we can extend the construction rules for the treatment of the additives connectives but our aim is to focus on proof nets in MLL.

The rules defined above allow to associate naturally a proof net \overline{Π} to a sequential proof Π in MLL. This notion of proof net inductively defined corresponds to the classical ones based on some information circulation criteria [4, 9].

3.4 Example

We can construct at the same time the sequential proof Π_{1} (see 3.1) and the corresponding proof net \overline{Π_{1}} for the sequent ⊢ A ⊗ B, B^{⊥} ⊗ C^{⊥}, A^{⊥}℘C. Whatever order is used to apply the construction rules, the final proof net is the same. The set of input/output with the opening on edges constitutes the external interface of the box associated to the sequent.

[figure: B^{⊥} ⊗ C^{⊥}; A ⊗ B; B^{⊥}; B; A; C^{⊥}; C; A^{⊥}; A^{⊥}℘C; ⊗; ⊗; ℘; I/O; I/O; I/O; Id; Id; Id]

4 Principle of automatic proof nets construction

We can consider forward or backward chaining for proof nets construction. We use here the first one, considering elementary proof nets, associated with identity axioms and using construction rules; it is a step by step construction through successive connections, resulting in more complex proof nets. The problem here consists in having an algorithm allowing to decide if a given sequent ⊢ A_{1}, A_{2}, ..., A_{n} in MLL is provable or not and to construct an associated proof net. According to the Gentzen Haupsatz, we can only consider proofs without cuts.

4.1 Free edges association by duality

The formulae A_{1}, A_{2}, ..., A_{n} of the sequent to prove determine what we call the terminal branches of the proof net to construct.

Definition 2. A terminal branch is a connected component (of the future proof net) without the nodes representing identity axioms.

Considering this definition, we can associate a terminal branch B_{i} with each formula A_{i} of the sequent to prove. After the creation of the terminal branches B_{1}, B_{2}, ..., B_{n}, we have to associate their free edges by duality.

Definition 3. i) An edge is free, in a terminal branch, if it has no start node. ii) Two edges are dual if they are labelled by dual formulae (negation of each other).

If we are not careful, an association by duality of two free edges can lead to several disjoint proof nets. For example, the sequent ⊢ A, A^{⊥}, B, B^{⊥} is not provable and such association by duality leads to two disjoint proof nets. To avoid it, we distinguish one the terminal branches chosen as start point of the proof net in construction G.

Definition 4. A proof net in construction G is a connected graph obtained by association of dual free edges of terminal branches, using identity axioms.

We associate only from free edges of G so as to preserve the connexity. The construction stops when G has no more free edges. There are two possibilities: a) terminal branches remain that are not connected to G (it is not the expected result), b) no terminal branches remain, that is the expected result provided that we can prove that the logical structure obtained is a proof net.

4.2 Correction verification and chaining activation

In case b) we are not sure that the structure is a proof net. But rather than make an a posteriori verification (including a complete reconstruction in case of negative result), we prefer to make it during the construction building, at the same time and step by step, G and a set R of proof nets that are fragments of G. At the beginning R is empty. But each new association produces an elementary net added to R. Moreover the elements of R are nets opening on known nodes that are either inputs/outputs or connectors times or par. When two elements \overline{Π_{1}} and \overline{Π_{2}} in R open on the same times connector, we activate this one. Then \overline{Π_{1}} and \overline{Π_{2}} are replaced in R by a unique more complex net. Likewise, when an element \overline{Π_{0}} of R has two edges opening on the same connector par, this one is activated and \overline{Π_{0}} is replaced in R by the new net resulting of this activation. Each new association can thus start a chaining activation of binary connectors. During the construction, the elements of R are more and more complex and if the construction succeeds, R consists, at the end, of the expected net.

4.3 Incorrectness and backtracking

The construction of R is not necessarily linear. It is possible to create incorrect intermediate nets. For example, it can happen that an element of R element has two inputs/outputs opening on the same connector times. In this case, we make a backtracking on the last association. This possibility of backtracking imposes us to conserve an important quantity of knowledge : for each element of R an history of its construction and an history of dual free edges of effective associations.

4.4 Duality property

Before considering the net construction, it would be interesting to have simple criteria easy to verify that allow to filter certain classes of non provable sequents with a view to eliminating it directly. In a proof in MLL we have a conservation of the atoms and then the following property (of duality): If a sequent is provable in MLL then the multi-set of these atoms can be split into pairs of dual atoms.

5 An example

We aim to prove the sequent: ⊢ A ⊗ B, (A^{⊥}℘B^{⊥}) ⊗ A, A^{⊥} ⊗ B, B^{⊥}. It corresponds to the search of a proof net being the internal structure of the following box:

[figure: B^{⊥}; A ⊗ B; A^{⊥} ⊗ B; (A^{⊥}℘B^{⊥}) ⊗ A; I/O; I/O; I/O; I/O]

The duality property being verified, we consider the terminal branches for A⊗B (1), (A^{⊥}℘B^{⊥}) ⊗ A (2), A^{⊥} ⊗ B (3), B^{⊥} (4) . Let us choose the branch 1 as starting point of the construction of G. Among the two free edges A and B, we decide to associate the edge A. Between the possibilities for association with A: edge A^{⊥} of branch 2 or of branch 3, we choose the first one.

A first consequence of this association is to extend G to branch 2 and a second one is the creation of the elementary net ◯ 1 (to indicate it in the figure we numerate their terminal edges). This new proof net is the first element of the set R. Hence, the figure below (intermediate proof nets created during the construction are in bold)

[figure: 1; id; 1; I/O; I/O; I/O; I/O; branch 4; B^{⊥}; B; ⊗; ⊗; ⊗; ℘; A^{⊥}; B^{⊥}; A^{⊥}℘B^{⊥}; A; (A^{⊥}℘B^{⊥}) ⊗ A; A^{⊥}; A^{⊥} ⊗ B; branch 1; branch 2; branch 3; A ⊗ B; B; A]

G has three free edges. Let us choose the edge B of branch 1 and associate it, for example, with the edge B^{⊥} of branch 2. We note ◯ 2 this new elementary net that we add to R. Then R = {◯ 1 , ◯ 2 }. We are trying a chaining connection of elements of R from the edge B (just considered) and then from B^{⊥}. The function connections-propagation realizes this task in the algorithm. Seeing that B opens on a times connector, that is the arrival of the net ◯ 1 of R, this connector can be activated. It means we gather the nets ◯ 1 and ◯ 2 to constitute a new one ◯ 3. We verify that the connection is correct because the nets ◯ 1 et ◯ 2 are independent and then we can replace in the set R the nets ◯ 1 and ◯ 2 by ◯ 3. Then R = {◯ 3 }. The successor node of current node times is an input-output then the chaining connection from the edge B from branch 1 stops. We attempt the same process from the previous free edge B^{⊥} of branch 2. The connector par of branch 2 can now be activated and by connection of the two terminal edges of net ◯ 3 we obtain the net named ◯ 4.

[figure: I/O; id; id; 3; 2; 3; 1; 2; 1; 3; 4; 4; I/O; I/O; I/O; A; B; A ⊗ B; branch 3; branch 2; branch 1; A^{⊥} ⊗ B; A^{⊥}; (A^{⊥}℘B^{⊥})⊗A; A; A^{⊥}℘B^{⊥}; B^{⊥}; A^{⊥}; ℘; ⊗; ⊗; ⊗; B; B^{⊥}; branch 4]

We verify that this creation is correct, considering that the connected edges belong to the same net. Then we can replace in R the net ◯ 3 by the net ◯ 4. The successor of the current node par is a times with a free initial edge then the chaining connection stops. Now G has only one free edge: the edge A of branch 2 that can only be associated with the edge A^{⊥} of branch 3. We continue in a similar way until there is no more free edge. Consequently, the construction is terminated and is successful because there is no more terminal branch not connected to G. The final net is

[figure: I/O; id; id; id; id; 6; 6; 6; 7; 8; 8; 8; 8; 7; I/O; I/O; I/O; A; B; A ⊗ B; branch 3; branch 2; branch 1; A^{⊥} ⊗ B; A^{⊥}; (A^{⊥}℘B^{⊥}) ⊗ A; A; A^{⊥}℘B^{⊥}; B^{⊥}; A^{⊥}; ℘; ⊗; ⊗; ⊗; B; B^{⊥}; branch 4]

6 Proof net construction algorithm

6.1 Algorithm presentation

Definition 5. The following definitions are function or predicate definitions used in the proof net construction algorithm:

1) The set duality-test(A) is the set of free edges A^{⊥} that have already been tested for the association with A.

2) The set assoc-edges is the set of the edges that have been associated.

3) The set R is the set of the (already constructed) intermediate nets.

4) The graph G is the net under construction.

5) The set term-branch(⊢ Γ) is the set of the terminal branches of ⊢ Γ.

6) duality(⊢ Γ) is true if the sequent ⊢ Γ verifies the duality property.

7) exist-free-edge(S) is true if there exists a free edge in S.

8) property-free-edge(E) is true if E is a free edge leading, if possible, to a binary connector that is the opening of a net from R and situated as high as possible in G.

9) good-link(A,A^{⊥}) is true if the union of G (including A) and the terminal branch of B including A^{⊥} has another free edges when B is not reduced to this union.

10) new-graph(G,A,A^{⊥}) is the graph obtained from G by associating the open edge A of G with the open edge A^{⊥} of G or B.

11) elem-proof-net(A,A^{⊥}) is the new elementary proof net constructed through the association of A and A^{⊥}.

The algorithm (see appendix) formalizes what has been described through the example. It uses the intermediate function connections-propagation, that takes a net G under construction, a set R of intermediate already constructed proof nets and a node current-node of G as inputs and returns an incorrectness message or a set R′ of intermediate proof nets. It activates by chaining the binary connectors of G from the node current-node following the order determined by the edges of G and going as far as possible. If, during this chaining connection, we detect an incorrectness, the function returns a message giving it else R′ is the result of the successive activations of times and par.

6.2 Properties of the algorithm

Termination. The termination proof consists in proving the termination by associating with each loop in the algorithm a function with parameters characterizing the execution state of the algorithm. The value of the function will strictly decrease during the execution of the loop.

Correctness.

Proposition 6. the function net-construction, if it succeeds, returns a net \overline{Π}, being correct and constituting a proof of the sequent ⊢ Γ given as input.

Proof. 1) Let us prove that \overline{Π} is correct. It is sufficient to prove that the set R of intermediate created nets is, at any time of the execution of the algorithm, a set of correct nets. Let R_{k} be the value of R after the execution of the k^{th} step of the algorithm. Because of the termination of the algorithm, the sequence of values of R is finite and can be written R_{0}, R_{1}, ..., R_{n} where R_{0} is ∅ and R_{n} = \{\overline{Π}\} (considering that we are in the case where construction succeeds). We consider the following property: After the execution of the k^{th} step, the resulting set R_{k} is a set of correct sets, that can be proved by induction on k. Then, it is true for all k ≤ n and so for n. Consequently, \overline{Π} is a correct net.

2) Let us prove that \overline{Π} is a proof of ⊢ Γ, i.e., the set of formulae constituting the inputs-outputs of \overline{Π}, is the set of the formulae of ⊢ Γ. At first, we prove that each input-output of \overline{Π} is a formula of ⊢ Γ. As G is connected and has its inputs-outputs coinciding with the formulae of ⊢ Γ we have the result.

Completeness. Before beginning the completeness proof, we need to introduce the notion of trace-construction of a net with a corresponding proposition.

Definition 7. A trace-construction of a proof net \overline{Π} is a finite sequence R_{0}, R_{1}, ..., R_{n} of net sets that verifies (i) - R_{n} = \{\overline{Π}\} (ii) for all k such that 0 ≤ k < n, R_{k+1} is obtained from R_{k} by the connection of two elements of R_{k} with a times or the connection of two terminal edges of an R_{k} element with par.

Proposition 8. If (R_{k})_{0≤k<n} is a trace-construction of a proof net \overline{Π} and if there exists h such that 0 ≤ h < n and R_{h+1} obtained from R_{h} by activation of a par (resp. times) on two edges that were terminal edges of a net (resp. of two distinct nets) of R_{0}, then there exists a trace-construction (R′_{k})_{0≤k<n} of \overline{Π} such that R′_{0} = R_{0} and R′_{1} are obtained from R′_{0} by activation of the operator par (resp. times).

Proof. By induction on h.

Definition 9. A set of generator nets of a proof net \overline{Π} is a part of the first term of a trace-construction of \overline{Π}.

Proposition 10. If ⊢ Γ is a provable sequent in the multiplicative linear logic then the function net-construction applied to ⊢ Γ returns a proof net of ⊢ Γ.

Proof. Let us reason by refutation. We assume that the function net-construction returns a failure message and consider Π a particular proof net of ⊢ Γ and n the number of the identity axioms it contains (n is strictly positive and depends only on ⊢ Γ). We have to prove the following property P(k)( 0 ≤ k < n): At a certain time during the execution of the algorithm net-construction, one succeeds in associating k free edges, and R is then a set of generators net of \overline{Π}. \underline{proof}. 1) P(0) is true. At the beginning of the execution, we do not try to associate a free edge with another one and R is empty.

2) Let us assume P(k) is true for 0 ≤ k < n and prove that P(k+1) is true. Let us consider the time when one has succeeded in associating k free edges and then R is a set of generator nets of Π (it is possible because P(k) is true). k < n and free edges remain in G because G is never closed while all terminal branches are not linked. Let A be the free edge that is going to be selected by the algorithm and A^{⊥} the one to which A is linked by an identity axiom in Π. R is a set of generator nets of Π and A^{⊥} is necessarily a free edge at this time. By hypothesis, the algorithm fails to construct a proof net of ⊢ Γ and then all the eventual associations of A with a dual edge are going to fail; it implies that, at one time, we attempt to associate A with A^{⊥}. Let us consider the time when A and A^{⊥} are linked by an identity axiom and when we call the function connections-propagation for A. We have to prove that the propagation succeeds and that the resulting R is a set of generator nets of Π. Let p the number of iterations of loop 3) that will be executed, we can prove by induction for 0 ≤ h ≤ p the following property Q(h): After h executions of loop 3) there is no incorrectness and the set R remains formed with generators of Π(the proof uses the trace-construction concept). Particularly Q(p) is true and then the propagation of the connections from A has succeeded and the resulted R is a set of generator nets of Π. We can do the same proof for the connections propagation from A^{⊥}. The association of A and A^{⊥} has succeeded and the set R is a set of generators of Π. Then P(k+1) is true. We proved that P(k) is true for all k such that 0 ≤ k ≤ n. □ P(n) is true and the algorithm succeeds for the construction of Π, that is in contradiction with the initial hypothesis. If ⊢ Γ is provable then the algorithm succeeds in constructing a proof net for it.

7 Conclusion

We have proposed a procedure to construct a proof net automatically for a given sequent in MLL. From this study we have a better view of the concept of proof net in linear logic and we can consider some applications with it as logical framework. The connections between proof nets and proof-search algorithms for matrix-methods (connections [5] or matings [3]) would be studied and this algorithm could be helpful for such a work. Linear logic seems an adequat framework to consider plans generation from a logical point of view [14]. If we consider the conjunctive planning using MLL with proper axioms, a plan corresponds to a proof net. Some extensions of the algorithm for the proper axioms treatment are possible. Considering logic programming, we can extend Prolog in the framework of MLL, in the same spirit as [2], but the expressivity gain is not obvious and moreover ⊗ sets some performance problems. But some works, like [12], emphasize the necessity to extend the work, for logic programming application, to additive and multiplicative linear logic (AMLL) and even to LL. To do this, we have two possibilities: the first one is to extend the proof net notion to AMLL [4] and to consider its automated construction by a similar approach. A second one is to consider the problem of proof construction directly in AMLL with a specific, and completely different, decision procedure [8] and to study its relationship with extension of proof nets notion. Even so, this mechanization of proof net construction in MLL is a step for the use of proof net, having in mind its computational interpretation.

References

1. S. Abramsky. Computational interpretations of linear logic. technical report, Department of Computing, Imperial College, London SW7 2Bz, England, 1991.

2. J.M. Andreoli and R. Pareschi. Logic programming with sequent systems: A linear logic approach. In Int. Workshop on Extensions of Logic Programming, LNCS 475, pages 1–30, Tübingen, Germany, December 1989.

3. P. Andrews. Theorem proving via general mating. Journal of ACM, 28(2):193–214, 1981.

4. G. Bellin. Proof nets for multiplicative and additive linear logic. Technical Report ECS-LFCS 91-161, Department of Computer Science, Edinburgh University, May 1991.

5. W. Bibel. On matrices with connections. Journal of ACM, 28(4):633–645, 1981.

6. V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.

7. D. Galmiche. Constructive system for automatic program synthesis. Theoretical Computer Science, 71(2):227–239, 1990.

8. D. Galmiche and G. Perrier. Automated deduction in additive and multiplicative linear logic. In Logic at Tver ’92, Logical Foundations of Computer Science Symposium, Tver, Russia, July 1992.

9. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

10. J.-Y. Girard. Towards a geometry of interaction. In J.-W. Gray and A. Scedrov, editors, AMS Conference on categories in computer science and logic, pages 69–108, Boulder-Colorado, June 1987.

11. J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, 1989.

12. J. S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE symposium Logic in Computer Science, pages 32–42, Amsterdam, July 1991.

13. P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. In 31st annual IEEE Symp. on Foundations of Computer Science, St-Louis, Missouri, October 1990.

14. M. Masseron, C. Tollu, and J. Vauzeilles. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pages 63–75, Bangalore, India, December 1990.

15. U. Solitro. A typed calculus based on a fragment of linear logic. Theoretical Computer Science, 68:333–342, 1989.

16. A.-S. Troelstra and D. Van Dalen. Constructivism in Mathematics, an Introduction. North-Holland, Amsterdam, 1988.

A The algorithm

function net-construction

input: a sequent ⊢ Γ of MLL. output: a proof net \overline{Π} or a failure message specification: If ⊢ Γ is provable then \overline{Π} is a proof net of ⊢ Γ else the function returns a failure message.

begin if not duality-property(⊢ Γ) then return ”failure” endif B := term-branch(⊢ Γ); for each free edge A of terminal branches in B do duality-test(A) := ∅ endfor; assoc-edges := ∅; R := ∅; G := one of the terminal branches of B; B := B - {G}; while exist-free-edge(G) do choose a free edge A of G with property-free-edge(A); nosuccessassoc := true; while there exists in the graphs in B a free edge A^{⊥} ∉ duality- test(A) such that good-link(A,A^{⊥}) and nosuccessassoc. do choose a free edge A^{⊥} of B ∉ duality-test(A) such that good-link(A,A^{⊥}) and property-free-edge(A^{⊥}); duality-test(A) := {A^{⊥}} ∪ duality-test(A); G := new-graph(G,A,A^{⊥}); update(B); R := R ∪ {elem-proof-net(A,A^{⊥})}; R := connections-propagation(G, R, A); if R ≠ incorrectness then R:=connections-propagation(G,R,A^{⊥}) endif nosuccessassoc := (R=incorrectness); if nosuccessassoc then give back to G, B, R the initial values before the asso- ciation attempt of A with A^{⊥} endif endwhile if not(exist-free-edge(G)) and card(R) ≠ 1 then nosuccessassoc := true endif. if nosuccessassoc then duality-test(A) := ∅; if assoc-edges = ∅ then return ”failure” else extract the head A’ of assoc-edges ; Give back to G, B, R the initial values before the asso- ciation attempt of A’ with A^{′⊥} endif else assoc-edges := cons(A ,assoc-edges ) endif

endwhile return the unique net \overline{Π} element of R;

end