Connection-based proof construction in Non-Commutative Logic

D. Galmiche and J.-M. Notin

LORIA - Université Henri Poincaré 54506 Vandœuvre-lès-Nancy Cedex, France

                         galmiche{notin}@loria.fr

Abstract. We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.

1 Introduction

Since last years there is an increasing amount of interest for logical systems that are resource sensitive (linear logic [10] with its resource consumption interpretation and bunched implications logic [16] with its resource sharing interpretation) but also order-aware (non-commutative logic [1]). As specification logics, they can represent features as interaction, resource distribution and mobility, nondeterminism, sequentiality or coordination of entities. Here, we focus on this order-awareness in the Non-Commutative Logic (NL) [1, 17] that incorporates, in a conservative way, the notion of order into Linear Logic. This logic is motivated by a fine logical characterization of operational aspects of concurrent constraint programming (CC) [18]. It allows to analyze how to manage coordination in the access to resources and information [3]. Its intuitionistic fragment also allows to specify and verify the TCP/IP protocol [12] for which one needs a linear implication that consumes its premise in a particular order, together with a commutative conjunction. In this paper we focus on proof construction in the multiplicative fragment of Non-Commutative Logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. Non-Commutative Logic is mainly characterized by two equivalent sequent calculi that are enriched with a structure of order, the first with an order variety [1] and the second with bunches of formulae including a commutative and a noncommutative separators [17]. Proof search is difficult in such settings in particular because of the management of context splitting. Recent works on MNL proof search are based on particular treatments of order varieties and the introduction of the focusing principle. We can mention a cluster calculus with a simple way to propagate the order structure [4] and a bipolar sequent calculus that allows to deal with partial information, through specific constraints, during proof construction [2]. The later approach has been also adapted to the proof net construction [3]. Independently, we have studied proof construction in MNL through the construction of labelled proof nets [7], the labels allowing to fix constraints and/or to propagate information necessary to guide and control the construction process. But the labels were not clearly related to the MNL semantics and cannot help for instance for countermodel generation. We recently proposed new sequent and proof net calculi with dependency relations (on formulae) and in this setting the provability of a MNL formula A is studied through the provability of the corresponding MLL formula (A without distinction between commutative and non-commutative connectives) and the verification of some conditions on a set of dependency relations generated during the proof search process [8]. All these works come from, or are influenced by, the definition of NL with order varieties. An alternative way consists in studying proof search from the MNL sequent calculus with bunches [17] and its phase semantics. Because of the presence of two context separators and two structural rules, this calculus is not well adapted to the design of an automatic theorem prover of MNL. Therefore, we propose a connection-based characterization of provability in MNL, starting from our previous works on connection methods for MLL and proof nets construction [5]. It is based on the introduction of polarities on formulae, of labels and label constraints in order to deal with bunched contexts and thus to capture the specific interactions between commutative and non-commutative connectives. The use of labels and constraints for designing a connection method has been already studied in the setting of a bunched logic, namely BI logic [16], in which labels and constraints are counterparts of the resource semantics [6]. Here an essential preliminary step is the computation of a polarization, which implicitly allows us to consider an intuitionistic encoding of the formula to prove. Moreover, we can naturally define a similar connection-based characterization of provability for the intuitionistic fragment of MNL (IMNL). A consequence of both characterizations is a new characterization of proof nets for both MNL logics and a new procedure for MNL proof nets construction that can be considered as an alternative connection method [5] and a verification method for MNL proof nets [14].

2 The Non-Commutative Logic

The MNL formulae are built from literals p, q, …, p^{⊥}, q^{⊥}, … with commutative connectives (conjunction ⊗ and disjunction & ) and non-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 MLL (resp. MCyLL) formulae are built from literals and the connectives ⊗ and & (resp. ⊙ and ⊲). The

\begin{aligned}\begin{aligned}& (Ax.) \\ ⊢ A, A^{⊥} \end{aligned} & \begin{aligned}⊢ Γ, A & ⊢ A^{⊥}, Δ \\ & (Cut) \\ ⊢ Γ, Δ \end{aligned} & \begin{aligned}⊢ Γ, A & ⊢ Δ, B \\ & (⊗) \\ ⊢ Δ, Γ, A ⊗ B \end{aligned} \\ \begin{aligned}⊢ Γ, A & ⊢ Δ, B \\ & (⊙) \\ ⊢ (Δ; Γ), A ⊙ B \end{aligned} & \begin{aligned}⊢ Γ, A, B \\ & ( & ) \\ ⊢ Γ, A & B \end{aligned} & \begin{aligned}⊢ Γ, (A; B) \\ & (⊲) \\ ⊢ Γ, A ⊲ B \end{aligned} \\ \begin{aligned}⊢ Γ [Δ; Σ] \\ & (Entropy) \\ ⊢ Γ [Δ, Σ] \end{aligned} & \begin{aligned}⊢ Γ, Δ \\ & (Seesaw) \\ ⊢ Γ; Δ \end{aligned} & \begin{aligned}⊢ Γ; Δ \\ & (CoSeesaw) \\ ⊢ Γ, Δ \end{aligned} \end{aligned}

Fig. 1. A sequent calculus for MNL

