Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic

Abstract

We propose a connection-based characterization for multiplicative intuitionistic linear logic (MILL) which is based on labels and constraints that capture Urquhart's possible world semantics of the logic. We rst briey recall the purely syntactic sequent calculus for MILL, which we call LMILL. Then, in the spirit of our previous results on the Logic of Bunched Implications (BI), we present a connection-based characterization of MILL provability. We show its soundness and completeness without the need for any notion of multiplicity. From the characterization, we nally propose a labelled sequent calculus for MILL.

Introduction

A ` A

ax Γ, A, B, Δ ` C Γ, A ∗ B, Δ ` C Γ ` A

Δ, B ` C Γ, A −∗ B, Δ ` C ∗L −∗L Γ ` C Γ, 1 ` C 1L ` 1

1R Γ ` A

Δ ` B Γ, Δ ` A ∗ B

∗R Γ, A ` B Γ ` A −∗ B

−∗R The propositional language of MILL consists of a denumerable set L = P, Q, . . . of propositional letters, the multiplicative unit 1 and the multiplicative connectives ∗ and −∗. P(L), the collection of MILL propositions over L, is given by the following inductive denition:

A ::= P | 1 | A ∗ A | A −∗ A.

Let us remark that since the forthcoming connection-based characterization of MILL-provability is inspired by our previous work on BI [ 2 ], we do not use the more widespread symbols ⊗ and −◦ to denote multiplicative conjunction and implication and rather stick with the star and magic-wand notations of these connectives.

Judgements of MILL are sequents of the form Γ ` A, where A is a proposition and Γ, called the context, is a (possibly empty) multiset of formulas.

The standard sequent calculus for MILL, which we call LMILL 1, is given in Figure 1. One diculty with such a calculus lies in the fact that the rules for left-implication and rightconjunction both require context splitting from conclusion to premises. Making relevant choices when context-splitting is required is crucial for the eciency of backward proof-search.

The semantics we use for MILL models is a possible worlds semantics la Kripke, mainly inspired from the operational semantics of Urquhart [ 12 ]. Let us recall it briey. Denition 1 (MILL-frame). A MILL-frame is a partially ordered commutative monoid h M, ·, e, v i, in which M is a set of worlds and v is compatible with ·, i.e.: M = ∀m∀n ∈ M. if m v n and m0 v n0 then m · m0 v n · n0.

Denition 2 (MILL-interpretation) . A MILL-intepretation is a function J−K : L → P(M ) that satises Kripke monotonicity, i.e.:

∀m, n ∈ M. if m v n and m ∈ JPK then n ∈ JPK.

Denition 3 (MILL-model). Let P(L) be the collection of MILL propositions over a language L of propositional letters, a MILL-model is a structure R = h M, ·, e, v, J−K, |= i, in which h M, ·, e, v i is a MILL-frame, J−K is a MILL-interpretation, and |= is a forcing relation on M × P(L) satisfying the following conditions: • m |= P i

m ∈ JPK 1 In the spirit of LJ and LK for intuitionistic and classic logic, although LMILL has no labels. • m |= 1 i e v m • m |= A ∗ B i there exist

n1, n2 ∈ M such that n1 · n2 v m, n1 |= A and n2 |= B • m |= A −∗ B i, for all n1, n2 ∈ M , if n1 |= A and m · n1 v n2 then n2 |= B. Denition 4 (MILL-validity). Let R be MILL-model. A formula A is valid in R, written R |= A, i e |= A. A is valid, written, |= A, i R |= A for all models R. A nite set of formulas { A1, . . . , An } entails a formula B, written A1, . . . , An |= B, i |= (A1 ∗ . . . ∗ An) −∗ B. Theorem 1 (Soundness and Completeness) . For all formulas A, |= A i ` A. 3

Labelled Connections for MILL

The connection-based characterization of MILL-provability we dene in this paper is based on labels and constraints that capture the semantic properties of MILL-frames instead of capturing the syntactic properties (such as permutabilities, context-splitting or linearity) of the purely syntactic sequent calculus LMILL as the standard prex-based approach does for IL or MLL [ 5, 6, 13 ]. We already successfully used a similar approach for BI [ 2 ], and since BI is conservative w.r.t. MILL [ 7 ], the characterization in [ 2 ] also applies to MILL. However, although the characterization for MILL presented in this paper can indeed be seen as a renement of the one given for BI, its improvements are two-fold: rstly, it does not need any notion of multiplicity and, secondly, it is local in that the conditions for characterizing provability are not stated w.r.t. the global set of atomic paths but w.r.t. each atomic path individually. The locality of the characterization is a key step towards implementing a memory-space ecient depth-rst path-reduction strategy in a future connection-based prover for MILL. Indeed global conditions would require us to keep the whole set of atomic paths in memory while checking provability conditions. Since the number of atomic paths can grow exponentially large with the size of a formula, local conditions are preferable if one wants to make a more ecient use of the memory space (linear in the size of the initial formula). 3.1

Labels and Constraints Given an alphabet C (for example a, b, c, · · · ), C0, the set of atomic labels over C, is dened as the set C extended with the unit symbol . We then dene LC, the set of labels over C, as the smallest set containing C0, and closed under composition ( x, y ∈ LC implies xy ∈ LC). Labels are considered up to associativity, commutativity and identity w.r.t. . Therefore, aabcc, cbaca and cbcaa are simply regarded as equivalent.

