Calculi with dependency relations for Mixed Linear Logic - extended abstract -

D. Galmiche, J.M. Notin

LORIA–Université Henri Poincaré Campus Scientifique, BP 239 Vandœuvre-lès-Nancy, France

Abstract

In this paper we propose new calculi for the multiplicative fragment of Mixed Linear Logic (MMLL) which is a logic that combines both commutative and noncommutative connectives. These based-on sequent and proof net calculi, that can be seen as a new proof-theoretical formulation of MMLL, are based on the definition of dependency relations. We provide a proof-search procedure for MMLL that is based on proof nets construction with associated sets of dependencies.

1 Introduction

Many works have been recently devoted to the study of linear logic [10] (or some of its fragments) and its ability, as a logic of resources, to be easily and strongly related with different topics in computer science, like process calculi or concurrent constraint programming [3]. In many cases, it appears that commutative linear logic is not enough expressive to specify processes having both asynchronous and synchronous behaviors and thus a possible solution can be the use of non-commutative logic [2] or non-commutative connectives to deal with sequentiality. Recently, a mixed version of classical propositional linear logic, which combines both commutative and non-commutative connectives, has been proposed [1] with the motivation to define logical characterizations of synchronization mechanisms in concurrent constraint programming [15]. But in order to apply such a logic to process calculi and concurrent programming (specification, verification) it is necessary to have new proof systems and related efficient proof-search methods.

Preprint submitted to Elsevier Science 16 July 2001

The multiplicative fragment of Mixed Linear Logic ^{1} (MMLL) extends the commutative multiplicative linear logic (MLL) and the non-commutative (or cyclic) multiplicative linear logic (NCMLL). We naturally consider our previous works, based on the concept of proof net, dedicated to proof search in both fragments [6,7] but in MMLL an essential step consists in understanding and analyzing the interaction between commutative and non-commutative connectives during the proof-search process. We have recently studied two proof search methods in MMLL that were based on the definition of labelled (with constraints) proof nets [8], the labels allowing in the former to fix some constraints to satisfy during the proof net construction and in the latter to propagate some informations useful to guide and control the search. Such based-on proof nets methods are useful to efficiently detect the non-provability.

In this paper, we propose new sequent and proof net calculi for the multiplicative fragment of Mixed Linear Logic (MMLL). These calculi are based on the definition of dependency-relations and provide a new formulation of MMLL based on such relations in the spirit of [5]. Such new proof systems allow to naturally consider this logical fragment as a particular refinement of the MLL fragment. Moreover the definition of dependencies (or constraints) attached to the calculi is a natural way to translate some proof-theoretical results of MMLL into simple and tractable automated proof-search procedures, that are based on the construction of semantical structures like proof nets [6,11]. After the study of the relationships between both systems (adequacy and sequentialization), we propose a based-on proof nets algorithm for proof construction in MMLL that builds in parallel a proof structure (like in MLL) and a set of dependencies on which we have to verify some validity conditions. In order to have a simple and efficient verification process on the dependencies, we propose refinements of both calculi that include dependencies with constraints. Such systems will be more deeply studied in order to analyze the execution of programs or to prove systems properties specified in such a mixed logic. Moreover our new proof net definition provides a new correctness criterion for MMLL that will be studied from both complexity and algorithmic points of view.

2 Mixed Non-Commutative Linear Logic

In this section we consider the multiplicative fragment of mixed linear logic, called MMLL, that is an extension of both commutative (MLL) and noncommutative or cyclic (NCMLL) linear logic [15]. This logic is an alternative to commutative classical, intuitionistic or linear logics for applications in

1 In [1], this logic is called non-commutative linear logic. Here we keep the initial appellation of mixed linear logic to avoid some confusions.

linguistics or computer science (process calculi or concurrent constraint programming [15]).

2.1 Motivations and applications

Let us first illustrate the motivations and the interest to have a logical fragment where commutative and non-commutative connectives cohabit, with an example coming from the concurrent constraint (CC ) programming [15]. Let us consider the problem of two processes (p_{1} and p_{2}) that request the same two resources (r_{1} and r_{2}). It can be expressed in CC by

P = tell(r_{1}) ∥ tell(r_{2}) ∥ \underbrace{r_{1} → r_{2} → (tell(r_{1}) ∥ tell(r_{2}))}_{p_{1}} ∥ \underbrace{r_{2} → r_{1} → (tell(r_{2}) ∥ tell(r_{1}))}_{p_{2}}

In this expression ∥ represents the parallel composition of processes ; tell(r_{1}) allows to state that the resource r_{1} is available. Moreover p_{1} ≡ r_{1} → p′_{1} expresses that p_{1} waits for the resource r_{1} to be available, and then consumes this resource to become p′_{1}. Obviously, this situation can lead to a deadlock, that is to say :

D = \underbrace{r_{2} → (tell(r_{1}) ∥ tell(r_{2}))}_{p′_{1}} ∥ \underbrace{r_{1} → (tell(r_{2}) ∥ tell(r_{1}))}_{p′_{2}}

where p′_{1} and p′_{2} both wait for resources that are no more available, because p_{1} has consumed the resource r_{1}, and p_{2} has consumed the resource r_{2}.

In order to characterize such properties, programs or expressions like P or D can be translated into a particular logic. For instance, P is translated into commutative linear logic, in which formulae are considered as resources, as follows:

P̂ = r_{1} ⊗ r_{2} ⊗ (r_{1} ⊸ (r_{2} ⊸ (r_{1} ⊗ r_{2}))) ⊗ (r_{2} ⊸ (r_{1} ⊸ (r_{1} ⊗ r_{2})))

where ⊸ is the linear implication, and ⊗ is the multiplicative conjonction.

Unfortunately, because of logical interactions between ⊗ and ⊸, we cannot use the validity in commutative linear logic in order to state that the program P can lead to the above deadlock D. It appears necessary to use a non-commutative linear implication −•, together with ⊗, in order to express that the program P can lead to the deadlock situation D. The formula representing our program is :

P̌ = r_{1} ⊗ r_{2} ⊗ (r_{1} −•(◇ ⊗ (r_{2} −•(◇ ⊗ r_{1} ⊗ r_{2})))) ⊗ (r_{2} −•(◇ ⊗ (r_{1} −•(◇ ⊗ r_{2} ⊗ r_{1}))))

where ◇ is a new atomic formula. Following the same translation, the deadlock D is represented by the formula :

(r_{2} −•(◇ ⊗ r_{1} ⊗ r_{2})) ⊗ (r_{1} −•(◇ ⊗ r_{1} ⊗ r_{2}))

Thus the fact that P can lead to D is ensured by the validity of the se-