MNL sequent calculus, given in Figure 1, is based on bunches with two formula separators (a commutative ‘,’ and a non-commutative ‘;’). Moreover, it includes some explicit structural rules (Entropy and Seesaw) that establish relationships between both separators. We have added a restricted case of entropy, namely the rule CoSeesaw, that is the opposite of the Seesaw rule. More details are given in [17]. The phase semantics of MNL is defined as follows:

Definition 1 (Non-commutative phase space). A non-commutative phase space is a sextuplet P = (P, ·, ⋆, 1, ≤, ⊥) such that:

- (P, ·, 1) is a monoid,

- (P, ⋆, 1) is a commutative monoid,

- ≤ is a partial order on P, compatible with both monoidal structures and such that: ∀x, y ∈ P x ⋆ y ≤ x · y,

- ⊥ ⊆ P is an order ideal such that: ∀x, y ∈ P x · y ∈ ⊥ ⇔ x ⋆ y ∈ ⊥.

Given a phase space P, F ⊆ P and G ⊆ P, we define the following operations:

F ⊗G = (F ⋆G)^{⊥⊥}; F ⊙G = (F ·G)^{⊥⊥}; F & G = (G^{⊥} ⋆F^{⊥})^{⊥} and F ⊲G = (G^{⊥} ·F^{⊥})^{⊥}

Definition 2 (Validity). Given a phase space P and a valuation S that assigns a fact of P to any propositional symbol, we define the interpretation ⟦·⟧_{S}^{P} as usual. A formula F is valid if and only if 1 ∈ ⟦F ⟧_{S}^{P} for every phase space P and every interpretation S.

Theorem 1. The sequent calculus with explicit structural rules is sound and complete w.r.t. the phase semantics.

Proof. The complete proof is given in [17].

We aim to start from the sequent calculus with bunches and its proof-theoretical results in order to study proof search in MNL. Because of the presence of two context separators and two structural rules, this calculus is not well adapted for the design of proof search methods. For instance, the context splitting problem is hardened by the structure of sequents (see ⊗ and ⊙ rules). The structural rules impose an order between the sequent formulae modulo cyclicity. There is no explicit rule for cyclicity, but it can be recovered through applications of Seesaw and Entropy rules. In fact, in that case, we consider a restricted case of entropy through the rule CoSeesaw (see Figure 1). As an example, we consider the sequent ⊢ A, (B; (C, D)). It can be derived from ⊢ (A; B), C, D by a reversible sequence of Seesaw and Entropy rules. Both sequents can be considered to be equivalent modulo cyclicity. In order to represent sequents that are equivalent modulo reversible applications of Seesaw and CoSeesaw rules (ie modulo cyclicity), we consider sequents through a “viewpoint”. Considering a family F of sequents that are equivalent modulo cyclicity, we represent F by ⊢ Γ, A that is an element of F with A an arbitrary formula. Thanks to the following theorem any formula of any sequent of F can be considered as a “viewpoint”.

Theorem 2. Let ⊢ Γ be a MNL sequent and A be a formula in Γ, we can built from Γ a reversible derivation of ⊢ Δ, A by using only Entropy and Seesaw rules.

Proof. Given in detail in [17].

Sequent calculi without structural rules have been proposed for MNL [17]. The structure of formulae in such sequents is expressed through order varieties, that are a refinement of cyclic orders. Proof search in these calculi has been studied through the focalization and bipolar calculus [2, 4]. Our aim is to propose proof search methods based on simple (algorithmic) structures, that can be easily handled in an automated proof search procedure. In this perspective, order varieties (and their operations) as mathematical structures seem not to be appropriate for the design of useful proof search methods for MNL. Our previous works based on sequents and proof nets with formulae dependencies [7, 8] were a first step to find alternative and useful semantical structures. A key point of our approach is to separate in a simple way the linearity and non-commutativity aspects.

3 A matrix characterization for MNL

We define a matrix characterization for MNL by extending one characterization for MLL [5, 13] with specific labels and constraints that capture the interactions between commutative and non-commutative connectives. In fact, the label calculus allow to express in a simple way constraints on formulae ordering inside a context.

3.1 Dealing with linearity

First, we consider the matrix characterization for MLL of [5], by ignoring the structure of the context, and by seeing ⊙ as ⊗, and ⊲ as & . As usual in matrix characterizations, we first define the formula tree and thus consider the decomposition tree of the formula F to prove, where nodes are called positions (denoted a_{0}, a_{1}, …). A position u exactly identifies a subformula of F. We identify two

\begin{matrix}a_{0} & F_{0} \\ a_{1} & (B^{⊥} & C^{⊥}) ⊙ D^{⊥} \\ a_{2} & B^{⊥} & C^{⊥} \\ a_{3} & B^{⊥} \\ a_{4} & C^{⊥} \\ a_{5} & D^{⊥} \\ a_{6} & (D ⊲ [(C ⊗ B) ⊙ A]) & A^{⊥} \\ a_{7} & D ⊲ [(C ⊗ B) ⊙ A] \\ a_{8} & D \\ a_{9} & (C ⊗ B) ⊙ A \\ a_{10} & C ⊗ B \\ a_{11} & C \\ a_{12} & B \\ a_{13} & A \\ a_{14} & A^{⊥} \end{matrix}

Fig. 2. An example of formula tree

types of nodes, α and β: a node is of type α (resp. β) if the principal connective is &or ⊲ (resp. ⊗ or ⊙). Now, we define the notion of a path through a formula F, knowing that u denotes a position and l(u) (resp. r(u)) denotes the left (resp. right) premise of u.