A label constraint is an expression x ≤ y where x and y are labels. A constraint of the form x ≤ x is called an axiom and we write x = y to express that x ≤ y and y ≤ x. We use the following inference rules for reasoning on constraints: x ≤ x

R x ≤ z z ≤ y x ≤ y

T x ≤ y x0 ≤ y0 xx0 ≤ yy0

F

The R and T rules formalize the reexivity and transitivity of ≤ while the F rule corresponds to the functoriality (also called compatibility) of label-composition w.r.t. ≤. In this formal system, given a constraint k and a set of constraints H, we write H |≈ k if there is a deduction of k from H. The notation H |≈ K, where K is a non-empty set of constraints, means that for all k ∈ K, H |≈ k. 3.2

Labelled Indexed Formula Tree Here we recall the standard notions coming from previous matrix-characterizations of provability [ 6, 13 ]. A decomposition tree of a formula A is its representation as a syntactic tree with nodes called positions. A position u exactly identies a subformula of A denoted f (u). An atomic position is a position for an atomic formula. If u is a non-atomic position the principal connective of f (u) is denoted c(u). Moreover such a position corresponds to an internal node and we denote [u]i with i ∈ { 1, 2 } the position of the i-th child of the node corresponding to u and then [u]? = { v | (∃i ∈ N)(v = [u]i) }. If u is not a root position we say that u is of rank r(u) = i if u is the i-th child of its father position denoted by [u]0.

The decomposition tree induces a partial order on the positions such that the root is the least element and if u v then u dominates v in the tree or in the formula (from now on we do not distinguish a formula A from its decomposition tree). Then we denote [u] ↑ the set { v | v ∈ A and v u } of upward positions of u and [u] ↓ the set { v | v ∈ A and u v } of its downward positions. The notations [·] ↑ and [·] ↓ are easily generalized to a set s of positions by [s] ↑ = { u | u ∈ [v] ↑ and v ∈ s } and [s] ↓ = { u | u ∈ [v] ↓ and v ∈ s }.

For each position, we assign a polarity pol(u) but also a principal type ptyp(u) and a secondary type styp(u). Therefore, we have dierent principal types depending on the connective and the associated polarity. We dene two principal types named πα, πβ . Given a set of positions p, Pα(p) = { u | u ∈ p and ptyp(u) = πα } is the set of positions of type πα and Pβ (p) = { u | u ∈ p and ptyp(u) = πβ } is the set of positions of type πβ .

Moreover we consider the following sets of secondary type positions: for i in { 1, 2 }, Sαi(p) = { u | u ∈ p and styp(u) = παi }, Sβ i(p) = { u | u ∈ p and styp(u) = πβ i } and Sα(p) = Sα1(p) ∪ Sα2(p), Sβ (p) = Sβ 1(p) ∪ Sβ 2(p).

Depending on the principal type, we associate a label slab(u) and sometimes a constraint kon(u) to a position u. Such a label is either a position or a position with a tilde in order to identify the formula that introduced the label. We dene constraints in order to capture contextsplitting. The labelled signed formula lsf (u) of a position u is a triple (slab(u), f (u), pol(u)) and is denoted f (u)pol(u) : slab(u). The construction of an indexed formula tree is obtained by inductively applying the rules described in Figure 2.

lsf (u) (A −∗ B)0 : x (A ∗ B)1 : x (A −∗ B)1 : x (A ∗ B)0 : x ptyp(u) πα πα πβ πβ kon(u) xu ≤ u˜ uu˜ ≤ x xu ≤ u˜ uu˜ ≤ x lsf (u1) A1 : u A1 : u A0 : u A0 : u lsf (u2) B0 : u˜ B1 : u˜ B1 : u˜

B0 : u˜

For a given formula A the root position a0 has a polarity pol(a0) = 0, a label slab(a0) = and the signed formula (A)0 : where is the identity of label composition. u1 and u2 are respectively the rst and second subpositions. The principal type of a position u depends on its principal connective and polarity.

The constraints associated to πα-positions are called assertions while those associated to πβ -positions are called requirements. The atomic labels introduced by positions of principal type πα (resp. πβ ) are called constants (resp. variables). Given a set of positions p, the associated sets of assertions and requirements are Kα(p) = { kon(u) | u ∈ Pα(p) } and Kβ (p) = a5 a2 a4 a1 πα πα − πα πβ − − − πβ πβ − πα − − − a6 a3 a7

a10 a0 { kon(u) | u ∈ Pβ (p) } respectively. The associated sets of constants and variables are then dened as Σα(p) = { x | x occurs in Kα(p) } and Σβ (p) = { x | x occurs in Kβ (p) }. We set Σαβ (p) = Σα(p)∪Σβ (p) and dene Lα(p), Lβ (p) and Lαβ (p) as the sets of atomic and compound labels generated by Σα(p), Σβ (p) and Σαβ (p) respectively. For readability, we omit the set of positions p in notations whenever p is the set Pos of all positions. 3.2.1