quent r_{1} ⊗ r_{2} ⊗ (r_{1} −•(◇ ⊗ p′_{1})) ⊗ (r_{2} −•(◇ ⊗ p′_{2})) ⊢ ◇ ⊗ ◇ ⊗ 1 ⊗ p′_{1} ⊗ p′_{2} (where p′_{1} = r_{2} −•(◇ ⊗ r_{1} ⊗ r_{2}) and p′_{2} = r_{1} −•(◇ ⊗ r_{1} ⊗ r_{2})) in Mixed Linear Logic. It can

be done by proof-search for this sequent in one of the sequent calculi of this logic.

Therefore, we see that a logic like linear logic, in which formulae can be seen and treated as resources or agents, is necessary to some specificy properties of real systems. Moreover, the use of mixed linear logic, where commutative and non-commutative connectives cohabit, is necessary to obtain the logical characterization of finer operational aspects of concurrent constraints computations (stores, successes and suspensions) with synchronization constraints [15].

In addition to this ability to represent mechanisms or properties dealing with sequentiality and concurrency, this logic can also offer new perspectives to the connection between concurrency and proof theory, with the paradigm of logic programming (proof-search as computation). Therefore, one could propose new definitions or extensions of process calculi [4,12] where sequentiality and concurrency can cohabit, following such a correspondence with Mixed Linear Logic. It suggests new investigations of the semantics of concurrency from proof theory.

In order to study the execution of programs (agents) or to prove systems properties specified in such a mixed logic, appropriate proof systems (sequent or proof net calculi) are required. We will propose such new calculi in this paper, focusing on the syntax of proof nets (particular proof graphs in linear logic) that is more suited for the representation of concurrent computations [11] but, as recently shown, also for proof construction in commutative and non-commutative linear logic [7].

2.2 A sequent calculus with explicit structural rules

The formulae (of MMLL) are build from literals p, q, …, p^{⊥}, q^{⊥}, … with noncommutative connectives (conjunction ⊙ and disjunction ⊲), commutative connectives (conjunction ⊗ and disjunction & ). The negation is defined as follows with the De Morgan laws: (p)^{⊥} = p^{⊥}, (p^{⊥})^{⊥} = p, (A⊙B)^{⊥} = B^{⊥} ⊲A^{⊥}, (A⊲B)^{⊥} = B^{⊥}⊙A^{⊥}, (A⊗B)^{⊥} = B^{⊥} & A^{⊥}, (A & B)^{⊥} = B^{⊥}⊗A^{⊥}. The formulae of MLL (resp. NCMLL) are build from the atoms p, q, …, p^{⊥}, q^{⊥}, … and the connectives ⊗, & , (resp. ⊙ and ⊲). There exists a sequent calculus with explicit structural rules for MMLL [1]. To mix commutative and non-commutative connectives in a same sequent calculus, two separators of formulae are used in a sequent: a commutative one

\overline{⊢ A^{⊥}, A} ax  \frac{⊢ Γ, A ⊢ A^{⊥}, Δ}{⊢ Γ, Δ} cut  \frac{⊢ Γ[Δ; Σ]}{Γ[Δ, Σ]} entr

\frac{⊢ Γ, Δ}{⊢ Γ; Δ} seesaw  \frac{⊢ Γ; A  ⊢ B; Δ}{⊢ Γ; A ⊙ B; Δ} ⊙  \frac{⊢ Γ; A; B}{⊢ Γ; A ⊲ B} ⊲

\frac{⊢ Γ, A  ⊢ B, Δ}{⊢ Γ, A ⊗ B, Δ} ⊗  \frac{⊢ Γ, A, B}{⊢ Γ, A & B} &

Fig. 1. A sequent calculus for MMLL

‘,’ and a non-commutative one ‘;’. In this MMLL sequent calculus (see figure 1), some explicit structural rules (seesaw and entropy) define the relationships between these separators. Moreover they are used in conjunction with the rule for the commutativity of ’,’ in order to recover the cyclicity of ’;’. The notation Γ[ ] represents a context with a hole in its decomposition tree and Γ[Δ] is the context Γ[ ] where the hole is filled by Δ. The proof-theoretic and semantic results about MMLL (cut-elimination, sub-formula property, phase semantics, completeness theorem) are given in [1,14]. If we aim to analyze the proof search with this calculus, some problems arise: some orders are fixed by the non-commutative connectives and the commutative and non-commutative connectives interact in the same framework. Let us note that an alternative to study the proof theory of MMLL is to consider the notion of proof net [11].

2.3 A Sequent calculus with implicit structural rules

In [1], P. Ruet introduced a sequent calculus which used a specific mathematical structure, namely order variety, to deal with the interaction between commutative and non-commutative connectors.

2.3.1 Order varieties

We recall here the main definitions and theorems about order varieties [1,14]. Order varieties can be seen as refinements of cyclic orders and are structures which, provided a point of view (an element x in the base set), can be seen as partial orders on the complement of {x}.

Definition 1 (order variety) Let E be a set, an order variety on E is a ternary relation α which is :

- cyclic : ∀x, y, z ∈ E α(x, y, z) ⇒ α(y, z, x)

- anti-reflexive : ∀x, y ∈ E ¬α(x, x, y)

- transitive : ∀x, y, z, t ∈ E α(x, y, z) ∧ α(z, t, x) ⇒ α(y, z, t)

- spreading : ∀x, y, z, t ∈ E α(x, y, z) ⇒ α(t, y, z) ∨ α(x, t, z) ∨ α(x, y, t).

An order variety is said total when : ∀x, y, z ∈ E x ≠ y ≠ z ⇒ α(x, y, z) ∨ α(z, y, x)

Any order variety α on a set E induces an oriented graph →_{α} on E with an edge between x and y ∈ E iff : ∀z ∈ E z ≠ x ∧ z ≠ y ⇒ α(x, y, z). If α is a total order variety, then →_{α} is an oriented cycle. Let α be an order variety on E and x ∈ E, the binary relation α_{x} on E \ {x} is defined by α_{x}(y, z) iff α(x, y, z).

Definition 2 Let (E, ω) be a strict order and z ∈ E, the binary relation <^{z}_{ω} is defined by :

x <^{z}_{ω} y iff x <_{ω} y and z is comparable with neither x nor y.

The ternary relation \overline{ω} on E is defined by:

\overline{ω}(x, y, z) iff \{ \begin{matrix}x <_{ω} y <_{ω} z ∨ z <_{ω} x <_{ω} y ∨ y <_{ω} z <_{ω} x ∨ \\ x <^{z}_{ω} y ∨ y <^{x}_{ω} z ∨ z <^{y}_{ω} x \end{matrix}

Definition 3 Let ω_{1} and ω_{2} be orders on disjoints sets X and Y. We define their parallel (ω_{1} ∥ ω_{2}) and serial (ω_{1} ≪ ω_{2}) composition, that are both orders on X ∪ Y, by :

- (ω_{1} ∥ ω_{2}) (x, y) iff x <_{ω_{1}} y or x <_{ω_{2}} y,

- (ω_{1} ≪ ω_{2}) (x, y) iff x <_{ω_{1}} y or x <_{ω_{2}} y or (x ∈ X and y ∈ Y).

Definition 4 (interior) Let α be an order variety on E, its interior is defined by: ♮α = ⋂_{x∈E} \overline{α_{x} ∥ x}

2.3.2 A sequent calculus with order varieties

Informally, the inference rules are those of the sequent calculus for MLL, seeing ⊲ as a & , and ⊙ as a ⊗. In order to recover the non-commutative behavior of ⊲ and ⊙, sequents are associated with order varieties. Thus, when an inference rule is applied, the order variety corresponding to the conclusion of the rule is obtained from the order varieties associated to the premisse. Moreover, the rule for ⊲ can be applied only if a particular condition about the related order variety is satisfied.

Definition 5 (Sequents) A sequent of MMLL ⊢ Γ ⟨α⟩ is a multiset Γ of occurrences of formulae, together with an order variety α on Γ.

The rules of the sequent calculus are given in figure 2. Let us note that they use operations on order varieties defined as follows: let α and β be two order varieties respectively defined on Γ ∪ {A} and Δ ∪ {B}, α ⊙_{A,B} β is the order variety on Γ∪Δ∪\{A⊙B\} defined by α⊙_{A,B} β = \overline{α_{A} ≪ A ⊙ B ≪ β_{B}}. Moreover α ⊗_{A,B} β is the order variety on Γ ∪ Δ ∪ {A ⊗ B} defined by α ⊗_{A,B} β =

\overline{⊢ A^{⊥}, A ⟨∅⟩} ax  \frac{⊢ Γ, A ⟨α⟩  ⊢ B, Δ⟨β⟩}{⊢ Γ, A ⊙ B, Δ ⟨α ⊙_{A,B} β⟩} ⊙

\frac{⊢ Γ, A, B ⟨α⟩}{⊢ Γ, A ⊲ B ⟨α[A ⊲ B/A, B]⟩} ⊲ if A →_{α} B

\frac{⊢ Γ, A ⟨α⟩  ⊢ B, Δ ⟨β⟩}{⊢ Γ, A ⊗ B, Δ ⟨α ⊗_{A,B} β⟩} ⊗  \frac{⊢ Γ, A, B ⟨α⟩}{⊢ Γ, A & B ⟨α[A & B/A, B]⟩} &

Fig. 2. A sequent calculus with order varieties

\overline{α_{A} ∥ A ⊗ B ∥ β_{B}}. In addition, let α be an order variety on a set E ∪\{x, y\} with x, y ∉ E, and let z ∈ E, we define the pasting α[z/x, y] of x and y along z in α by : α[z/x, y] = ♮ (α↾_{E∪{x}} [z/x] ⋂ α↾_{E∪{y}} [z/y]). It is important to notice that the ⊲ rule can only be applied under the condition A →_{α} B. This point is essential to understand the contributions of the next section.

Let us give a proof of the sequent ⊢ (A ⊙ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥}.

\begin{aligned}& (ax) \\ ⊢ C^{⊥}, C ⟨∅⟩ \end{aligned} \begin{matrix}\begin{aligned}& (ax) \\ ⊢ A^{⊥}, A ⟨∅⟩ \end{aligned} & \begin{aligned}& (ax) \\ ⊢ B^{⊥}, B ⟨∅⟩ \end{aligned} \\ (⊙) \\ ⊢ A^{⊥}, A ⊙ B, B^{⊥} ⟨\overline{A^{⊥} < A ⊙ B < B^{⊥}}⟩ \end{matrix}
(⊙)
⊢ C, C^{⊥} ⊙ B^{⊥}, A^{⊥}, A ⊙ B ⟨\overline{C < C^{⊥} ⊙ B^{⊥} < A^{⊥} < A ⊙ B}⟩
(⊲)
⊢ (A ⊙ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥} ⟨\overline{C^{⊥} ⊙ B^{⊥} < A^{⊥} < (A ⊙ B) ⊲ C}⟩

This derivation is a proof of the sequent because the condition to apply the ⊲ rule is satisfied. We observe that this verification cannot be trivially included in the process of proof search within this calculus. That is one of the main interest of a new calculus with dependencies in which such a condition is more naturally expressed inside the calculus itself.

2.4 Proof search in MMLL

The calculus with explicit structural rules is clearly not appropriate for automated proof search because of the difficult management of the structural rules during the proof search process. In the opposite, the calculus with implicit structural rules has no more two formulae separators to deal with, and the underlying sequent calculus is in fact the MLL sequent calculus, for which we have results on proof normalization [9] and proof-search [6]. But the order varieties, associated to sequents, are mathematical structures which are difficult to deal with during proof-search.

We have recently study proof-search in MMLL from both commutative and non-commutative linear logics and thus have defined two different proof-search algorithms, both based on the construction of labelled proof nets [8]. The labels allow in the former to fix some constraints to satisfy during the proof net search and in the latter to propagate some informations useful to guide and control the search. Moreover, such based-on proof nets methods are useful in order to efficiently detect the non-provability.

Our aim is thus to propose a new formulation of MMLL based on dependencyrelations with a new sequent calculus but also a new proof net definition that is another view to present the interactions between commutative and noncommutative connectives in the same logic. Moreover, the based-on proof nets calculus we propose is more appropriate to deal with proof-search in MMLL following our based-on proof nets approach of proof construction in commutative and non-commutative MLL [6,7]. Comparisons with our previous proposals [8] will be studied.

Our aim here is proof construction but we will see that our algorithm, based on proof net construction, can also be adapted and used for proof verification. Our new proof net definition provides a new correctness criterion for MMLL and thus our algorithm provides a new way to verify correctness. It will be compared to the recent quadratic correctness criterion proposed in [13].

3 A sequent calculus with dependency relations

We now introduce a new sequent calculus, which aims to be more adapted for proof search and proof construction in MMLL. This calculus use the notion of dependency in order to express some order between formulae.

Definition 6 A dependency relation between two formulae A and B is represented by A → B. A sequent with dependencies ⊢ Γ D is a multiset Γ of formulae, associated with a set of dependencies D.

Let γ be a subset of Γ. Then, D ↾_{γ} denotes the restriction of D to the subset γ of formulae. Thus we have D ↾_{γ}= {E → F |E, F ∈ γ, E → F ∈ D}. Moreover D[Y/X] represents the set D where the formula (occurrences) X is replaced by Y.

A set of dependencies D is a graph the nodes of which are the formulae of Γ and with edges representing dependency relations between formulae. By construction, a set of dependencies is cyclic.

Definition 7 A cycle is said maximal in D if it exactly contains once all the formulae of Γ.

By construction, there always exists a maximal cycle in a set D. Let ⊢ Γ D be a sequent with dependencies, the set of maximal cycles in D is denoted D_{C}.

3.1 A new sequent calculus

We give a sequent calculus with dependencies in figure 3. In fact, we observe that the sequent rules are structurally the same for ⊗ and ⊙ and also for & and ⊲ and that the semantical differences are in fact in the construction of the dependency relations. Let us note that the rules \frac{⊢A D_{1} ⊢B,Δ D_{2}}{⊢A⊙B,Δ D} ⊙ and \frac{⊢Γ,A D_{1} ⊢B D_{2}}{⊢Γ,A⊙B D} ⊙ are special cases of the sequent rule \frac{⊢Γ,A D_{1} ⊢B,Δ D_{2}}{⊢Γ,A⊙B,Δ D} ⊙. The distinction between these cases allows to simplify the calculus of the dependencies. A similar remark can be made for the ⊗-rule. Moreover, looking at the rule for ⊗, we can see that the dependencies are extended as for A ⊙ B, and also as for B ⊙ A. This difference in the construction of the dependencies from those associated to the premisse allows, in some way, to express the commutativity of ⊗. Actually, the difference is made essentially on the maximal cycles, especially when checking the condition on the application of the ⊲-rule.

Before to present the properties of this calculus, we give an example of derivation with the sequent ⊢ (A ⊗ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥}. A proof is the classical sequent tree where a set of dependencies is associated to each sequent. The important point is that a rule application modifies the set of dependencies D_{i} and that when one applies a ⊲ rule we have to verify the condition about the membership to the maximal cycles.

\begin{aligned}& (Ax) \\ ⊢ C^{⊥}, C D_{3} \end{aligned} \begin{matrix}\begin{aligned}& (Ax) \\ ⊢ A^{⊥}, A D_{1} \end{aligned} & \begin{aligned}& (Ax) \\ ⊢ B^{⊥}, B D_{2} \end{aligned} \\ (⊗) \\ ⊢ A^{⊥}, A ⊗ B, B^{⊥} D_{4} \end{matrix}

where D_{1} = \{ \begin{matrix}A & → & A^{⊥} \\ A^{⊥} & → & A \end{matrix} \}, D_{2} = \{ \begin{matrix}B & → & B^{⊥} \\ B^{⊥} & → & B \end{matrix} \}, D_{3} = \{ \begin{matrix}C & → & C^{⊥} \\ C^{⊥} & → & C \end{matrix} \}.

We have D_{4} = \{ \begin{matrix}B^{⊥} & → & A ⊗ B & B^{⊥} & → & A^{⊥} \\ A ⊗ B & → & A^{⊥} & A^{⊥} & → & A ⊗ B \\ A^{⊥} & → & B^{⊥} & A ⊗ B & → & B^{⊥} \end{matrix} \},

and finally D_{5} = \{ \begin{matrix}C & → & A ⊗ B & C & → & A^{⊥} \\ A ⊗ B & → & A^{⊥} & A^{⊥} & → & A ⊗ B \\ A^{⊥} & → & C^{⊥} ⊙ B^{⊥} & A ⊗ B & → & C^{⊥} ⊙ B^{⊥} \\ C^{⊥} ⊙ B^{⊥} & → & C \end{matrix} \}.

(⊙)

⊢ C, C^{⊥} ⊙ B^{⊥}, A^{⊥}, A ⊗ B D_{5}

(⊲)

⊢ (A ⊗ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥} D_{6}

\overline{⊢A^{⊥},A D}Ax  with D = \{ \begin{matrix}A & → & A^{⊥} \\ A^{⊥} & → & A \end{matrix} \}

\frac{⊢Γ,A D_{1}  ⊢B,Δ D_{2}}{⊢Γ,A⊙B,Δ D} ⊙ with \begin{aligned}D & = & D_{1} ↾_{Γ} ∪D_{2} ↾_{Δ} ∪ \\ & & \{E → F |E ∈ Γ, F ∈ Δ, E → A ∈ D_{1}, \\ & & B → F ∈ D_{2}\} ∪ \\ & & \{A ⊙ B → E|E ∈ Γ, A → E ∈ D_{1}\} ∪ \\ & & \{F → A ⊙ B|F ∈ Δ, F → B ∈ D_{2}\} \end{aligned}

\frac{⊢A D_{1}  ⊢B,Δ D_{2}}{⊢A⊙B,Δ D} ⊙ with D = D_{2}[A ⊙ B/B]
\frac{⊢Γ,A D_{1}  ⊢B D_{2}}{⊢Γ,A⊙B D} ⊙ with D = D_{1}[A ⊙ B/A]

\frac{⊢Γ,A,B D_{1}}{⊢Γ,A⊲B D}⊲

iff B → A is in all the maximal cycles in D_{1}

with D = D_{1}[A ⊲ B/A, A ⊲ B/B]

\frac{⊢Γ,A D_{1}  ⊢B,Δ D_{2}}{⊢Γ,A⊗B,Δ D} ⊗ with D = D_{1} ↾_{Γ} ∪D_{2} ↾_{Δ} ∪ \{E → F |E ∈ Γ, F ∈ Δ, E → A ∈ D_{1}, B → F ∈ D_{2}\} ∪ \{A ⊗ B → E|E ∈ Γ, A → E ∈ D_{1}\} ∪ \{F → A ⊗ B|F ∈ Δ, F → B ∈ D_{2}\} ∪ \{F → E|E ∈ Γ, F ∈ Δ, A → E ∈ D_{1}, F → B ∈ D_{2}\} ∪ \{A ⊗ B → F |F ∈ Δ, B → F ∈ D_{2}\} ∪ \{E → A ⊗ B|E ∈ Γ, E → A ∈ D_{1}\}

\frac{⊢A D_{1}  ⊢B,Δ D_{2}}{⊢A⊗B,Δ D} ⊗ with D = D_{2}[A ⊗ B/B]
\frac{⊢Γ,A D_{1}  ⊢B D_{2}}{⊢Γ,A⊗B D} ⊗ with D = D_{1}[A ⊗ B/A]

\frac{⊢Γ,A,B D_{1}}{⊢Γ,A & B D} &  with \begin{aligned}D & = & D_{1}[A & B/A, A & B/B]∪ \\ & & \{E → F |E, F ∈ Γ, E → A, A → F ∈ D_{1}\} ∪ \\ & & \{E → F |E, F ∈ Γ, E → B, B → F ∈ D_{1}\} \end{aligned}

Fig. 3. A sequent calculus with dependencies

There are two maximal cycles in D_{5}, namely C → A⊗B → A^{⊥} → C^{⊥}⊙B^{⊥} → C and C → A^{⊥} → A ⊗ B → C^{⊥} ⊙ B^{⊥} → C. Then we can deduce that C → A ⊗ B does not belong to the maximal cycles of D_{5}. Then, we cannot apply any rule to obtain (A ⊗ B) ⊲ C and therefore the given sequent is not provable.

If we replace (A ⊗ B) by (A ⊙ B) we have a similar proof tree but with another set D_{5}. In this case, the only maximal cycle in D_{5} is C → A ⊙ B → A^{⊥} → C^{⊥} ⊙ B^{⊥} → C and therefore C → A ⊙ B is in all the maximal cycles in D_{5}. Thus, the given sequent ⊢ (A ⊙ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥} is provable.

The main point for the proof construction within this calculi is the construction of the set of dependencies associated to the sequents and the verification for the ⊲ rules of the condition for a special dependency to belong to all maximal cycles of the related dependencies set. In the next section, we propose a new calculus based on proof nets with dependencies and an algorithm for the construction of such proof nets in order to analyze the provability in MMLL. Before we prove the equivalence between this new calculus and the initial calculus with order varieties.

3.2 Properties of the calculus

Theorem 8 Let Π be a proof in the sequent calculus with dependencies, with conclusion ⊢ Γ D. Then, there exists a maximal cycle in D.

PROOF. By induction on the structure of Π. □

Theorem 9 The sequent calculus with dependencies is equivalent to the sequent calculus with order varieties.

PROOF. The main point is that when deleting the structure associated to sequents (order varieties or dependencies), the calculus is the one for MLL, considering the connectives ⊙ and ⊲ as respectively ⊗ and & . Let us consider the ⊲-rule in both sequent calculus :

\frac{⊢ Γ, A, B ⟨α⟩}{⊢ Γ, A ⊲ B ⟨α[A ⊲ B/A, B]⟩} ⊲ \frac{⊢ Γ, A, B D_{1}}{⊢ Γ, A ⊲ B D}⊲

Thus, to prove the equivalence of both calculus, we only need to prove the equivalence of the conditions of the ⊲-rule, that is to say :

A →_{α} B iff B → A is in all the maximal cycles of D_{1}

This can be shown directly by induction, using the results on order varieties. The proof is not detailed here, but it will follow from the results on the use of dependencies for proof nets construction. □

4 Proof nets of MMLL

In this section we remind the main results about proof nets in MMLL, mainly the relations between proof nets and proofs in the sequent calculus with order varieties [1]. Then we introduce a new definition of proof nets with dependencies and analyze its connections with the sequent calculus. First we remind a definition of the proof nets in MMLL that is based on the notion of trip in a proof structure.

Definition 10 The links of MMLL are the following graphs, the vertices of which are labelled with MMLL formulae:

\begin{matrix}A^{⊥} & A \\ axiom \end{matrix}  \begin{aligned}A^{⊥} & & A \\ & cut \end{aligned}  \begin{aligned}A & B & A ⊗ B \\ & times \end{aligned}  \begin{aligned}A & B & A & B \\ & par \end{aligned}  \begin{aligned}A & B & A ⊙ B \\ & next \end{aligned}  \begin{matrix}A & B & A ⊲ B \\ sequential \end{matrix}

Axiom-links have two conclusions and no premisse. Cut links have two premisses and no conclusion. In the other cases, A and B are respectively the first and second premisse and the third formula is the conclusion.

Definition 11 A proof structure (of MMLL) is a graph built from links of MMLL such that every occurrence of formula is either the conclusion of exactly one link or the premisse of at most one link. An occurrence that is not a premisse of a link is called terminal and it is a conclusion of the structure.

A proof structure of MLL (resp. NCMLL) is a proof structure labelled with only MLL (resp. NCMLL) formulae.

Definition 12 For any link l of a proof structure π, one defines a set S(l) of partial functions, called switching positions, given in figure 4. Any function s such that, for any l of π, s(l) ∈ S(l), is called a switching of π. A switching for π is ⊲_{3}-free if for every ⊲-link, s(l) ≠ ⊲_{3}.

[figure: A^{⊥}; A; axiom; A^{⊥}; A; cut; A; B; A ⊗ B; times; A; B; A ⊗ B; times; A; B; A ^{&} B; par]

[figure: A; B; A ^{&} B; par; A; B; A ⊲_{R} B; sequential; A; B; A ⊲_{L} B; sequential; A; B; A ⊲_{3} B; sequential; A; B; A ⊙ B; next]

Fig. 4. Switching positions for MMLL

Definition 13 Let π be a proof structure and s be a switching for π, then s(π) is the oriented graph with nodes being the decorated formulae of π and an oriented edge from A^{x} to B^{y} if and only if either there exists a link l such that B^{y} = s(l)(A^{x}), or we have A^{x} = C^{↓} and B^{y} = C^{↑} and C is a conclusion of π. A trip is defined as a cycle or a maximal path in s(π).

Definition 14 Let π be a proof structure and s(π) a switching for π, a trip v in s(π) is said long if v is a cycle and any occurrence formula A appears twice: one time decorated with ↓, another time with ↑. A cycle v in s(π) is said bilateral if v has not the form A^{x}, .., B^{y}, .., A\overline{x}, .., B\overline{y}, .., A^{x} where A and B are formulae occurrences of π.

Theorem 15 Let π be a proof structure of MMLL, then π is a proof net if and only if for any switching s of π : a) there exists exactly one cycle σ in s(π), b) σ contains all the conclusions, c) σ is bilateral.