Definition 3. Let F be a MNL formula, the set of paths through F is the smallest set of positions such that:

- {a_{0}} is a path;

- if {s, u} is a path then:

if type(u) = α then {s, l(u), r(u)} is a path;

if type(u) = β then {s, l(u)} and {s, r(u)} are paths. An atomic path is a path that contains only atomic positions.

Definition 4. Given a MNL formula F, a set of connections SC linearly spans F if and only if

- all literals in the formula tree appear exactly once in SC;

- if (a, b) and (c, d) are distinct elements of SC then a ≠ c and b ≠ d;

- every atomic path contains a connection from SC;

- no proper subset of SC spans F.

This definition is the one for MLL [5] without distinction between commutative and non-commutative connectives in the construction process of atomic paths. Thus, if a MNL formula F is such that there exists a set of connections SC that linearly spans F then the commutative version of F is provable in MLL. In order to illustrate the different steps of the characterization, we consider the following MNL formula: F_{0} = (B^{⊥} & C^{⊥}) ⊙ D^{⊥} & (D ⊲ [(C ⊗ B) ⊙ A]) & A^{⊥}. From this first step we obtain the indexed formula tree of F_{0} (see Figure 2) and build the set of paths following Definition 3. The set of atomic paths of F_{0} is:

\{ \begin{matrix}\{a_{3}, a_{4}, a_{8}, a_{11}, a_{14}\}, \{a_{3}, a_{4}, a_{8}, a_{12}, a_{14}\}, \{a_{3}, a_{4}, a_{8}, a_{13}, a_{14}\}, \\ \{a_{5}, a_{8}, a_{11}, a_{14}\}, \{a_{5}, a_{8}, a_{12}, a_{14}\}, \{a_{5}, a_{8}, a_{13}, a_{14}\} \end{matrix} \}

The set of connections {(a_{14}, a_{13}), (a_{3}, a_{12}), (a_{4}, a_{11}), (a_{8}, a_{5})} linearly spans F_{0}.

\begin{aligned}x ≤ y & x′ ≤ y′ \\ & (Comp_{⋆}) \\ x ⋆ x′ ≤ y ⋆ y′ \end{aligned}  \begin{aligned}x ≤ y & x′ ≤ y′ \\ & (Comp_{·}) \\ x · x′ ≤ y · y′ \end{aligned}

\begin{aligned}& (Ent) \\ x ⋆ y ≤ x · y \end{aligned}  \begin{aligned}& (Ax) \\ x ≤ x \end{aligned}  \begin{aligned}x ≤ y & y ≤ z \\ & (T r) \\ x ≤ z \end{aligned}

Fig. 3. Inference rules for constraint resolution

3.2 Dealing with the non-commutativity

In order to deal with ordering constraints within subformulae, we define label and constraints for MNL that in fact capture the semantics and allow us to encode the structure of MNL sequents, and to express constraints on it. Labels are computed w.r.t. a polarization of the formula that informally defines a “viewpoint” of a sequent.

Definition 5. A polarization pol for a MNL formula F is a function that associates a polarity (+ or −) to F and all its subformulae.

Definition 6. Given a formula F and a polarization pol for F, pol is nodecorrect if and only if, for every subformula of F it respects the following inductive rules:

\begin{matrix}pol(A ⊗ B) = + ⇒ pol(A) = pol(B) = +; & pol(A ⊗ B) = − ⇒ pol(A) ≠ pol(B); \\ pol(A ⊙ B) = + ⇒ pol(A) = pol(B) = +; & pol(A ⊙ B) = − ⇒ pol(A) ≠ pol(B); \\ pol(A & B) = − ⇒ pol(A) = pol(B) = −; & pol(A & B) = + ⇒ pol(A) ≠ pol(B); \\ pol(A ⊲ B) = − ⇒ pol(A) = pol(B) = −; & pol(A ⊲ B) = + ⇒ pol(A) ≠ pol(B); \end{matrix}

Definition 7. Given a formula F, a set of connections SC and a polarization pol, pol is admissible if and only if it is node-correct and for every connection (a, b) ∈ SC, pol(a) ≠ pol(b).

Theorem 3. Given a formula F, if there exists a set of connections SC that linearly spans F then there exists an admissible polarization for F.

Proof. Following [15], we can give a linear algorithm that, given a MNL formula, a set of connections and a DR-switching, builds a polarization for F.

Given a polarization of a formula to prove F, we define the notion of label. A label structure is a tuple L = (Σ, ⋆, ·, 1) such that: Σ is a set of so called simple labels, denoted a, b, c, …; ⋆ is a commutative monoidal operator; · is a monoidal operator; 1 is a unit for both ⋆ and ·. Labels are considered modulo associativity of ⋆ and ·, and commutativity of ⋆. A label is said linear when it contains no repetition of the same simple label. We express constraints on the structure of contexts through label constraints of the form x ≤ y and the resolution of such constraints is performed using the inference rules given in Figure 3. Given a set of constraints H and a constraint E, we write H |≈ E to express that there exists a derivation tree starting from