An Example (part 1) Let us consider the formula A ≡ (P ∗ ((Q −∗ R) ∗ S)) −∗ ((P ∗ (Q −∗ R)) ∗ S) that is represented as a syntax tree each node of which being identied with a position (see the tree at the righthand side of Figure 3). Moreover, we can associate an indexed formula tree (with labelled signed formulae as nodes), inductively built from (A)0 : and the rules of Figure 2. This tree is the one at the lefthand side of Figure 3. In parallel, we have the generation of constraints for the positions of principal type πα and πβ (see kon(u) in the table of Figure 3). Then, in this case we can deduce that Pα = { a0, a1, a3, a11 }, Pβ = { a4, a8, a9 }, Sα1 = { a1, a2, a4, a12 }, Sβ 1 = { a5, a9, a10 }, Sα2 = { a3, a7, a8, a13 }, Sβ 2 = { a6, a11, a14 }. In addition the assertions and requirements are

Kα = { a0 ≤ a˜0, a1a˜1 ≤ a0, a3a˜3 ≤ a˜1, a˜9a11 ≤ a˜11 } Kβ = { a8a˜8 ≤ a˜0, a9a˜9 ≤ a8, a3a4 ≤ a˜4 } { a0 } { a1, a8 } { a2, a3, a8 } { a2, a4, a7, a8 } { a2, a5, a7, a8 }

{ s, a11 } In this section, we adapt the standard notions of path, connection and spanning set of connections in the context of labels and constraints.

Denition 5 (Paths). Let A be an indexed formula. The set of paths in A is inductively dened as follows:

1. { a0 } is a path, where a0 is the root position.

2. If s is a path such that u ∈ s then

• if ptyp(u) ∈ { πα } then s\{ u } ∪ { [u]1, [u]2 } is a path, • if ptyp(u) ∈ { πβ } then s\{ u } ∪ { [u]1 } and s\{ u } ∪ { [u]2 } are paths2.

We say that a path s0 in A is obtained from a path s by reduction on the indexed position u if it results from s using the second clause of Denition 5. An atomic path is a path that only contains atomic indexed positions. Consequently an atomic path is non-reducible and is always a leaf of a path reduction tree. A conguration of A is a nite set of paths in A. Denition 6 (Reduction). A reduction of an indexed formula A is a nite sequence (Si)1≤i≤n of congurations in A such that Si+1 is obtained from Si by reduction of a position u in a path s of Si following Denition 5. We say that Si+1 is obtained by reduction of Si of u in s. A reduction (Si)1≤i≤n is said atomic if all the paths of Sn are atomic.

Denition 7

(Connection). Let A be an indexed formula, a connection c in A is: 1. a pair h u, v i of atomic positions such that f (u) = f (v), pol(u) = 1 and pol(v) = 0, or 2 Let us remark that the branching indicates non-determinism. 2. a pair h a0, v i such that f (v) = 1 and pol(v) = 0.

The rst case corresponds to an atomic axiom rule (ax) in LMILL, while the second one corresponds to the rule 1R. Let us also note that the rst position of a connection is the one with the positive polarity.

We denote Con the set of connections in A. The constraint kon(c) associated to a connection c = h u, v i is dened as kon(c) = slab(u) ≤ slab(v). For a 1-connection c = h a0, v i we have kon(h a0, v i) = ≤ slab(v) since slab(a0) = . In order to distinguish these constraints from the assertions and requirements they are called connection constraints . Moreover, the notions of upward and downward positions are extended to connections as follows: c ↑ = { u, v } ↑ and c ↓ = { u, v } ↓.

Denition 8 (MILL-cover) . Let A be an indexed formula, a connection c = h u, v i in A covers a path s in A, denoted c s, if v ∈ s and (u 6= a0 ⇒ u ∈ s). Let S be a set of paths in A, a cover of S is a set C = { (s, h u, v i) | s ∈ S and h u, v i ∈ Con and h u, v i s } such that (s, h u, v i) ∈ C and (s, h u0, v0 i) ∈ C ⇒ u = u0 and v = v0.

A cover of A is a cover of the set of atomic paths in A. 3.3.1

An Example (part 2) The reduction of the initial path { a0 } results in six atomic paths as depicted in Figure 4. At each step, we indicate the position which is reduced with an underscore. For conciseness, we write s and s0 as shortcuts for a2, a5, a7 and a2, a6, a7. The set C =

{ (s1, h a2, a10 i), (s2, h a12, a5 i), (s3, h a7, a14 i), (s4, h a2, a10 i), (s5, h a6, a13 i), (s6, h a7, a14 i) } covers all atomics paths. Indeed, h a2, a10 i covers paths s1 and s4, h a12, a5 i covers the path s2, h a7, a14 i covers the path s3 and s6, h a6, a13 i covers the path s5. We observe that connections h a2, a10 i and h a7, a14 i cover two atomic paths at the same time. 3.4

Characterizing MILL-Provability In this section we dene a connection-based characterization of MILL-provability which relies on the notions of substitution and certication.

Denition 9 (Substitution). Let A be an indexed formula. A substitution for A is an application σ : Σβ → Lα, that can be extended to labels and constraints as follows: • xσ = x if x is a constant or if x = , • (x ◦ y)σ = xσ ◦ yσ, • (x ≤ y)σ = xσ ≤ yσ.

Moreover a substitution σ for an indexed formula A induces an instantiation relation on indexed positions, denoted ≺, such that