Theorem 16 ([1]) Let π be a MMLL proof structure, π is a MMLL proof net if and only if its commutative translation π^{∗} (obtained by replacing in π ⊙ by ⊗ and ⊲ by & ) is a proof net of MLL such that for every ⊲_{3}-free switching s for π, the inner parts of ⊲-links in s(π) contain no conclusion and do not overlap.

This last result gives a characterization of a MMLL proof net π from its commutative translation π^{∗} in MLL. The interest is that we can benefit of results about the construction of proof nets in MLL including some refinements or specializations.

4.1 Proof nets and order varieties

Definition 17 If π is a proof net of MMLL and s is a switching for π, then the oriented graph with vertices the conclusions of π and an oriented edge from a conclusion A to a conclusion B iff there is no conclusion between B^{↑} and A^{↓} in the unique cycle σ in s(π), is an oriented cycle called the cycle of the conclusions in s(π)

Definition 18 Let π be a proof net of MMLL with conclusion Γ,

a) If s is a switching for π, α_{π,s} is the total order variety on Γ corresponding to the cycle of the conclusions in s(π).

b) α_{π} = ♮(⋂_{s} α_{π,s}).

Definition 19 To a proof D of conclusion ⊢ Γ ⟨α⟩ in sequent calculus, is associated in the obvious way a proof structure \overline{D} with conclusion Γ.