u  type(u) lbl(u) lbl(l(u)) lbl(r(u)) Cont(u)
A^{+} ⊗^{+} B^{+} β  x  y  z x ≤ y ⋆ z
A^{+} ⊗^{−} B^{−} β  l  x  x ⋆ l
A^{−} ⊗^{−} B^{+} β  l  x ⋆ l  x
A^{+} ⊙^{+} B^{+} β  x  y  z x ≤ y · z
A^{+} ⊙^{−} B^{−} β  l  x  l · x
A^{−} ⊙^{−} B^{+} β  l  x · l  x
A^{+} &^{+}B^{−} α  x  b ⋆ x  b
A^{−} &^{+}B^{+} α  x  a  a ⋆ x
A^{−} &^{−}B^{−} α  l  a  b l ≤ b ⋆ a
A^{+} ⊲^{+} B^{−} α  x  x · b  b
A^{−} ⊲^{+} B^{+} α  x  a  a · x
A^{−} ⊲^{−} B^{−} α  l  a  b l ≤ b · a

Fig. 4. Inductive rules for label computation

E, by using inferences given in Figure 3 and such that each branch ends with a Ax-rule, a Ent-rule or with a constraint of H. If E is a set of constraints, we write H |≈ E to express that, for all E ∈ E we have H |≈ E. Given a MNL formula F and a node-correct polarization for F, we can compute the polarities of F subformulae by starting from F with the polarity + and the label 1 and by applying the rules given in Figure 4. The labels associated with premises of ⊗^{+} or ⊙^{+} nodes and to the positive premise of ⊗^{−} or ⊙^{−} nodes are considered as variables. The labels associated with premises of &^{−} or ⊲^{−} nodes, and to the negative premise of &^{+} or ⊲^{+} nodes are considered as constants (simple labels). A substitution σ is an application that associates a label l to a variable x such that l is a element of the label structure (C, ⋆, ·, 1), where C denotes the set of constants. In some cases, we generate label constraints that are splitted into two sets: the set of assertions (Ass) that are introduced by &^{−} or ⊲^{−} nodes, and the set of requirements (Req) that are introduced by ⊗^{+} and ⊙^{+} nodes. The assertions are axioms in the calculus on constraints. We can notice that label constraints express some constraints on the formulae structure inside a sequent. Therefore, one could expect to have also such constraints associated to &^{+}, ⊲^{+}, ⊗^{−} and ⊙^{−}. For these nodes, constraints are expressed through the way the premise labels are computed and the constraints derived from connections.

Definition 8. A formula F of MNL is connection-provable if and only if

i) there exists a set of connections SC such that linearly spans F; ii) there exists an admissible polarization pol and a substitution σ such that:

- For every connection (a^{+}, a^{−}) of SC, σ(Ass) |≈ σ(a^{+} ≤ a^{−}),

- σ(Ass) |≈ σ(Req).

Coming back to our example, we can now enrich its formula tree with labels. The polarity and the label associated to each subformula of F_{0} are given in the labelled formula tree of F_{0} are given in Figure 5. Moreover we have some

u Pol(u) lbl(u) Cont(u)
a_{0} +  1
a_{1} −  e
a_{2} − s · e s · e ≤ b ⋆ c
a_{3} −  b
a_{4} −  c
a_{5} +  s
a_{6} +  e

\begin{matrix}a_{7} & + & a ⋆ e \\ a_{8} & − & d \\ a_{9} & + & d · (a ⋆ e) & d · (a ⋆ e) ≤ t · x \\ a_{10} & + & t & t ≤ z ⋆ y \\ a_{11} & + & z \\ a_{12} & + & y \\ a_{13} & + & x \\ a_{14} & − & a \end{matrix}

Fig. 5. An example of labelled formula tree

label constraints. Among them, we can distinguish an assertion: s · e ≤ b ⋆ c, two requirements: d · (a ⋆ e) ≤ t · x and t ≤ z ⋆ y and constraints coming from connections: x ≤ a, y ≤ b, z ≤ c and s ≤ d. In these constraints, {a, b, c, d, e} are constants (simple labels), and {x, y, z, s, t} are variables. In order to solve these constraints, we can easily deduce, from the constraints obtained from connections, a partial substitution: {x ↦ a, y ↦ b, z ↦ c, s ↦ d}. Moreover, the requirement t ≤ z ⋆ y becomes t ≤ c ⋆ b and thus can be satisfied if we consider t ↦ b ⋆ c. Then, this substitution trivially satisfies constraints from connections and the requirement t ≤ z ⋆ y. We have now to verify that it also satisfies the last requirement d · (a ⋆ e) ≤ t · x. Using inference rules of Figure 3 we can obtain the following proof:

\begin{aligned}d ≤ d & a ⋆ e ≤ e · a \\ & (Comp) \\ d · (a ⋆ e) ≤ d · e · a \end{aligned} \begin{aligned}d · e ≤ b ⋆ c & a ≤ a \\ & (Comp) \\ d · e · a ≤ (b ⋆ c) · a \end{aligned}
(T r)
d · (a ⋆ e) ≤ (b ⋆ c) · a