(∀u, v ∈ Pos)(u ≺ v i v ∈ Pβ and (u ⊆ vσ or u˜ ⊆ vσ).

Denition 10 (Certication) . Let A be an indexed formula. A certication for A is an application γ : Pβ → ℘(Pα) that associates a set of πα-positions with any πβ -position in A.

A certication γ for an indexed formula A induces a deduction relation on indexed positions, denoted @, such that

An expression u @ v means that v is deduced from u (in A). The relations of domination, instantiation and deduction induce a reduction relation C= ( ∪ ≺ ∪ @)+ where (·)+ represents the transitive closure. An expression u C v means that u must be reduced before v (in A). Now we can express the provability conditions in terms of connections.

Denition 11 (Complementarity) . Let s be a path in an indexed formula A and σ be a substitution, a connection c in A is complementary in s under σ if c s and Kα(s ↑)σ |≈ kon(c)σ. A path s is complementary under σ if there exists a connection that is complementary in s under σ. A cover C of a set of paths in A is complementary under σ if (∀(s, c) ∈ C) c is complementary in s under σ.

Denition 12 (Provability). A formula A is provable if there exist a cover C of the set of atomic paths of A, a substitution σ and a certication γ for A such that: 1. the reduction relation C is irreexive, 2. ∀(s, h u, v i) ∈ C, ∀w ∈ Pβ (s ↑), wγ ⊆ Pα(s ↑), 3. ∀(s, h u, v i) ∈ C, ∀w ∈ Pβ (s ↑), k(wγ)σ |≈ k(w)σ, 4. ∀(s, h u, v i) ∈ C, ∀x ∈ Σβ (s ↑), xσ ∈ Lα(s ↑), 5. ∀(s, h u, v i) ∈ C, h u, v i is complementary in s under σ. (C1) (C2) (C3) (C4) (C5)

The rst condition induces the acyclicity of the graph associated to C and then the existence of a reduction (decomposition) order of the formula A that respects the precedence constraints between πα and πβ positions. The second and third conditions ensure that, in an atomic path s, every requirement introduced by a position of principal type πβ must be introduced before the two positions of the connection that makes the path s complementary and should be certied by assertions corresponding to positions of principal type πα that can be reduced before this requirement in a reduction from the initial path { a0 } to s. In a similar way the fourth condition means that each variable, introduced before reaching the connection that makes an atomic path complementary, is instantiated by a label composed from constants that can be reduced before this variable in a reduction from the initial path { a0 } to s. 3.4.1

An Example (part 3) The reduction path process from { a0 } provides the following atomic paths: s1 = { a2, a5, a7, a10 }, s2 = { a2, a5, a7, a12, a13 }, s3 = { a2, a5, a7, a14 }, s4 = { a2, a6, a7, a10 }, s5 = { a2, a6, a7, a12, a13 } and s6 = { a2, a6, a7, a14 }.

From the following cover C =

{ (s1, h a2, a10 i), (s2, h a12, a5 i), (s3, h a7, a14 i), (s4, h a2, a10 i), (s5, h a6, a13 i), (s6, h a7, a14 i) } we generate the set of constraints:

KC = { (s1, a1 ≤ a9), (s2, a11 ≤ a4), (s3, a˜3 ≤ a˜8), (s4, a˜1 ≤ a˜9), (s5, a˜4 ≤ a˜11)(s6, a˜3 ≤ a˜8) }.

Then we consider the substitution:

a9σ = a1, a4σ = a11, a˜8σ = a˜3, a˜4σ = a˜11, a8σ = X, a˜9σ = Y

Then we solve the following requirements:

1) a0 ≤ a˜0, a1a˜1 ≤ a0, a3a˜3 ≤ a˜1, Y a11 ≤ a˜11 |≈ a3a11 ≤ a˜11 2) a0 ≤ a˜0, a1a˜1 ≤ a0, a3a˜3 ≤ a˜1, Y a11 ≤ a˜11 |≈ Xa˜3 ≤ a˜0 3) a0 ≤ a˜0, a1a˜1 ≤ a0, a3a˜3 ≤ a˜1, Y a11 ≤ a˜11 |≈ a1Y ≤ X From 1) we directly deduce Y = a3 and also a4γ = { a11 }. The requirement in 1) is the one of the position a4 and in order to verify it we use the assertion a3a11 ≤ a˜11 of position a11. From 3) we deduce a trivial solution for X that is X = a1a3 and also that a9γ = ∅. Requirement 2) is veried because we have: a1 ≤ a1 a3a˜3 ≤ a˜1 a1a3a˜3 ≤ a1a˜1

F a1a3a˜3 ≤ a0 a1a˜1 ≤ a0

T a1a3a˜3 ≤ a˜0 a0 ≤ a˜0

T and then we deduce a8γ = { a0, a1, a3 } since a0 ≤ a˜0, a1a˜1 ≤ a0, a3a˜3 ≤ a˜1 are the respective assertions of a0, a1, a3.

In order to verify the conditions (C2) to (C5), let us consider the following table: (s, h u, v i)