Theorem 20 (Adequacy) If D is a sequential proof with conclusion ⊢ Γ ⟨α⟩, then \overline{D} is a proof net and α = α\overline{D}.

Theorem 21 (Sequentialization) Let π be a proof net with conclusion Γ. There exists a sequent calculus proof D, with conclusion ⊢ Γ ⟨α⟩ such that π = \overline{D}.

Theorem 22 A →_{α_{π}} B iff for every switching s there is no conclusion between B^{↑} and A^{↓} in the unique cycle σ in s(π).

PROOF. Let π be a MMLL proof net with conclusions Γ, there exists a sequential proof with conclusion ⊢ Γ ⟨α_{π}⟩, where α_{π} is : α_{π} = ♮ (⋂_{s} α_{π,s}), where α_{π,s} is the order variety corresponding to the cycle of conclusions in the unique cycle σ in s(π). □

4.2 A new definition of MMLL proof nets

In this definition, we attach to each proof net Π a set of pairs of conclusions, called a set of dependencies Dep(Π). This set is inductively built in parallel with the proof net structures (cf. construction rules). In the rest of the paper |Dep(Π)|_{A} (resp. |Dep(Π)|_{A,B} ) represents the set of dependencies built from π with cancellation of the dependencies including A (resp. A or B). Moreover Conc(Π), with Π being a proof net, is the set of conclusions of Π.

