=Paper=
{{Paper
|id=Vol-2095/paper3
|storemode=property
|title=Labelled Connection-based Proof Search for
Multiplicative Intuitionistic
|pdfUrl=https://ceur-ws.org/Vol-2095/paper3.pdf
|volume=Vol-2095
|authors=Didier Galmiche,Daniel Mery
|dblpUrl=https://dblp.org/rec/conf/cade/GalmicheM18
}}
==Labelled Connection-based Proof Search for
Multiplicative Intuitionistic==
https://ceur-ws.org/Vol-2095/paper3.pdf
Labelled Connection-based Proof Search for
Multiplicative Intuitionistic Linear Logic
Didier Galmiche and Daniel Méry
LORIA - Université de Lorraine
Campus Scienti que, BP 239
Vand÷uvre-lès-Nancy, France
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 brie y 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.
1 Introduction
In previous works we have developed connection-based characterizations of validity in non-
classical logics like the Logic of Bunched Implications (BI) [2] and Bi-intuitionistic logic [3].
They are based on speci c concepts like labels and constraints in order to capture the model
semantics and then the semantic interactions between connectives in such logics. It is an
alternative approach to the standard view of connection calculi for non-classical logics that are
based on the notion of pre xes. This notion allows one to capture the non-permutabilities of
the sequent calculi rules and has been developed and improved in the context of intuitionistic
logic [9, 10] but also of modal logics [8]. There exist connection-based characterizations and
related connection methods for multiplicative (commutative) linear logic (MLL) [1, 6] but, as
far as we know, not for multiplicative intuitionistic linear logic (MILL). The connection-based
characterization proposed for fragments of Linear Logic [4] like MLL or MELL is based on
particular pre xes and substitutions dedicated to these logics [6, 5]. In order to extend or adapt
it to MILL, it would be necessary to de ne and consider what could be called intuitionistic and
linear pre xes, which could be di cult to deal with.
Our approach consists in specializing our above-mentioned results for BI to the Multiplica-
tive Intuitionistic Linear Logic (MILL) and then de ne and illustrate a connection-based char-
acterization of provability for MILL that deals with speci c labels and constraints. Then we
generate semantic structures from MILL's Urquhart's semantics [12] and develop a characteri-
zation of provability from labels and constraints that capture this semantics. It could be seen as
a generalization of the pre xes more appropriate to connection-based proof search in resource
logics like BI logic or Linear Logic. Since BI is conservative over MILL [7], a connection-based
characterization for MILL can be obtained, by restriction of the previous characterization for
BI, to the multiplicative connectives. In this case, we have to take into account the notion of
multiplicity and also global conditions on the paths. The characterization for MILL proposed
here does not deal with multiplicity and only considers local conditions on the paths. In ad-
dition we de ne a labelled sequent calculus for MILL, called GMILL and prove its soundness
and also its completeness by translation of MILL proofs to GMILL proofs.
ARQNL 2018 49 CEUR-WS.org/Vol-2095
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
Γ`C
ax 1L 1R
A`A Γ, 1 ` C `1
Γ, A, B, ∆ ` C Γ`A ∆`B
∗L ∗R
Γ, A ∗ B, ∆ ` C Γ, ∆ ` A ∗ B
Γ ` A ∆, B ` C Γ, A ` B
−∗L −∗R
Γ, A −∗ B, ∆ ` C Γ ` A −∗ B
Figure 1: Sequent Calculus for MILL
2 Multiplicative Intuitionistic Linear Logic
The propositional language of MILL consists of a denumerable set L = P, Q, . . . of proposi-
tional 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 de nition:
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 LMILL1 , is given in Figure 1. One
di culty with such a calculus lies in the fact that the rules for left-implication and right-
conjunction both require context splitting from conclusion to premises. Making relevant choices
when context-splitting is required is crucial for the e ciency 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 brie y.
De nition 1 (MILL-frame). A MILL-frame is a partially ordered commutative monoid M =
h M, ·, e, v i, in which M is a set of worlds and v is compatible with ·, i.e.:
∀m∀n ∈ M. if m v n and m0 v n0 then m · m0 v n · n0 .
De nition 2 (MILL-interpretation). A MILL-intepretation is a function J−K : L → P(M )
that satis es Kripke monotonicity, i.e.:
∀m, n ∈ M. if m v n and m ∈ JPK then n ∈ JPK.
De nition 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.
2 50
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
• 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.
De nition 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 for-
mulas { 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 de ne 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 pre x-based approach does for IL or MLL
[5, 6, 13]. We already successfully used a similar approach for BI [2], and since BI is conser-
vative 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 re nement 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 e cient 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 e cient 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 de ned as
the set C extended with the unit symbol . We then de ne 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≤z z≤y x≤y x0 ≤ y 0
R T F
x≤x x≤y xx0 ≤ yy 0
The R and T rules formalize the re exivity 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 .
51 3
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
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 identi es 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 sec-
ondary type styp(u). Therefore, we have dierent principal types depending on the connective
and the associated polarity. We de ne 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 de ne constraints in order to capture context-
splitting. The labelled signed formula lsf (u) of a position u is a triple (slab(u), f (u), pol(u))
pol(u)
and is denoted f (u) : slab(u). The construction of an indexed formula tree is obtained by
inductively applying the rules described in Figure 2.
lsf (u) ptyp(u) kon(u) lsf (u1 ) lsf (u2 )
0
(A −∗ B) : x πα xu ≤ ũ A1 : u B0 : ũ
1
(A ∗ B) : x πα u ũ ≤ x A1 : u B1 : ũ
1
(A −∗ B) : x πβ xu ≤ ũ A0 : u B1 : ũ
0
(A ∗ B) : x πβ u ũ ≤ x A0 : u B0 : ũ
Figure 2: Signed formulae for MILL
For a given formula A the root position a0 has a polarity pol(a0 ) = 0, a label slab(a0 ) =
0
and the signed formula (A) : 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) =
4 52
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
Q0 : a4 R1 : ã4 Q1 : a11 R0 : ã11 a5 a6 a12 a13
−∗1 : a3 S1 : ã3 P0 : a9 −∗0 : ã9 a4 a7 a10 a11
P1 : a1 ∗1 : ã1 ∗0 : a8 S0 : ã8 a2 a3 a9 a14
∗1 : a0 ∗0 : ã0 a1 a8
−∗0 : a0
u pol(u) f (u) ptyp(u) styp(u) slab(u) kon(u)
a0 0 (P ∗ ((Q −∗ R) ∗ S)) −∗ ((P ∗ (Q −∗ R)) ∗ S) πα − a0 ≤ ã0
a1 1 P ∗ ((Q −∗ R) ∗ S) πα πα1 a0 a1 ã1 ≤ a0
a2 1 P − πα1 a1 −
a3 1 (Q −∗ R) ∗ S πα πα2 ã1 a3 ã3 ≤ ã1
a4 1 Q −∗ R πβ πα1 a3 a3 a4 ≤ ã4
a5 0 Q − πβ 1 a4 −
a6 1 R − πβ 2 ã4 −
a7 1 S − πα2 ã3 −
a8 0 (P ∗ (Q −∗ R)) ∗ S πβ πα2 ã0 a8 ã8 ≤ ã0
a9 0 P ∗ (Q −∗ R) πβ πβ 1 a8 a9 ã9 ≤ a8
a10 0 P − πβ 1 a9 −
a11 0 Q −∗ R πα πβ 2 ã9 ã9 a11 ≤ ã11
a12 1 Q − πα1 a11 −
a13 0 R − πα2 ã11 −
a14 0 S − πβ 2 ã8 −
Figure 3: Indexed formula tree of (P ∗ ((Q −∗ R) ∗ S)) −∗ ((P ∗ (Q −∗ R)) ∗ S)
{ kon(u) | u ∈ Pβ (p) } respectively. The associated sets of constants and variables are then
de ned as Σα (p) = { x | x occurs in Kα (p) } and Σβ (p) = { x | x occurs in Kβ (p) }. We set
Σαβ (p) = Σα (p)∪Σβ (p) and de ne 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 identi ed with a position (see the tree at the righthand
side of Figure 3). Moreover, we can associate an indexed formula tree (with labelled signed
0
formulae as nodes), inductively built from (A) : 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 ≤ ã0 , a1 ã1 ≤ a0 , a3 ã3 ≤ ã1 , ã9 a11 ≤ ã11 }
Kβ = { a8 ã8 ≤ ã0 , a9 ã9 ≤ a8 , a3 a4 ≤ ã4 }
53 5
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
{ a0 }
{ a1 , a8 }
{ a2 , a3 , a8 }
{ a2 , a4 , a7 , a8 }
{ a2 , a5 , a7 , a8 } { a2 , a6 , a7 , a8 }
{ s, a9 } { s, a14 } { s0 , a 9 } { s0 , a14 }
{ s, a10 } { s, a11 } { s0 , a10 } { s0 , a11 }
{ s, a12 , a13 } { s0 , a12 , a13 }
Figure 4: Path reduction with s = a2 , a5 , a7 and s0 = a2 , a6 , a7
The constants and variables are
Σα = { a0 , ã0 , a1 , ã1 , a3 , ã3 , a11 , ã11 } Σβ = { a4 , ã4 , a8 , ã8 , a9 , ã9 }.
3.3 Paths and Connections
In this section, we adapt the standard notions of path, connection and spanning set of connec-
tions in the context of labels and constraints.
De nition 5 (Paths). Let A be an indexed formula. The set of paths in A is inductively
de ned 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 De nition 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 con guration of A is a nite set of paths in A.
De nition 6 (Reduction). A reduction of an indexed formula A is a nite sequence (Si )1≤i≤n
of con gurations in A such that Si+1 is obtained from Si by reduction of a position u in a path
s of Si following De nition 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.
De nition 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.
6 54
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
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 cor-
responds 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 de ned 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 } ↓.
De nition 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 , v 0 i) ∈ C ⇒ u = u0 and v = v 0 .
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 de ne a connection-based characterization of MILL-provability which relies
on the notions of substitution and certi cation.
De nition 9 (Substitution). Let A be an indexed formula. A substitution for A is an appli-
cation σ : Σβ → 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 ũ ⊆ vσ).
De nition 10 (Certi cation). Let A be an indexed formula. A certi cation for A is an appli-
cation γ : Pβ → ℘(Pα ) that associates a set of πα -positions with any πβ -position in A.
55 7
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
A certi cation γ for an indexed formula A induces a deduction relation on indexed positions,
denoted @, such that
(∀u, v ∈ Pos)(u @ v i v ∈ Pβ and u ∈ vγ).
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 (·)+ repre-
sents 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.
De nition 11 (Complementarity). Let s be a path in an indexed formula A and σ be a sub-
stitution, 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 σ .
De nition 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 certi cation γ for A such that:
1. the reduction relation C is irre exive, (C1)
2. ∀(s, h u, v i) ∈ C, ∀w ∈ Pβ (s ↑), wγ ⊆ Pα (s ↑), (C2)
3. ∀(s, h u, v i) ∈ C, ∀w ∈ Pβ (s ↑), k(wγ)σ |≈ k(w)σ , (C3)
4. ∀(s, h u, v i) ∈ C, ∀x ∈ Σβ (s ↑), xσ ∈ Lα (s ↑), (C4)
5. ∀(s, h u, v i) ∈ C, h u, v i is complementary in s under σ . (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 certi ed
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 , ã3 ≤ ã8 ), (s4 , ã1 ≤ ã9 ), (s5 , ã4 ≤ ã11 )(s6 , ã3 ≤ ã8 ) }.
8 56
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
Then we consider the substitution:
a9 σ = a1 , a4 σ = a11 , ã8 σ = ã3 , ã4 σ = ã11 , a8 σ = X, ã9 σ = Y
Then we solve the following requirements:
1) a0 ≤ ã0 , a1 ã1 ≤ a0 , a3 ã3 ≤ ã1 , Y a11 ≤ ã11 |≈ a3 a11 ≤ ã11
2) a0 ≤ ã0 , a1 ã1 ≤ a0 , a3 ã3 ≤ ã1 , Y a11 ≤ ã11 |≈ Xã3 ≤ ã0
3) a0 ≤ ã0 , a1 ã1 ≤ a0 , a3 ã3 ≤ ã1 , Y a11 ≤ ã11 |≈ a1 Y ≤ 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 a3 a11 ≤ ã11 of position a11 . From
3) we deduce a trivial solution for X that is X = a1 a3 and also that a9 γ = ∅. Requirement 2)
is veri ed because we have:
a1 ≤ a1 a3 ã3 ≤ ã1
F
a1 a3 ã3 ≤ a1 ã1 a1 ã1 ≤ a0
T
a1 a3 ã3 ≤ a0 a0 ≤ ã0
T
a1 a3 ã3 ≤ ã0
and then we deduce a8 γ = { a0 , a1 , a3 } since a0 ≤ ã0 , a1 ã1 ≤ a0 , a3 ã3 ≤ ã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 a0 , a1 , a3 a8 , ã8 , a9 , ã9 a0 , ã0 , a1 , ã1 , a3 , ã3
(s2 , h a12 , a5 i) a4 , a8 , a9 a0 , a1 , a3 , a11 a4 , ã4 , a8 , ã8 , a9 , ã9 ã0 , a1 , ã1 , a3 , ã3 , a11 , ã11
(s3 , h a7 , a14 i) a8 , a9 a0 , a1 , a3 a8 , ã8 a0 , ã0 , a1 , ã1 , a3 , ã3
(s4 , h a2 , a10 i) a8 , a9 a0 , a1 , a3 a8 , ã8 , a9 , ã9 a0 , ã0 , a1 , ã1 , a3 , ã3
(s5 , h a6 , a13 i) a4 , a8 , a9 a0 , a1 , a3 , a11 a4 , ã4 , a8 , ã8 , a9 , ã9 ã0 , a1 , ã1 , a3 , ã3 , a11 , ã11
(s6 , h a7 , a14 i) a8 , a9 a0 , a1 , a3 a8 , ã8 a0 , ã0 , a1 , ã1 , a3 , ã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 veri ed. In addition, for all paths s ∈ { s1 , s2 , s4 , s5 } we have
a9 σ = a1 ∈ Lα (s ↑) and ã9 σ = a3 ∈ Lα (s ↑) for all paths s ∈ { s1 , s2 , s3 , s4 , s5 , s6 } we have
a8 σ = a1 a3 ∈ Lα (s ↑) and ã8 σ = ã3 ∈ Lα (s ↑), and for all paths s ∈ { s2 , s5 } we have
a4 σ = a11 ∈ Lα (s ↑) and ã4 σ = ã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
a1 @ a9 , a3 @ a9 , a1 @ a8 , a11 @ a4
and the deduction relation induced by γ is
a0 @ a8 , a1 @ a8 , a3 @ a8 , a11 @ a4 .
The reduction relation C is represented in Figure 5. As the graph is acyclic, A is valid in MILL.
57 9
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
a5 a6 a12 a13
a4 a7 a10 a11
a2 a3 a9 a14
a1 a8
a0
Figure 5: Reduction order for (P ∗ ((Q −∗ R) ∗ S) −∗ ((P ∗ (Q −∗ R)) ∗ S)
4 Properties of the Characterization
In this section we prove the soundness and completeness of characterization given in De ni-
tion 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).
De nition 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 .
De nition 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 ↑).
De nition 15 (Realization). Let A be an indexed formula and s be a path in A. An inter-
pretation 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 kk = 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 con guration 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 de nition of a realization, for any assertion x0 ≤ y 0 of K we have kx0 kσ v ky 0 kσ .
By hypothesis, under σ , the constraint x ≤ y is deduced (in the K-deduction system) from
10 58
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
assertions of K by rules expressing re exivity and transitivity of ≤ and also compatibility of
label composition with ≤. Moreover, by de nition of a preorder, v is re exive and transitive and
by de nition 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 con guration 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 σ :
1
• Case (B ∗ C) : 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 : ũ . Then Σα (s0 ↑) = Σα (s ↑)∪{ u, ũ }
and Kα (s0 ↑) = Kα (s ↑) ∪ { u ũ ≤ x }. By hypothesis, k kσ is a realization of s and
then kxkσ |= B ∗ C. Thus, by de nition 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 ũ by de ning
kuk = m and kũk = n to obtain kukσ |= B, kũkσ |= C and ku ũkσ = kukσ · kũkσ v kxkσ .
Consequently s0 is realizable under σ .
0
• Case (B ∗ C) : x
The path is reduced into two paths s0 and s00 such that Σβ (s0 ↑) = Σβ (s ↑) ∪ { u },
Σβ (s00 ↑) = Σβ (s ↑) ∪ { ũ } and Kβ (s0 ↑) = Kβ (s00 ↑) = Kβ (s ↑) ∪ { u ũ ≤ x }. By hy-
pothesis 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 u ũ ≤ x ∈ Kβ (s0 ↑) entail Kα (s ↑)σ |≈ (u ũ ≤ x)σ . As k kσ is a realization of s, we
have kxkσ 6|= B ∗ C and from Lemma 1 we deduce kukσ ·kũkσ v kxkσ . Then, by de nition
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 kũ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 comple-
mentary 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 inter-
pretation 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.
59 11
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
Proof. As A is provable, there is a cover C of the set of atomic paths of A, a substitution σ
and a certi cation γ for A satisfying the conditions of De nition 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 con guration 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 con guration 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 su cient 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 CMILL-
provable.
• 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 certi cation γ for A that satisfy the conditions of De nition 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 −∗ B))0 : }
{ (ΦΓ ∗ A)1 : a0 , B0 : ã0 } { ΦΓ 1 : a0 , (A −∗ B)0 : ã0 }
{ ΦΓ 1 : a1 , A1 : ã1 , B0 : ã0 } { ΦΓ 1 : a0 , A1 : ai , B0 : ãi }
.. ..
. .
R1 R2
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 ã1 into ai and of ã0 into ã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 { a0 ã0 ≤, a1 ã1 ≤ ã0 } introduced in the two rst steps of R1 entail
relations between labels ã0 , a1 , ã1 of R1 weaker than the ones between labels a0 , ai , ãi in
12 60
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
Γ, ≤ x ` ∆
id 1R 1L
Γ, x ≤ y, A : x ` A : y, ∆ Γ, ≤ x ` x : 1, ∆ Γ, 1 : x ` ∆
Γ, ab ≤ x, A : a, B : b ` ∆ yz ≤ x, Γ ` A : y, ∆ yz ≤ x, Γ ` B : z, ∆
∗L ∗R
Γ, A ∗ B : x ` ∆ Γ, yz ≤ x ` A ∗ B : x, ∆
Γ, xy ≤ z ` A : y, ∆ Γ, xy ≤ z, B : z ` ∆ Γ, A : a, xa ≤ b ` B : b, ∆
−∗L −∗R
Γ, xy ≤ z, A −∗ B : x ` ∆ Γ ` A −∗ B : x, ∆
Γ, x ≤ x ` ∆ Γ, x ≤ z, x ≤ y, y ≤ z ` ∆ Γ, xx0 ≤ yy 0 , x ≤ x0 , y ≤ y 0 ` ∆
R T F
Γ`∆ Γ, x ≤ y, y ≤ z ` ∆ Γ, x ≤ y, x0 ≤ y 0 ` ∆
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.
Figure 6: Labelled Sequent Calculus GMILL
R2 by assertions { a0 ã0 ≤, ã0 ai ≤ ã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 De nition
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 de ned 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 speci c 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.
61 13
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
. . . , a1 ≤ a1 , . . . , P : a1 , . . . ` . . . , P : a1
Π3
. . . , a3 ≤ a3 , . . . , Q −∗ R : a3 , . . . ` . . . , Q −∗ R : a3
Π4
Π3 Π4
∗R
a1 a3 ≤ a1 a3 , a3 ≤ a3 , . . . , a1 ≤ a1 , . . . , P : a1 , Q −∗ R : a3 , . . . ` . . . , P ∗ (Q −∗ R) : a1 a3
F
a3 ≤ a3 , . . . , a1 ≤ a1 , . . . , P : a1 , Q −∗ R : a3 , . . . ` . . . , P ∗ (Q −∗ R) : a1 a3
R
a1 a3 ã3 ≤ ã0 , . . . , P : a1 , Q −∗ R : a3 , . . . ` . . . , P ∗ (Q −∗ R) : a1 a3
Π1
ã3 ≤ ã3 , . . . , S : ã3 ` . . . , S : ã3
R
a1 a3 ã3 ≤ ã0 , a1 a3 ã3 ≤ a1 ã1 , a1 ≤ a1 , a3 ã3 ≤ ã1 , a1 ã1 ≤ ã0 , a0 ≤ ã0 , . . . , S : ã3 ` . . . , S : ã3
Π2
Π1 Π2
∗R
a1 a3 ã3 ≤ ã0 , . . . , P : a1 , Q −∗ R : a3 , S : ã3 ` ((P ∗ (Q −∗ R)) ∗ S) : ã0
T
a1 a3 ã3 ≤ a1 ã1 , . . . , a1 ã1 ≤ ã0 , . . . , P : a1 , Q −∗ R : a3 , S : ã3 ` ((P ∗ (Q −∗ R)) ∗ S) : ã0
F
a1 ≤ a1 , a3 ã3 ≤ ã1 , . . . , P : a1 , Q −∗ R : a3 , S : ã3 ` ((P ∗ (Q −∗ R)) ∗ S) : ã0
R
a3 ã3 ≤ ã1 , a1 ã1 ≤ ã0 , a0 ≤ ã0 , P : a1 , Q −∗ R : a3 , S : ã3 ` ((P ∗ (Q −∗ R)) ∗ S) : ã0
a1 ã1 ≤ ã0 , a0 ≤ ã0 , P : a1 , ((Q −∗ R) ∗ S) : ã1 ` ((P ∗ (Q −∗ R)) ∗ S) : ã0
a0 ≤ ã0 , (P ∗ ((Q −∗ R) ∗ S) : a0 ` ((P ∗ (Q −∗ R)) ∗ S) : ã0
` (P ∗ ((Q −∗ R) ∗ S)) −∗ ((P ∗ (Q −∗ R)) ∗ S) :
Figure 7: GMILL-proof of (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 GMILL-
proofs 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 De nition 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
14 62
Labelled Connection-based Proof Search for MILL Didier Galmiche and Daniel Méry
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 Future Work
From this connection-based characterization of validity in MILL we will consider dierent per-
spectives. First we aim at de ning a connection method for MILL from such a characterization
that mainly corresponds to the de nition and implementation of an algorithm for solving our
constraints. A complementary question consist in studying how our results can be adapted or
re ned to deal with other fragments of Intuitionistic Linear Logic and mainly rst-order ones
including quanti cations.
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-uni cation: unifying pre xes 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.
63 15