Pβ({ u, v } ↑) Pα(s ↑) Σβ({ u, v } ↑) Σα(s ↑) (s1, h a2, a10 i) a8, a9 (s2, h a12, a5 i) a4, a8, a9 (s3, h a7, a14 i) a8, a9 (s4, h a2, a10 i) a8, a9 (s5, h a6, a13 i) a4, a8, a9 (s6, h a7, a14 i) a8, a9 a0, a1, a3 a8, a˜8, a9, a˜9 a0, a˜0, a1, a˜1, a3, a˜3 a0, a1, a3, a11 a4, a˜4, a8, a˜8, a9, a˜9 a˜0, a1, a˜1, a3, a˜3, a11, a˜11 a0, a1, a3 a8, a˜8 a0, a˜0, a1, a˜1, a3, a˜3 a0, a1, a3 a8, a˜8, a9, a˜9 a0, a˜0, a1, a˜1, a3, a˜3 a0, a1, a3, a11 a4, a˜4, a8, a˜8, a9, a˜9 a˜0, a1, a˜1, a3, a˜3, a11, a˜11 a0, a1, a3 a8, a˜8 a0, a˜0, a1, a˜1, a3, a˜3 We have a9γ = ∅ ⊆ Pα(s ↑) for all paths s ∈ { s1, s2, s4, s5, s6 } and a8γ = { a0, a1, a3 } ⊆ Pα(s ↑) for all paths s ∈ { s1 . . . s6 }. Moreover, for all paths s ∈ { s2, s5 }, a4γ = { a11 } ⊆ Pα(s ↑). Then the condition (C2) is veried. In addition, for all paths s ∈ { s1, s2, s4, s5 } we have a9σ = a1 ∈ Lα(s ↑) and a˜9σ = a3 ∈ Lα(s ↑) for all paths s ∈ { s1, s2, s3, s4, s5, s6 } we have a8σ = a1a3 ∈ Lα(s ↑) and a˜8σ = a˜3 ∈ Lα(s ↑), and for all paths s ∈ { s2, s5 } we have a4σ = a11 ∈ Lα(s ↑) and a˜4σ = a˜11 ∈ Lα(s ↑).

The last thing to do is to compute the reduction relation C that is obtained by the transitive closure of the domination relation , the instantiation relation @ and the deduction relation @. The instantiation relation induced by σ is and the deduction relation induced by γ is

The reduction relation C is represented in Figure 5. As the graph is acyclic, A is valid in MILL. a5 a2 a4 a1 a6 a3 a7

a10 a0 a12 a9 a11 a8 a13 a14

Properties of the Characterization In this section we prove the soundness and completeness of characterization given in Denition 12. The completeness is proved by showing that any formula provable in the LMILL sequent calculus is also provable according to the connection-based characterization (CMILL-provable). Denition 13 (Complete reduction) . Let A be an indexed formula and C be a cover of A, a reduction (Si)1≤i≤n in A is complete for C if C is a cover of Sn.

Denition 14 (Proper reduction) . Let A be an indexed formula and σ be a substitution for A, a reduction (Si)1≤i≤n is σ-proper i 1. ∀S ∈ (Si)1≤i≤n, ∀s ∈ S, Kα(s ↑)σ |≈ Kβ (s ↑)σ and 2. ∀S ∈ (Si)0≤i≤n, ∀s ∈ S, ∀x ∈ Σβ (s ↑), xσ ∈ Lα(s ↑).

Denition 15 (Realization). Let A be an indexed formula and s be a path in A. An interpretation of s in a resource model R = h (M, v, ·, e), |=, J K i is a function k k : Σα(s ↑) → M that can be extended to labels Lα(s ↑) with k k = e and kxyk = kxk · kyk.

Given a substitution σ for A, we denote k kσ the composed function k k ◦ σ from the set Lαβ (s ↑) of labels of s to the set of worlds M of R.

A realization of s is a couple (k k, σ) such that: 1. For all assertions x ≤ y ∈ Kα(s ↑), kxkσ v kykσ. 2. For all positions u ∈ s such that lsf (u) = A1 : x, kxkσ |= A.

3. For all positions u ∈ s such that lsf (u) = A0 : x, kxkσ 6|= A.

A path is realizable if there exists a realization of s in a model R. A conguration is realizable if at least one of its paths is realizable.

Lemma 1. Let s be a path in an indexed formula A, (k k, σ) be a realization of s in a model R = (M, e, ·, v, |=) and K ⊆ Kα(s ↑) a subset of assertions associated to s. If Kσ |≈ (x ≤ y)σ then kxkσ v kykσ.

Proof. By denition of a realization, for any assertion x0 ≤ y0 of K we have kx0kσ v ky0kσ. By hypothesis, under σ, the constraint x ≤ y is deduced (in the K-deduction system) from assertions of K by rules expressing reexivity and transitivity of ≤ and also compatibility of label composition with ≤. Moreover, by denition of a preorder, v is reexive and transitive and by denition of a MILL-model, world composition is compatible with v in R. Consequently, the rules of the K-deduction system transfer the notion of realizability from premisses to conclusion. Lemma 2. Let A be an indexed formula, σ be a substitution for A and (Si)1≤i≤n be a σ-proper reduction for A, if Si is σ-realizable then Si+1 is σ-realizable.