Definition 23 The MMLL proof nets with dependencies are inductively defined in the following way:

- if Π is an axiom-link _{A A^{⊥}} then the set Dep(Π) is built as follows:

Dep(Π) = \{ \begin{matrix}A → A^{⊥} \\ A^{⊥} → A \end{matrix} \}

- if Π is ^{Π_{1}}  ^{Π_{2}}^{A}  ^{B}^{A ⊙ B}^{⊙}  the set Dep(Π) is built from Dep(Π_{1}) and Dep(Π_{2})

as follows:

Dep(Π) = |Dep(Π_{1})|_{A} ∪ |Dep(Π_{2})|_{B} ∪
{E → F |E ∈ Conc(Π_{1}) \ A, F ∈ Conc(Π_{2}) \ B, E → A ∈ Dep(Π_{1}),
B → F ∈ Dep(Π_{2})} ∪
{A ⊙ B → E|E ∈ Conc(Π_{1}) \ A, A → E ∈ Dep(Π_{1})} ∪
{F → A ⊙ B|F ∈ Conc(Π_{2}) \ B, F → B ∈ Dep(Π_{2})} ∪
{E → A ⊙ B|E ∈ Conc(Π_{1}) \ A, E → A ∈ Dep(Π_{1}), |Conc(Π_{2})| = 1} ∪
{A ⊙ B → F |F ∈ Conc(Π_{2}) \ B, B → F ∈ Dep(Π_{2}), |Conc(Π_{1})| = 1}

- if Π is ^{Π_{1}}  ^{Π_{2}}^{A}  ^{B}^{A ⊗ B}^{⊗}  the set Dep(Π) is built from Dep(Π_{1}) and Dep(Π_{2})

as follows:

Dep(Π) = |Dep(Π_{1})|_{A} ∪ |Dep(Π_{2})|_{B} ∪
{E → F |E ∈ Conc(Π_{1}) \ A, F ∈ Conc(Π_{2}) \ B, E → A ∈ Dep(Π_{1}),
B → F ∈ Dep(Π_{2})} ∪
{A ⊗ B → E|E ∈ Conc(Π_{1}) \ A, A → E ∈ Dep(Π_{1})} ∪
{F → A ⊗ B|F ∈ Conc(Π_{2}) \ B, F → B ∈ Dep(Π_{2})} ∪
{F → E|E ∈ Conc(Π_{1}) \ A, F ∈ Conc(Π_{2}) \ B, A → E ∈ Dep(Π_{1}),
F → B ∈ Dep(Π_{2})} ∪
{A ⊗ B → F |F ∈ Conc(Π_{2}) \ B, B → F ∈ Dep(Π_{2})} ∪
{E → A ⊗ B|E ∈ Conc(Π_{1}) \ A, E → A ∈ Dep(Π_{1})}

- if Π is  ^{Π_{1}}^{&}^{A}  ^{B}^{A & B} the set Dep(Π) is built from Dep(Π_{1}) as follows:

Dep(Π) = Dep(Π_{1})[A & B/A, A & B/B]
{E → F |E, F ∈ Conc(Π_{1}) \ {A, B}, E → A, A → F ∈ Dep(Π_{1})} ∪
{E → F |E, F ∈ Conc(Π_{1}) \ {A, B}, E → B, B → F ∈ Dep(Π_{1})}

- if Π is:  ^{Π_{1}}^{⊲}^{A}  ^{B}^{A ⊲ B} the set Dep(Π) is built from Dep(Π_{1}) as follows:

if B → A is in all the maximal cycles in Dep(Π_{1}), then we have

Dep(Π) = Dep(Π_{1})[A ⊲ B/A, A ⊲ B/B]

In fact, the construction of the dependencies in this inductive definition is similar to the one for the sequent calculus given in figure 3. The only syntactical differences come from the differences between sequents and proof nets in terms of notations. As in the sequent calculus, when one forgets the dependencies sets, the given inductive definition is exactly the one for the proof nets of MLL seeing ⊙ and ⊲ as, respectively, ⊗ and & .

Let us comment this definition. The construction of Dep(Π) is more complex for ⊗ than for ⊙ because we extend the dependencies like for A ⊙ B but also for B ⊙ A. In the case of & , we are obliged to apply the transitivity of the dependencies because the substitution of A and B by A & B make lost the relationships between A and B. In the case of ⊲, the dependencies are the same than for & , except that, because of the condition, we know that B → A ∈ Dep(Π_{1}) and thus the application of transitivity is not necessary.

Theorem 24 A proof structure π can be constructed using this inductive definition iff π is a proof net of MMLL.

PROOF. From theorem 16, a proof structure π is a proof net iff : i) π^{∗} is a proof net of MLL, ii) for every ⊲_{3}-free switching s for π, the inner parts of ⊲-links in s(π) contain no conclusion and do not overlap. First, if we ignore the dependencies set, the given inductive definition is exactly the one for the proof nets of MLL seeing ⊙ and ⊲ as, respectively, ⊗ and & . Thus, every structure π built using the inductive definition is such that π^{∗} is a proof net of MLL. Conversely, if π is a proof structure such that π^{∗} is a proof net of MLL, then π can be constructed iff the condition on the application of the ⊲-rule is verified for each ⊲-link in π.