Let us remark that the label constraints capture the constraints on the bunched context for rule applications in the MNL sequent calculus. For instance, the constraint a ⋆ e ≤ e · a corresponds to the use of the Entropy rule in the sequent calculus. Finally, we check that the MNL formula of our example is connectionprovable and in fact valid (see next subsection). Let us consider now the formula G_{0} = (B^{⊥} & C^{⊥}) ⊙ D^{⊥} & (D ⊲ [(C ⊗ B) ⊗ A]) & A^{⊥} that is obtained from the previous one by changing (C⊗B)⊙A to (C⊗B)⊗A. If we take the same polarization as for F_{0}, we obtain the same computed labels. But the requirement generated by the subformula (C ⊗B)⊗A is now d·(a⋆e) ≤ t⋆x. Using the substitution, we obtain the constraint d · (a ⋆ e) ≤ b ⋆ c ⋆ a, that cannot be satisfied. Taking another admissible polarization changes the labels and the constraints associated to subformulae, but the set of constraints does not admit a solution. Then, as we have no other choice for the set of connections, we can state that G_{0} is not connection-provable, and consequently is not valid in MNL.

3.3 Properties of the characterization

Let us show that our characterization is correct and complete w.r.t. the MNL sequent calculus with bunches. It is mainly based on: a) a polarization of the sequent in order to deal with irrelevant (reversible) applications of (co-)seesaw rules; b) labels to represent the structure of formulae inside a sequent; c) constraints on labels to deal with applications of the Entropy rule in the sequent calculus. A key point is that provability is independent from the choice of an admissible polarization. If, for such a choice, the set of constraints has no solution then we can claim the non-provability for the given set of connections and thus try another one if possible. An admissible polarization for F is defined in such a way that if ⊢ Γ is a sequent that can be derived from F, then there exists exactly one positive formula in ⊢ Γ. In some way, our polarization gives a “viewpoint” of a MNL sequent, as defined in the previous section. The structure of formulae within a sequent ⊢ Δ is considered w.r.t. the structure of ⊢ Γ^{−}, A^{+}, where ⊢ Γ, A is equivalent to ⊢ Δ modulo cyclicity. Moreover, labels are computed w.r.t. the polarization in such a way that, given a set of connections SC, the sets of constraints generated from a choice of an admissible polarization are all equivalent. This is related to the fact that, in the MNL sequent calculus, sequents are equivalent modulo cyclicity (as said in previous section). As an example, we consider the part of the proof of F_{0} (see Figure 6). Each formula inside a sequent is together with its label. We can easily see that the label d · (a ⋆ e) (associated with (C ⊗ B) ⊙ A, that is the positive formula of S_{2} and S′_{2}) represents the structure of both S_{2} and S′_{2}.

⊢ [e : (B^{⊥} & C^{⊥}) ⊙ D^{⊥}; d : D], t : C ⊗ B \begin{aligned}& (Ax.) \\ ⊢ x : A, a : A^{⊥} \end{aligned}
(⊙)

S_{1} : ⊢ [a : A^{⊥}; e : (B^{⊥} & C^{⊥}) ⊙ D^{⊥}; d : D], d · (a ⋆ e) : (C ⊗ B) ⊙ A

(Entropy)

S′_{2} : ⊢ [(a : A^{⊥}, e : (B^{⊥} & C^{⊥}) ⊙ D^{⊥}); d : D], d · (a ⋆ e) : (C ⊗ B) ⊙ A

(Seesaw)
⊢ [a : A^{⊥}, e : (B^{⊥} & C^{⊥}) ⊙ D^{⊥}]; d : D; d · (a ⋆ e) : (C ⊗ B) ⊙ A
(Ent.)

S_{2} : ⊢ e : (B^{⊥} & C^{⊥}) ⊙ D^{⊥}, (d : D; d · (a ⋆ e) : (C ⊗ B) ⊙ A), a : A^{⊥}

Fig. 6. A part of proof with labels

Now, we illustrate how label constraints are related to ordering constraints within a sequent. Let us consider the sequent ⊢ Σ, A ⊙ B. In order to apply a ⊙-rule we need to turn the context Σ into the form Δ; Γ. This transformation is not reversible in general and induces some constraints on (the structure of) Γ and Δ. Let us consider the way labels and constraints are computed for ⊙^{+}. The requirement l ≤ x · y expresses that Σ has to be turned into the particular form Δ; Γ, and thus some constraints on variables x and y. In the case of ⊙^{−}, we have to compute labels in a different way taking into account the polarization. Constraints on contexts are expressed by the way labels are computed and by equations coming from connections. In our example, we have to apply an Entropy rule to obtain the sequent S_{1} from S_{2}. The structure of S_{1} would be represented by the label d · e · a. In our characterization, we associate a constraint d · (a ⋆ e) ≤ t · x to (C ⊗ B) ⊙ A. We have to use an entropy relation namely a ⋆ e ≤ e · a, to solve this constraint. Let us remind that a MNL sequent ⊢ Γ is provable in MNL if and only if Dis(Γ) is connection-provable, where Dis : Context ↦ F ormula is defined by: Dis(A) = A if A is a formula; Dis(Γ, Δ) = Dis(Γ) & Dis(Δ); Dis(Γ; Δ) = Dis(Γ) ⊲ Dis(Δ).

Theorem 4 (Correctness). If a MNL formula F is connection-provable then it is provable in the MNL sequent calculus.

Proof. At first, the existence of a set of connections that linearly spans F gives a proof in MLL of the commutative version of F. It provides a skeleton for the proof of F in MNL. Then, we need to attach a structure to each sequent of this skeleton. For that, we use the label associated to each formulae. In fact, the label of the positive formula induces an order between other (negative) formulae. The existence of a solution such that label constraints are satisfied ensures that we can insert structural rules, between each inference of the skeleton, such that the proof construction leads to a MNL proof.