Proof. As the conguration Si is realizable under σ, it contains a path s that is realizable under σ in a model (M, e, ·, v, |=) for a interpretation k k. Let us suppose that Si+1 is obtained by a reduction of a position u in a path of S. If u 6∈ s then Si+1 remains realizable under σ because it always contains the path s. Otherwise, we proceed by case analysis depending on the principal connective of lsf (u) = Apol : x and show that Si+1 remains realizable under σ: • Case (B ∗ C)1 : x

The path s is reduced into s0 by replacing the position u by its children positions [u]1 and [u]2 such that lsf ([u]1) = B1 : u and lsf ([u]2) = C1 : u˜. Then Σα(s0 ↑) = Σα(s ↑)∪{ u, u˜ } and Kα(s0 ↑) = Kα(s ↑) ∪ { uu˜ ≤ x }. By hypothesis, k kσ is a realization of s and then kxkσ |= B ∗ C. Thus, by denition of |=, there exist two worlds m, n ∈ M such that m · n v kxkσ, m |= B and n |= C. We then extend k k to u and u˜ by dening kuk = m and ku˜k = n to obtain kukσ |= B, ku˜kσ |= C and kuu˜kσ = kukσ · ku˜kσ v kxkσ.

Consequently s0 is realizable under σ. • Case (B ∗ C)0 : x

The path is reduced into two paths s0 and s00 such that Σβ (s0 ↑) = Σβ (s ↑) ∪ { u }, Σβ (s00 ↑) = Σβ (s ↑) ∪ { u˜ } and Kβ (s0 ↑) = Kβ (s00 ↑) = Kβ (s ↑) ∪ { uu˜ ≤ x }. By hypothesis the reduction (Si)1≤i≤n is σ-proper and we have Kα(s0 ↑)σ |≈ Kβ (s0 ↑)σ and Kα(s00 ↑)σ |≈ Kβ (s00 ↑)σ. In particular Kα(s ↑) = Kα(s0 ↑) = Kα(s00 ↑), Kβ (s0 ↑) = Kβ (s00 ↑) and uu˜ ≤ x ∈ Kβ (s0 ↑) entail Kα(s ↑)σ |≈ (uu˜ ≤ x)σ. As k kσ is a realization of s, we have kxkσ 6|= B ∗ C and from Lemma 1 we deduce kukσ ·ku˜kσ v kxkσ. Then, by denition of |=, for all worlds m, n ∈ M such that m · n v kxkσ, we have either m 6|= B or n 6|= C. In particular, we have either kukσ 6|= B or ku˜kσ 6|= C. Consequently, either s0 is realizable under σ or s00 is realizable under σ.

• The other cases are similar.

Lemma 3. Let A be an indexed formula and σ be a substitution for A. If a path s is complementary under σ then it is not realizable under σ.

Proof. Let us suppose that s contains a connection h u, v i such that f (u) = f (v), pol(u) = 1, pol(v) = 0 and Kα(s ↑)σ |≈ slab(u)σ ≤ slab(v)σ. If s is realizable under σ for an interpretation k k in a model R then kslab(u)kσ |= f (u), kslab(v)kσ 6|= f (u) and kslab(u)kσ v kslab(v)kσ, which is contradictory because by Kripke monotonicity kslab(u)kσ v kslab(v)kσ and kslab(u)kσ |= f (u) entail kslab(v)kσ |= f (u). The case of a 1-connection is similar. Theorem 2 (Soundness). If a formula A is CMILL-provable then it is valid. Proof. As A is provable, there is a cover C of the set of atomic paths of A, a substitution σ and a certication γ for A satisfying the conditions of Denition 12.

Let us suppose that A is not valid. Then, there exists a model R = (M, e, ·, v, |=) such that e 6|= A. The initial conguration S1 = { { a0 } } is then trivially realizable under σ by considering the interpretation k k the domain of which is empty. It is easy to show that conditions (C1) to (C5) entail the existence of a reduction (Si)1≤i≤n from S1 that is complete for C, σ-proper and such that all paths of Sn contain at least a connection of C. As S1 is realizable under σ, Lemma 2 entails that the conguration Sn is also realizable under σ. But then, by Lemma 3, we deduce that Sn cannot be complementary, which is a contradiction. Therefore, A is valid.

Let us now consider the question of completeness of this characterization.