Let π be a proof structure built using our inductive definition, and D be the set of dependencies associated to π. In theorem 26, we prove that the maximal cycles of D correspond exactly to the cycles of conclusions in π. Thus, the condition on the application of the ⊲-rule in the inductive definition insures for every ⊲-link A ⊲ B and every switching s in π, there is no conclusion between B^{↑} and A^{↓} in the unique cycle in s(π). By induction, we can prove the inner parts of ⊲-link do not overlap. For a detailed proof of this point we can refer to [8]. Finally, we prove that a proof structure built using our inductive definition is a proof net of MMLL. Moreover, a proof net of MMLL can be built using our inductive definition. This is a direct consequence of theorem 16, since the maximal cycles exactly correspond to the cycles of conclusions. Indeed, the condition on the inner parts of ⊲-links ensures that the condition on the application of the ⊲-rule is verified. □

4.2.1 An example

Here is a proof structure for the sequent ⊢ (A ⊗ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥}.

A  B ⊗  C ⊲ (A ⊗ B) ⊲ C  A^{⊥}  ⊙ C^{⊥}  B^{⊥} C^{⊥} ⊙ B^{⊥}

Dep(A ⊗ B, C, A^{⊥}, C^{⊥} ⊙ B^{⊥}) = \{ \begin{matrix}C & → & A ⊗ B & C & → & A^{⊥} \\ A ⊗ B & → & A^{⊥} & A^{⊥} & → & A ⊗ B \\ A^{⊥} & → & C^{⊥} ⊙ B^{⊥} & A ⊗ B & → & C^{⊥} ⊙ B^{⊥} \\ C^{⊥} ⊙ B^{⊥} & → & C \end{matrix} \}

There are two maximal cycles in Dep(A ⊗ B, C, A^{⊥}, C^{⊥} ⊙ B^{⊥}), namely C^{⊥} ⊙

B^{⊥} → C → A ⊗ B → A^{⊥} → C^{⊥} ⊙ B^{⊥} and C^{⊥} ⊙ B^{⊥} → C → A^{⊥} → A ⊗ B →

C^{⊥} ⊙ B^{⊥}. In fact, C → A ⊗ B belongs to the first cycle, but not to the second cycle. Thus, the ⊲ rule is not applicable. As the choice for the axiom links to build is unique, we cannot perform any backtracking, and then cannot build a proof net for the given sequent. Thus, we can deduce that the given sequent is not provable.

4.3 Properties of proof nets

Definition 25 Let C be an oriented cycle, we define \overline{C} as the inverse of C, i.e., for every couple of vertices (A, B), A → B ∈ C iff B → A ∈ \overline{C}.

Theorem 26 Let π be a proof net. C is a maximal cycle in Dep(π) iff \overline{C} is a cycle of conclusions in π.

PROOF. The main point is to notice that the construction of a dependencies set is made in respect with the switching positions of the various links. Thus, when focusing on maximal cycles, we actually build the cycles of conclusions of the proof net. We proceed by induction on the structure of proof nets. □

From a proof net of MMLL, we can easily build a proof in the sequent calculus with dependencies, and conversely, we can also build a proof net from a proof in the sequent calculus with dependencies.

Theorem 27 (Adequacy) If D is a sequential proof with conclusion ⊢ Γ D, then \overline{D} is a proof net and Dep (\overline{D}) = D.

PROOF. Proof similar to the one of MLL, by tacking dependency relations into account. □

Theorem 28 (Sequentialization) Let π be a proof net with conclusion Γ. There exists a sequent calculus proof D, with conclusion ⊢ Γ Dep(π) such that π = \overline{D}.

PROOF. Proof similar to the one of MLL, by tacking dependency relations into account. □

5 Proof search and dependencies in MMLL

We have seen that both sequent calculus (with order varieties and with dependencies) relies on MLL. However, we have a procedure for automatic proof nets construction in MLL [7] that we can adapt to design a procedure for proof net construction in MMLL.

5.1 Principles of construction

This procedure is based on principles that are similar to the ones of our algorithm for MLL proof nets construction. From the inductive definition of proof nets, we notice that from two disjoint proof nets, we can build a new proof net by fusion and extension with a ⊗- link or a ⊙-link and that from a given proof net we can build a new proof net by extension with a & -link or a ⊲-link. At this step, commutative and non-commutative connectives have the same behaviour during this construction but their semantical differences are reflected in the set of dependencies attached to proof structures.

In fact, it means that we apply the algorithm for MLL on the commutative translation of the formula to prove and in addition we build set of dependencies that are used to test the condition about the validity of the application of the ⊲ rule. Therefore, our algorithm considers the decomposition tree of the given sequent, that will be used as a frame to guide the proof net search. In addition, it manages a set R of intermediate proof nets that is initialized to the empty set. Then, starting from the literals (or leaves) of the decomposition tree, it builds step by step axiom-links, that are elementary proof nets added to R. When conclusions of proof nets of R are premises of a ⊗ or ⊙-link, they are linked and extended with this link to obtain a new proof net that replaces the two initial ones in R. When conclusions of a given proof net of R are in fact premises of a &or ⊲-link, then it is extended with this link to obtain a new proof net that replaces the initial one in R. If two premises of a &or ⊲-link (in the decomposition tree) are conclusions of two different nets in R then we postpone the extension of such a link. With respect to the permutability results in linear sequent calculus [9], we have to always apply, if possible, a ⊗ or ⊙ (extension) rule before a &or ⊲ (extension) rule.

The algorithm is proved complete and correct using the arguments of the MLL case and the new proof net definition. A detailed description of the algorithm and its proofs of correction and completeness will be given in the full version.

5.2 An example

We illustrate the algorithm with the sequent ⊢ (A ⊗ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥}. We first start by building the decomposition for the sequent to prove.

A  B ⊗  C ⊲ (A ⊗ B) ⊲ C  A^{⊥}  ⊙ C^{⊥}  B^{⊥} C^{⊥} ⊙ B^{⊥}

We then build the two elementary proof nets corresponding to the axioms ⊢ A^{⊥}, A and ⊢ B^{⊥}, B.

A  B ⊗  C ⊲ (A ⊗ B) ⊲ C  A^{⊥}  ⊙ C^{⊥}  B^{⊥} C^{⊥} ⊙ B^{⊥}

Dep(A − A^{⊥}) = \{ \begin{matrix}A → A^{⊥} \\ A^{⊥} → A \end{matrix} \} and Dep(B − B^{⊥}) = \{ \begin{matrix}B → B^{⊥} \\ B^{⊥} → B \end{matrix} \}

We can now apply the rule for the ⊗-link.

A  B ⊗  C ⊲ (A ⊗ B) ⊲ C  A^{⊥}  ⊙ C^{⊥}  B^{⊥} C^{⊥} ⊙ B^{⊥}