Theorem 5 (Completeness). If a MNL formula F is provable in the MNL sequent calculus then F is connection-provable.

Proof. If the formula F is provable, then there exists a proof of F in the MNL sequent calculus. From this proof, we can deduce a set of connections that linearly spans F (see [5] for more details). We can then compute an admissible polarization for F and by linearity, in any sequent appearing in the proof there is exactly one positive formula (other formulae of the sequent being negative). Thus, the polarization gives a so-called viewpoint in any sequent, and the label associated to the positive formula represents the structure of the negative formulae. Then, given this viewpoint, we can relate the rule of structural entropy with the corresponding Entropy rule in the calculus of constraints.

3.4 The related connection method

From this characterization we can define a connection-based proof search method with the following main steps: 1) to compute the atomic paths and choose a spanning set of connections like in MLL [5, 13]; 2) to compute, from the set of connections, an admissible polarity and then labels and constraints; 3) to compute a substitution that is a solution for the set of constraints (connection constraints and requirements satisfied from assertions). Steps 1) and 2) being standard and without difficulty we aim to analyze the step 3) and its main problem, that is to find a substitution such that requirements can be proved from assertions using some particular inference rules. Given these rules, constraints of the form x ≤ a (where x is a variable and a is a constant) are satisfied if and only if σ(x) = a. The way in which constraints are generated makes constraint resolution relatively easy. Moreover, we can use the linearity of labels to reduce the search space. Assertions are of the form l ≤ a□b, where a and b are constants (simple labels) and l is a label composed of variables and constants (l does not contain a or b). Requirements are of the form l ≤ x□y, where x and y are (fresh) variables. Thus, variables have a very restricted set of possible instantiations. Moreover, labels attached to positive formulae always appear on the left-hand side of a constraint (generated by a connection or by a ⊗^{+} or ⊙^{+} rule). However, when created, variables are attached to positive premise (for instance, see the construction of labels for ⊗^{+} in Figure 4). As a result, variables always appear in the right-hand side of a constraint and on the left-hand side of another one. This means that the set of admissible values of each variable is strongly restricted by the constraints. Coming back to our example, the variable t appears on the left-hand side of t ≤ z ⋆ y (y and z appear in the constraint y ≤ b and z ≤ c). It also appears on the right-hand side of d · (a ⋆ e) ≤ t · x. Thus, from this requirement (and taking into account that σ(x) = a, we can deduce the following constraint d·e ≤ t, using compatibility and entropy rules. Then, the choices of values for t are strongly reduced because of the constraint d · e ≤ t ≤ b ⋆ c that admits a solution because we have an assertion d · e ≤ b ⋆ c. In our example, we have seen that σ(t) = b ⋆ c satisfies requirements and that σ(t) = d · e is also a solution for t. These two solutions for t can be considered equivalent, as they are deducible from each other using the assertion. The choice between b⋆c and d·e depends on strategies applied to compute a substitution. A smart choice of substitution can strongly reduce the complexity of constraints resolution.

4 A Characterization for Intuitionistic MNL

From the previous results on MNL, we aim to analyze what happens in the case of Intuitionistic MNL (IMNL). This work is inspired from the relationships between MLL and MILL described in [15]. IMNL formulae are built from propositional variables p, q, … and commutative connectives ⊗ and ⊸, and non-commutative ones ⊙, −• and •−. The corresponding sequent calculus is given in Figure 7. There exists a strong relationship between MLL and intuitionistic MLL [15] that can be extended to MNL. In fact, any IMNL formula can be translated to a MNL formula using De Morgan laws and the equalities: A ⊸ B = A^{⊥} & B, A−•B = A^{⊥} ⊲ B and B•−A = B ⊲ A^{⊥}. For that, given a IMNL formula A, we define its classical counterpart \overline{A} (and \underline{A}). Let A be an IMNL formula, we define its classical counterpart \overline{A} (and \underline{A}) as follows:

\begin{matrix}\overline{a} = a & \underline{a} = a^{⊥} & \overline{A ⊗ B} = \overline{A} ⊗ \overline{B} & \underline{A ⊗ B} = \underline{B} & \underline{A} \\ \overline{A ⊙ B} = \overline{A} ⊙ \overline{B} & \underline{A ⊙ B} = \underline{B} ⊲ \underline{A} & \overline{A ⊸ B} = \underline{A} & \overline{B} & \underline{A ⊸ B} = \underline{B} ⊗ \overline{A} \\ \overline{A−•B} = \underline{A} ⊲ \overline{B} & \underline{A−•B} = \underline{B} ⊙ \overline{A} & \overline{B•−A} = \overline{B} ⊲ \underline{A} & \underline{B•−A} = \overline{A} ⊙ \underline{B} \end{matrix}

\begin{matrix}\begin{aligned}& (Ax.) \\ A ⊢ A \end{aligned} & \begin{aligned}Γ [Δ; Σ] ⊢ C \\ & (Ent.) \\ Γ [Δ, Σ] ⊢ C \end{aligned} & \begin{aligned}Γ ⊢ A & Δ ⊢ B \\ & (⊗_{R}) \\ Γ, Δ ⊢ A ⊗ B \end{aligned} \\ \begin{aligned}Γ [A, B] ⊢ C \\ & (⊗_{L}) \\ Γ [A ⊗ B] ⊢ C \end{aligned} & \begin{aligned}Γ ⊢ A & Δ ⊢ B \\ & (⊙_{R}) \\ Γ; Δ ⊢ A ⊙ B \end{aligned} & \begin{aligned}Γ [A; B] ⊢ C \\ & (⊙_{L}) \\ Γ [A ⊙ B] ⊢ C \end{aligned} \\ \begin{aligned}Γ ⊢ A & Δ[B] ⊢ C \\ & (⊸_{L}) \\ Δ[Γ, A ⊸ B] ⊢ C \end{aligned} & \begin{aligned}A, Γ ⊢ B \\ & (⊸_{R}) \\ Γ ⊢ A ⊸ B \end{aligned} & \begin{aligned}Γ ⊢ A & Δ[B] ⊢ C \\ & (−•_{L}) \\ Δ[Γ; A−•B] ⊢ C \end{aligned} \\ \begin{aligned}A; Γ ⊢ B \\ & (−•_{R}) \\ Γ ⊢ A−•B \end{aligned} & \begin{aligned}Γ ⊢ A & Δ[B] ⊢ C \\ & (•−_{L}) \\ Δ[B•−A; Γ] ⊢ C \end{aligned} & \begin{aligned}Γ; A ⊢ B \\ & (•−_{R}) \\ Γ ⊢ B•−A \end{aligned} \end{matrix}

Fig. 7. A sequent calculus for IMNL

From this definition we have the following result

Theorem 6. A IMNL sequent H_{1}, …, H_{n} ⊢ C is provable if and only if the sequent MNL ⊢ \underline{H_{1}}, …, \underline{H_{n}}, \overline{C} is provable.

Proof. We build a proof of H_{1}, …, H_{n} ⊢ C from a proof of ⊢ \underline{H_{1}}, …, \underline{H_{n}}, \overline{C} and conversely. An intuitionistic sequent Γ ⊢ A, where Γ is a context with bunches, can be easily turned into a one-sided sequent, using negation and De Morgan laws. Moreover, as stated in theorem 2, any sequent ⊢ Δ[A] can be reversibly turned into the form ⊢ Γ, A.

Consequently, any linearly balanced IMNL formula A can be transformed to a variant MNL formula which is built from polarized atoms and polarized connectives in the following way

\begin{matrix}⌜a⌝ = a^{+} & ⌞a⌟ = a^{−} & ⌜A ⊗ B⌝ = ⌜A⌝ ⊗^{+} ⌜B⌝ \\ ⌞A ⊗ B⌟ = ⌞B⌟ &^{−}⌞A⌟ & ⌜A ⊙ B⌝ = ⌜A⌝ ⊙^{+} ⌜B⌝ & ⌞A ⊙ B⌟ = ⌞B⌟ ⊲^{−} ⌞A⌟ \\ ⌜A ⊸ B⌝ = ⌞A⌟ &^{+}⌜B⌝ & ⌞A ⊸ B⌟ = ⌞B⌟ ⊗^{−} ⌜A⌝ & ⌜A−•B⌝ = ⌞A⌟ ⊲^{+} ⌜B⌝ \\ ⌞A−•B⌟ = ⌞B⌟ ⊙^{−} ⌜A⌝ & ⌜B•−A⌝ = ⌜B⌝ ⊲^{+} ⌞A⌟ & ⌞B•−A⌟ = ⌜A⌝ ⊙^{−} ⌞B⌟ \end{matrix}

The transformation of a one-sided sequent into a two-sided (intuitionistic) sequent corresponds to a polarization of the sequent, as previously defined. In fact, a node-correct polarization follows De Morgan laws, and the definition of linear implication(s). Given a IMNL formula A we built a MNL formula ⌜A⌝ formula with a unique polarization, denoted ipol(A), derived from the above construction. It is easy to verify that it is node-correct. From now, we can apply the connection-based method of MNL and derive the following definition:

Definition 9. A formula F of IMNL is connection-provable if and only if

i) there exists a set of connections SC such that linearly spans ⌜A⌝. ii) given the polarization ipol(A), there exists a substitution σ such that:

- for every connection (a^{+}, a^{−}) of SC, σ(Ass) |≈ σ(a^{+} ≤ a^{−}),

- σ(Ass) |≈ σ(Req).

It means that a formula A of IMNL is connection-provable if and only if ⌜A⌝ is connection-provable in MNL but with a fixed polarization ipol(A).

Theorem 7. A IMNL formula A is valid if and only if A is connection-provable.

Proof. Similar to the proof for MNL with ipol(A) as an admissible polarization.

As an example, we can consider A, D−•(C ⊗ B) ⊢ D−•[(C ⊗ B) ⊙ A]. Its translation into an equivalent polarized MNL formula leads to the formula F_{0} with the polarization given in Figure 5.

5 MNL Proof nets

The notion of proof net has been introduced by Girard [11] in order to cope with the problems due to the intrinsic concurrence of the linear sequent calculus. It corresponds to a concise graph-theoretic representation of linear logic deductions. This concept, initially defined for MLL, has been defined for various LL fragments and then for MNL [1]. We can define a proof structure from a pair (Dectree, Axlinks) where, for a given sequent, Dectree is the set of its subformulae arranged as a decomposition tree and Axlinks is a set of axiom-links (or connections) between positive and negative occurrences of the same atomic formula. Such a pair is a proof structure if each atom of Dectree is the conclusion of exactly one axiom-link. There exist various correctness criteria that decides if a proof structure of a LL fragment corresponds to a (graphical) proof of a given sequent or not, i.e., if a proof structure is a proof net. It is known that a based-on connection characterization of MLL directly provides a new correctness criterion for MLL proof nets [5]. Moreover, an algorithm that builds a MLL proof net provides a connection method that builds in parallel a sequent proof and a proof net, in case of provability [5, 9].