Theorem 3 (Completeness). If a formula A is valid then A is CMILL-provable. Proof. From the sound and completeness of MILL-models, it is sucient to prove that if A is LMILL-provable then A is CMILL-provable (provable by the connection characterization). The proof is by induction on a LMILL-proof of A, knowing that a sequent Γ ` A is provable in LMILL if and only if the formula ΦΓ −∗ A is provable in LMILL, where ΦΓ is the formula obtained by replacing each comma in the context Γ with multiplicative conjunction ∗. • Case ax: the axiom A ` A corresponds to the formula A −∗ A which is trivially CMILLprovable. • Case −∗R: By induction hypothesis we suppose that the sequent Γ , A ` B is provable and we show that the sequent Γ ` A −∗ B is also provable. If Γ, A ` B is CMILL-provable an atomic reduction R1 = (Si)1≤i≤n of ((ΦΓ ∗ A) −∗ B), a cover C of Sn, a substitution σ and a certication γ for A that satisfy the conditions of Denition 12.

From the atomic reduction R1 for ((ΦΓ ∗ A) −∗ B) we can build an atomic reduction R2 for (ΦΓ −∗ (A −∗ B)). On the left-hand side of the next gure, we describe the rst steps of the reduction R1 and, on the right-hand side, we describe the rst steps of the corresponding reduction R2. We represent here a path s as a set of signed formulae and not as a set of positions, namely we have lsf (s) = { lsf (u) | u ∈ s }.

{ ((ΦΓ ∗ A) −∗ B)0 : } { (ΦΓ ∗ A)1 : a0, B0 : a˜0 } { (ΦΓ −∗ (A −∗ B))0 : } { ΦΓ1 : a0, (A −∗ B)0 : a˜0 } { ΦΓ1 : a1, A1 : a˜1, B0 : a˜0 }

{ ΦΓ1 : a0, A1 : ai, B0 : a˜i } We observe that the rst reduction steps in R1 and R2 lead to paths containing the same signed formulae, modulo a renaming of a1 into a0, of a˜1 into ai and of a˜0 into a˜i. Consequently, modulo the renaming, we can reduce R2 by applying exactly the same reduction steps than for R1. Then, after the two rst steps previously described, R1 and R2 introduce the same signed formulae and then the same constraints (assertions and requirements) between labels, modulo renaming.

Moreover, the assertions { a0a˜0 ≤, a1a˜1 ≤ a˜0 } introduced in the two rst steps of R1 entail relations between labels a˜0, a1, a˜1 of R1 weaker than the ones between labels a0, ai, a˜i in Γ, x ≤ y, A : x ` A : y, Δ

Γ, ≤ x ` x : 1, Δ id 1R Γ, ≤ x ` Δ Γ, 1 : x ` Δ 1L Γ, ab ≤ x, A : a, B : b ` Δ Γ, A ∗ B : x ` Δ ∗L yz ≤ x, Γ ` A : y, Δ