Dep(A^{⊥}, A ⊗ B, B^{⊥}) = \{ \begin{matrix}B^{⊥} & → & A ⊗ B & B^{⊥} & → & A^{⊥} \\ A ⊗ B & → & A^{⊥} & A^{⊥} & → & A ⊗ B \\ A^{⊥} & → & B^{⊥} & A ⊗ B & → & B^{⊥} \end{matrix} \}

We now choose the literal C^{⊥}, and try to branch it to the free literal C. We obtain a new elementary proof net corresponding to the axiom ⊢ C^{⊥}, C.

A  B ⊗  C ⊲ (A ⊗ B) ⊲ C  A^{⊥}  ⊙ C^{⊥}  B^{⊥} C^{⊥} ⊙ B^{⊥}

Dep(C, C^{⊥}) = \{ \begin{matrix}C^{⊥} & → & C \\ C & → & C^{⊥} \end{matrix} \}

We apply the rule for the ⊙-link, and thus obtain a new partial proof net.

A  B ⊗  C ⊲ (A ⊗ B) ⊲ C  A^{⊥}  ⊙ C^{⊥}  B^{⊥} C^{⊥} ⊙ B^{⊥}

Dep(A ⊗ B, C, A^{⊥}, C^{⊥} ⊙ B^{⊥}) = \{ \begin{matrix}C & → & A ⊗ B & C & → & A^{⊥} \\ A ⊗ B & → & A^{⊥} & A^{⊥} & → & A ⊗ B \\ A^{⊥} & → & C^{⊥} ⊙ B^{⊥} & A ⊗ B & → & C^{⊥} ⊙ B^{⊥} \\ C^{⊥} ⊙ B^{⊥} & → & C \end{matrix} \}

There are two maximal cycles in Dep(A ⊗ B, C, A^{⊥}, C^{⊥} ⊙ B^{⊥}) that are C^{⊥} ⊙

B^{⊥} → C → A ⊗ B → A^{⊥} → C^{⊥} ⊙ B^{⊥} and C^{⊥} ⊙ B^{⊥} → C → A^{⊥} → A ⊗ B →

C^{⊥} ⊙ B^{⊥}. In fact, C → A ⊗ B belongs to the first one, but not to the second one. Thus, the ⊲ rule is not applicable. As the choice for the axiom links to build is unique, we cannot perform any backtracking, and then cannot build a proof net for the given sequent. Thus, we can deduce that the given sequent is not provable.

6 Dependencies with constraints

In order to design efficient procedures for proof (net) construction, we aim to optimize the construction of maximal cycles. In the sequent calculus with dependencies, we have to consider a special condition on the application of the ⊲- rule, namely \frac{⊢Γ,A,B D_{1}}{⊢Γ,A⊲B D}⊲, in order to take into account the non-commutativity of ⊙ and ⊲. This condition is B → A is in all the maximal cycles in D_{1}. Thus, one needs to extract the maximal cycles in the graph of dependencies D_{1}, this step being a source of potential complexity in the proof search. For that, we extend our calculus on dependencies in order to directly check this condition about the ⊲-rule application, from the dependencies set.

A solution consists in adding guards on dependencies in order to avoid the construction of maximal cycles. These guards are in fact boolean formulae associated to dependencies. A valuation for the boolean variables will correspond to a maximal cycle : given a valuation v, we only keep the dependencies A ⟶^{x} B such that the formulae x equals to 1 for the valuation v. Thus, to check if a dependency is in all the maximal cycle, we only need to check the validity of the boolean formula associated to it. Finally, if we consider the ⊲-rule of the sequent calculus \frac{⊢Γ,A,B D_{1}}{⊢Γ,A⊲B D}⊲, the condition of its application can be reformulated by : from D_{1}, we can deduce B ⟶^{1} A (denoted D_{1} ⊢ B ⟶^{1} A). The boolean value, associated to a dependency relation, is then computed during the construction of the dependencies set.

This new sequent calculus will be defined in the full version of this paper, and its proof of equivalence with the initial sequent calculus with dependencies will be given. We will also illustrate how constraints can be used and solved in order to determinate the validity of the new condition of the ⊲ rule. Moreover we will propose a version of the proof nets calculus with such constraints and present their main results (equivalence with the previous system, ability to deal with efficient proof-search).

7 Conclusion

In this paper, we propose new calculi for the multiplicative fragment of Mixed Linear Logic (MMLL), that are are based on the definition of dependencyrelations. They provide a new proof-theoretical formulation of MMLL in the spirit of [5] and moreover the use of dependencies (or constraints) is a natural way to translate some proof-theoretical results of MMLL into simple and tractable automated proof-search procedures, that are based on the construction of semantical structures like proof nets [6,11]. Then, we provide an algorithm for proof net construction in MMLL that builds in parallel a proof structure and a set of dependencies on which we have to verify some validity conditions. Moreover, we propose refinements of both calculi that include dependencies with constraints in order to simplify their implementations. In further works, we will compare our algorithm with the previous ones we have recently developed [8]. In addition, we will show how to adapt our approach, that is based on proof nets, for proof (net) verification. Our new MMLL proof net definition provides a new correctness criterion for MMLL and we will discuss its complexity and compare it with the recent quadratic correctness criterion proposed for MMLL in [13].

References

[1] M. Abrusci and P. Ruet. Non-commutative logic I : the multiplicative fragment. Annals of Pure and Applied Logic, 101:29–64, 2000.

[2] V.M. Abrusci. Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. Journal of Symbolic Logic, 56(4):1403–1451, 1991.

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

[4] G. Bellin and P.J. Scott. On the π-calculus and linear logic. Theoretical Computer Science, 135(1):11–66, 1994.

[5] T. Bräuner and V. De Paiva. A formulation of linear logic based on dependencyrelations. In Computer Science Logic, CSL’97, LNCS 1414, pages 129–148. Springer Verlag, 1997.

[6] D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1-2):231–272, 2000.

[7] 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.

[8] D. Galmiche and J.M. Notin. Proof-search and proof nets in mixed linear logic. Electronic Notes in Theoretical Computer Science, 37, 2000.

[9] D. Galmiche and G. Perrier. On proof normalization in linear logic. Theoretical Computer Science, 135(1):67–110, 1994.

[10] 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.

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

[12] N. Kobayashi and A. Yonezawa. Asynchronous communication model based on linear logic. Formal Aspects of Computing, 3:279–294, 1994.

[13] V. Mogbil. Quadratic correctness criterion for non commutative logic. In Computer Science Logic, CSL’01, LNCS, Paris, France, September 2001.

[14] P. Ruet. Non-commutative logic II : sequent calculus and phase semantics. Math. Struct. in Comp. Science, 10:277–312, 2000.

[15] P. Ruet and F. Fages. Concurrent constraint programming and noncommutative logic. In 11th Int. Workshop on Computer Science Logic, CSL’97, LNCS 1414, pages 406–423, Aarhus, Denmark, August 1997.