Correctness and verification of proof nets. As a first consequence of our based-on connection characterization of MNL we can straightforwardly deduce a new correctness criterion for MNL proof nets based on a criterion for MLL with the computation of a polarization, the generation of labels and constraints and the satisfaction of requirements from assertions. Thus, we can design an algorithm for the verification of a MNL proof structure, starting by the verification of the MLL proof structure associated to the MNL one (without difference between commutative and non-commutative connectives), for instance with a linear algorithm [15]. The proof structure including a given set of connections, we can compute in parallel an admissible polarization for it (following [15]), and then compute labels attached to nodes (subformulae) of the proof structure and the set of constraints to satisfy.

Proof nets construction. Given a MLL formula F, there exists an algorithm [5] that automatically builds a set of axiom-links (or connections) such that the decomposition tree of F, together with this set of axiom-links is a proof net. It directly provides a particular connection method for MLL. We can easily adapt this algorithm to compute a set of connections that linearly spans a given MNL formula F. Then, as for the verification, we compute, in parallel with the construction of axiom-links, an admissible polarization for F and then generate the labels attached to subformulae (or nodes) in the proof structure. Finally, we solve the requirements from the assertions and check if there is a solution for the set of constraints. This algorithm can be adapted to intuitionistic MNL proof nets by only checking polarities during the axiom-links construction.

6 Conclusion and Perspectives

We present a connection-based characterization of the multiplicative fragment of Non-Commutative logic (MNL). It is related to a MNL sequent calculus with bunches and its phase semantics [17]. Its main steps are: to consider a MNL formula, first without distinction between commutative and non-commutative connectives; to introduce a polarization, that means to consider MNL through its intuitionistic fragment; to build labels and constraints that are syntactic counterparts of the semantics; to characterize provability through the resolution of constraint. Because of the central role of polarization, we can naturally derive a similar connection-based characterization for the intuitionistic fragment of MNL. Compared to other works on MNL proof construction, that are based on order varieties and the focusing principle [2, 4] and that deal with partial information in a specific way, our approach tends to separate the linearity from the non-commutativity during the proof construction process with the help of labels, constraints and constraint resolution. A similar approach has been already studied for the BI logic [16], in which additive and multiplicative connectives cohabit, but with different labels and constraints that capture a different semantics [6]. Moreover, we can derive a new correctness criterion for MNL proof nets and propose algorithms for the verification and the construction of MNL proof nets from our previous works on MLL [5]. In further work, we will focus on the constraint resolution process that deals with simple labels and particular constraints. Moreover, we will study the complexity of MNL proof net verification from our new criterion, in comparison with the quadratic one of [14]. The labels and constraints being syntactic counterparts of the semantics, we will also consider the problem of countermodel generation in MNL in case of non-provability.

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. J.M. Andreoli. Focussing and Proof construction. Annals of Pure and Applied Logic, 107:131–163, 2001.

3. J.M. Andreoli. Focusing proof-net construction as a middleware paradigm. In 18th Int. Conference on Automated Deduction, CADE-18, LNAI 2392, pages 501–516, 2002. Copenhagen, Danemark.

4. C. Faggian. Proof construction and non-commutativity: a cluster calculus. In International Conference on Principles and Practice of Declarative Programming, PPDP 2000, 2000. ACM Press.

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

6. D. Galmiche and D. Méry. Connection-based proof search in propositional BI logic. In 18th Int. Conference on Automated Deduction, CADE-18, LNAI 2392, pages 111–128, 2002. Copenhagen, Danemark.

7. D. Galmiche and J.M. Notin. Proof-search and Proof nets in Mixed Linear Logic. Electronic Notes in Theoretical Computer Science, 37, 2000.

8. D. Galmiche and J.M. Notin. Calculi with Dependency Relations for Mixed Linear Logic. In International Workshop on Logic and Complexity in Computer Science, LCCS’2001, pages 81–102, Créteil, France, 2001.

9. D. Galmiche and G. Perrier. A procedure for automatic proof nets construction. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 42–53, St. Petersburg, Russia, July 1992.

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. D. Gray, G. Hamilton, J. Power, and D. Sinclair. Specifying and verifying TCP/IP using Mixed Intuitionistic Linear Logic. Technical report, Dublin City Univ., 2001.

13. C. Kreitz, H. Mantel, J. Otten, and S. Schmitt. Connection-based proof construction in Linear Logic. In 14th Int. Conference on Automated Deduction, CADE-14, LNCS 1249, pages 207–221, Townsville, North Queensland, Australia, 1997.

14. V. Mogbil. Quadratic correctness criterion for non commutative logic. In 15th Int. Workshop on Computer Science Logic, CSL 2001, LNCS 2142, pages 69–83, Paris, France, 2001.

15. A. S. Murawski and C.-H. L. Ong. Dominator trees and fast verification of proof net. In 15th IEEE Symposium on Logic in Computer Science, Santa Barbara, California, June 2000.

16. P.W. O’Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.

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

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