yz ≤ x, Γ ` B : z, Δ Γ, yz ≤ x ` A ∗ B : x, Δ Γ, xy ≤ z ` A : y, Δ

Γ, xy ≤ z, B : z ` Δ Γ, xy ≤ z, A −∗ B : x ` Δ Γ, A : a, xa ≤ b ` B : b, Δ Γ ` A −∗ B : x, Δ ∗R −∗R Γ, x ≤ x ` Δ Γ ` Δ

R Γ, x ≤ z, x ≤ y, y ≤ z ` Δ Γ, x ≤ y, y ≤ z ` Δ Γ, xx0 ≤ yy0, x ≤ x0, y ≤ y0 ` Δ Γ, x ≤ y, x0 ≤ y0 ` Δ

F −∗L T

Side conditions:

In ∗L and −∗R, the constants a and b do not occur in the conclusion.

In R the label x must already occur in the conclusion. R2 by assertions { a0a˜0 ≤, a˜0ai ≤ a˜i } introduced in the two rst steps of R2. In fact, R1 imposes slab(ΦΓ)slab(A) ≤ slab(B) while R2 imposes slab(ΦΓ)slab(A) = slab(B). Consequently, as R1 leads to a set of atomic paths satisfying the conditions of Denition 12, it is the same for R2 by induction hypothesis. • Case ∗L: immediate by the translation Φ, because ΦΓ,A,B = ΦΓ,A∗B.

• The other cases are similar. 5

A Labelled Sequent Calculus for MILL From the previous characterization we can derive a sound and complete labelled sequent calculus GMILL3 for MILL. Soundness and completeness are easy consequences of Theorem 2 and Theorem 3.

Labels and constraints for GMILL are dened similarly as in Section 3.1 except that GMILL does not make use of variables. The sequent calculus GMILL deals with sequents of the form Γ ` Δ where Γ and Δ are multisets containing labelled formulas, Γ being allowed to also contain constraints. Labelled formulas are pairs (A, x), written A : x, where A is a formula and x is a label. Label constraints occurring in Γ are called assertions. We denote Γr the restriction of Γ to its constraints. GMILL does not have explicit requirements. Instead, the rules ∗R and −∗L are required to have a specic constraint (which in the connection-based characterization 3 The G in GMILL is reminiscent of the fact that labels and label-constraints can be viewed as a graphical structure we usually call a resource-graph in related works.

Π4 a1a3 ≤ a1a3, a3 ≤ a3, . . . , a1 ≤ a1, . . . , P : a1, Q −∗ R : a3, . . . ` . . . , P ∗ (Q −∗ R) : a1a3 a3 ≤ a3, . . . , a1 ≤ a1, . . . , P : a1, Q −∗ R : a3, . . . ` . . . , P ∗ (Q −∗ R) : a1a3

a1a3a˜3 ≤ a˜0, . . . , P : a1, Q −∗ R : a3, . . . ` . . . , P ∗ (Q −∗ R) : a1a3 Π3 Π4 Π1 Π2 a˜3 ≤ a˜3, . . . , S : a˜3 ` . . . , S : a˜3 a1a3a˜3 ≤ a˜0, a1a3a˜3 ≤ a1a˜1, a1 ≤ a1, a3a˜3 ≤ a˜1, a1a˜1 ≤ a˜0, a0 ≤ a˜0, . . . , S : a˜3 ` . . . , S : a˜3 Π1

Π2 a1a3a˜3 ≤ a˜0, . . . , P : a1, Q −∗ R : a3, S : a˜3 ` ((P ∗ (Q −∗ R)) ∗ S) : a˜0 a1a3a˜3 ≤ a1a˜1, . . . , a1a˜1 ≤ a˜0, . . . , P : a1, Q −∗ R : a3, S : a˜3 ` ((P ∗ (Q −∗ R)) ∗ S) : a˜0 a1 ≤ a1, a3a˜3 ≤ a˜1, . . . , P : a1, Q −∗ R : a3, S : a˜3 ` ((P ∗ (Q −∗ R)) ∗ S) : a˜0 a3a˜3 ≤ a˜1, a1a˜1 ≤ a˜0, a0 ≤ a˜0, P : a1, Q −∗ R : a3, S : a˜3 ` ((P ∗ (Q −∗ R)) ∗ S) : a˜0 a1a˜1 ≤ a˜0, a0 ≤ a˜0, P : a1, ((Q −∗ R) ∗ S) : a˜1 ` ((P ∗ (Q −∗ R)) ∗ S) : a˜0 a0 ≤ a˜0, (P ∗ ((Q −∗ R) ∗ S) : a0 ` ((P ∗ (Q −∗ R)) ∗ S) : a˜0

` (P ∗ ((Q −∗ R) ∗ S)) −∗ ((P ∗ (Q −∗ R)) ∗ S) : corresponds to a requirement) occuring in Γr for the rules to be applicable. The rules of the GMILL calculus are given in Figure 6.

From the proof of Theorem 3, one can derive a translation of LMILL-proofs into GMILLproofs so that for any LMILL-proof the corresponding GMILL-proof applies the same rules in the same order. Therefore, since LMILL does not allow contraction, GMILL has no need for it too. Moreover, conditions (C1) to (C5) given in Denition 12 imply that whenever ∗R and −∗L need to be applied in GMILL, Γr contains enough assertions to make the rule applicable. Therefore we have the following results.

Theorem 4. If a formula A has a proof in LMILL then it is has a proof in GMILL that follows the same rule application strategy.

Theorem 5. A formula A is provable in LMILL i it is provable in GMILL.

Figure 5 illustrates how GMILL works by giving an example of a derivation in the GMILL

R ∗R ∗R F

R T

F R calculus for the formula (P ∗ ((Q −∗ R) ∗ S)) −∗ ((P ∗ (Q −∗ R)) ∗ S), which is exactly the one prescribed by the reduction ordering we computed in the running example of Section 3.4. 6 From this connection-based characterization of validity in MILL we will consider dierent perspectives. First we aim at dening a connection method for MILL from such a characterization that mainly corresponds to the denition and implementation of an algorithm for solving our constraints. A complementary question consist in studying how our results can be adapted or rened to deal with other fragments of Intuitionistic Linear Logic and mainly rst-order ones including quantications.

The question of reconstruction of proofs in the MILL sequent calculus from our connection calculus for MILL with labels and constraints has also to be explored w.r.t. existing techniques [ 11 ]. Moreover, taking into account the relationships in MLL between some connection-based characterizations and proof-nets [ 1 ], we aim at studying similar relationships for MILL and propose new proof methods based on proof-net construction.

References

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

[2] 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 111128 , 2002 . Copenhagen, Danemark.

[3] D. Galmiche and D. MØry . A Connection-based Characterization of Bi-intuitionistic Validity . In 23rd Int. Conference on Automated Deduction, CADE-23, LNAI 6803 , pages 253267 , Wroclaw Poland , July 2011 .

[4] J.Y. Girard . Linear logic . Theoretical Computer Science , 50 ( 1 ): 1102 , 1987 .

[5] C. Kreitz and H. Mantel . A matrix characterization for multiplicative exponential linear logic . Journal of Automated Reasoning , 32 ( 2 ): 121166 , 2004 .

[6] C. Kreitz and J. Otten . Connection-based theorem proving in classical and non-classical logics . Journal of Universal Computer Science , 5 ( 3 ): 88112 , 1999 .

[7] P. W. O'Hearn and D. Pym . The Logic of Bunched Implications. Bulletin of Symbolic Logic , 5 ( 2 ): 215244 , 1999 .

[8] J. Otten . Mleancop: A connection prover for rst-order modal logic . In Int. Joint Conference on Automated Reasoning, IJCAR 2014, LNAI 8562 , pages 269276 , Vienna, Austria, 2014 .

[9] J. Otten and C. Kreitz . A connection based proof method for intuitionistic logic . In 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918 , pages 122137 , St Goar am Rhein, Germany , 1995 . Springer Verlag.

[10] J. Otten and C. Kreitz . T-string-unication: unifying prexes in non classical proof methods . In 5th Int. Workshop TABLEAUX'96, LNAI 1071 , pages 244260 , Terrasini , Palermo, Italy, 1996 . Springer Verlag.

[11] S. Schmitt and C. Kreitz . Converting non-classical matrix proofs into sequent-style systems . In 13th Int. Conference on Automated Deduction, LNAI 1104 , pages 418432 , New Brunswick, NJ, USA, 1996 .

[12] A. Urquhart . Semantics for Relevant Logic . Journal of Symbolic Logic , 37 : 159169 , 1972 .

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