Connection-Based Proof Construction in Linear Logic

C. Kreitz^{1} H. Mantel^{2} J. Otten^{3} S. Schmitt^{3}

1 Department of Computer Science, Cornell University Ithaca, NY 14853, USA

                                     kreitz@cs.cornell.edu

2 Deutsches Forschungszentrum für Künstliche Intelligenz GmbH Stuhlsatzenhausweg 3, 66123 Saarbrücken, Germany

                                     mantel@dfki.uni-sb.de

3 Fachgebiet Intellektik, Fachbereich Informatik, Technische Hochschule Darmstadt Alexanderstr. 10, 64283 Darmstadt, Germany

                    {jeotten,steph}@intellektik.informatik.th-darmstadt.de

Abstract. We present a matrix characterization of logical validity in the multiplicative fragment of linear logic. On this basis we develop a matrix-based proof search procedure for this fragment and a procedure which translates the machine-found proofs back into the usual sequent calculus for linear logic. Both procedures are straightforward extensions of methods which originally were developed for a uniform treatment of classical, intuitionistic and modal logics. They can be extended to further fragments of linear logic once a matrix characterization has been found.

1 Introduction

Linear logic [12] is often viewed as the most adequate formalism for reasoning about action and change in real world applications. Formulas can be considered as resources which disappear after their use unless they are explicitly marked as reusable. No frame axioms about the environment [18] need to be stated and one only has to deal with axioms about those objects which are involved in the action. Proof search in linear logic will therefore have many useful applications such as resource sensitive logic programming [14], modeling concurrent computation by petri nets [11], and planning [17].

Because of the expressivity of logic, however, reasoning in linear logic is difficult to automate. Propositional linear logic is already undecidable. In order to prove a linear logic formula syntactically one has to rely on either sequent calculi or proof nets [12, 6], a kind of natural deduction system with multiple conclusions. The former cover all of linear logic but are not useful for efficient proof search because of the many redundancies contained in them. Attempts to remove permutabilities from sequent proofs [1, 10] and to add proof strategies [26] have provided some improvements but the main difficulties still remain. Proof nets, on the other hand, are applicable only to a small fragment of the logic. In order to handle the other parts one has to introduce the concept of boxes [12] which again cause major problems for automated proof search. Although there has been progress in removing some boxes [13] efficient proof search for full linear logic appears to be beyond the scope of proof nets at this point of time.

In classical and many non-classical logics matrix characterizations of logical validity have successfully been used as foundation for efficient proof search methods. They yield a very compact representation of the search space and thus avoid many kinds of redundancies which usually occur in the sequent calculus and tableaux proof search methods. Originally developed as foundation of Bibel’s connection method for classical logic [2, 4] they have later been extended to nonclassical logics by Wallen [27]. Wallen’s formulation serves as a basis of a uniform proof method for a rich variety of logics [19, 21] and also allows to transform matrix proofs into sequent-style proofs by a uniform procedure [23, 24].

By Wallen‘s conjecture [27] matrix methods can be developed for any logic which has the same primary properties as classical logic. The linear connection method [3] has demonstrated that matrix methods can be resource sensitive. A desire for a matrix characterization of linear logic has already been expressed in [9]. Because of a superficial similarity between matrix characterizations and proof nets it is very likely that this can be achieved at least for those fragments which can be handled by proof nets. On the other hand, as far as proof search is concerned, matrix methods have proven to be a more general approach which does not underly the limitations of proof nets and may therefore apply to a larger fragment of linear logic. Therefore it is reasonable to develop matrix characterizations for various fragments of linear logic and to extend both the uniform proof method and the transformation procedure accordingly. The resulting combined procedure will then be able to efficiently search for a matrix proof of a linear logic formula and to present it in the more convenient sequent calculus.

In this paper we begin this work by investigating the multiplicative fragment of linear logic (MLL). We shall develop a matrix characterization of logical validity in MLL whose formulation is close to Wallen’s characterization of validity in modal logics [27] and prove it to be correct and complete (Section 2). On this basis we shall extend our uniform proof method into one that generates matrix proofs for MLL (Section 3) and our uniform transformation procedure into one that converts the matrix proof back into a sequent proof (Section 4). Finally we shall discuss other recent approaches to reasoning within fragments of linear logic, current and future work, and evidence which makes us confident that extensions of our methods to larger parts of linear logic are possible.

2 A Matrix Characterization of Logical Validity in MLL

Linear Logic [12] is a resource sensitive logic. From a proof theoretical point of view it can be seen as the outcome of removing the rules for contraction and weakening from classical sequent calculus and re-introducing them in a controlled manner. Linear negation ^{⊥} is involutive like classical negation. The two different traditions for writing the sequent rule for classical conjunction result in two different conjunctions ⊗ and & and, due to the involutive negation, in two different disjunctions ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and ⊕. The constant true splits up into 1 and ⊤ for the same reason and false splits up into ⊥ and 0. The unary connectives ? and ! allow a controlled application of weakening and contraction. Quantifiers ∀ and ∃ can be added like in classical logic.

Linear logic connectives can be divided into the multiplicative, additive, and exponential fragment. While in the multiplicative fragment resources (i.e. formulas) are used exactly once, resource sharing is enforced in the additive fragment. By means of the exponentials formulas are marked as being reusable. All fragments can be combined freely and exist on their own right. However, the full power of linear logic comes from combining all of them.

The multiplicative fragment MLL can be seen as the core of linear logic. ⊥, ⊗, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , −∘, 1, and ⊥ are the connectives of this fragment. Linear negation ^{⊥} expresses the difference between resources which are to be used up and resources which are to be produced. Having a resource G^{⊥} means that a resource G must be produced. Having a resource F_{1}⊗F_{2} is having F_{1} as well as F_{2}. A resource F_{1} −∘F_{2} allows the construction of F_{2} from F_{1}. The meaning of a resource F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2} is explained best by its equivalence to F_{1}^{⊥} −∘F_{2} and to F_{2}^{⊥} −∘F_{1}. Having a resource 1 has no impact while nothing can be constructed when ⊥ is used up.

Validity of a linear logic formula can be proved syntactically by using a sequent calculus. For multi-sets Γ and Δ of formulas Γ ⊢ Δ is called a sequent. It can be understood as the specification of a transformation where Δ is constructed from Γ. All formulas in Γ are connected implicitly by ⊗ while all formulas in Δ are connected implicitly by ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} . There is a close relation between ⊢ and linear implication −∘. Thus, sequents clearly lie in the multiplicative realm.

The sequent calculus Lin_{M} for the multiplicative fragment without constants is depicted in Figure 1. In a rule the sequents above the line are called premises. The one below is the conclusion. A principal formula is a formula which occurs in the conclusion but not in any premise. Formulas which occur in a premise but not in the conclusion are called active. All other formulas are the context.

\underline{identity}  \underline{negation}
A ⊢ A axiom  {Γ ⊢ Δ, G \atop Γ, G^{⊥} ⊢ Δ} ^{⊥}l {Γ, F ⊢ Δ \atop Γ ⊢ Δ, F^{⊥}} ^{⊥}r

multiplicative fragment

{Γ, F_{1}, F_{2} ⊢ Δ \atop Γ, F_{1}⊗F_{2} ⊢ Δ} ⊗l  \begin{matrix}Γ_{1} ⊢ Δ_{1}, G_{1} & Γ_{2} ⊢ Δ_{2}, G_{2} \\ Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}, G_{1}⊗G_{2} \end{matrix} ⊗r

\begin{matrix}Γ_{1}, F_{1} ⊢ Δ_{1} & Γ_{2}, F_{2} ⊢ Δ_{2} \\ Γ_{1}, Γ_{2}, F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2} ⊢ Δ_{1}, Δ_{2} \end{matrix} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} l  {Γ ⊢ Δ, G_{1}, G_{2} \atop Γ ⊢ Δ, G_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{2}} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r

\begin{matrix}Γ_{1} ⊢ Δ_{1}, G_{1} & Γ_{2}, F_{1} ⊢ Δ_{2} \\ Γ_{1}, Γ_{2}, G_{1} −∘ F_{1} ⊢ Δ_{1}, Δ_{2} \end{matrix} −∘ l  {Γ, F_{1} ⊢ Δ, G_{1} \atop Γ ⊢ Δ, F_{1} −∘ G_{1}} −∘ r

Fig. 1. The sequent calculus Lin_{M} for MLL

In analytic proof search one starts out with the sequent to be proven and reduces sequents by application of rules until the axiom-rule can be applied. There are several choice points within this process. First, a principal formula in the sequent must be chosen. Due to the restriction to the multiplicative fragment this choice already implies the choice of the rule by which the formula shall be reduced. Second, when applying ⊗r, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} l, or −∘l the context of the sequent must be partitioned onto the premises. This is called context splitting. Several solutions have been proposed in order to optimize these choices.

Resource management systems have been proposed in [5] as efficient techniques for splitting contexts. If subsequent applications of two rules have no impact on each other their order is unimportant. In proof search it suffices just to consider one possible order. This phenomenon is called permutability of rules and has been investigated for linear logic in [1, 10, 26]. As solutions to fix an order for such rules the focusing principle [1], normal proofs [10], and proof search strategies [26] have been proposed. Though being improvements compared to simple sequent calculus proof search all these proposals suffer from that they are still connective oriented. During proof search the state of a proof under construction needs to be stored at every choice point in order to make backtracking in case of a later failure possible. This causes major notational redundancies.

Matrix proof methods avoid these redundancies which results in an improved efficiency compared to sequent based proof search. They are built on notions of polarities, position trees, prefixes, paths, connections, and substitutions.

Polarities, Types, Position–trees, and Prefixes. A signed formula ⟨F, k⟩ relates a formula F to a polarity k ∈ {0, 1}. The components of a signed formula consist of an immediate sub-formula of F and a polarity as depicted in Table 1. The polarity indicates whether the number of explicit and implicit negations during the above decomposition is even (polarity 0) or odd (polarity 1). In a derivation of a signed formula ⟨F, 0⟩ a sub-formula ⟨F′, k′⟩ occurs in the succedent of sequents only for k′ = 0, and for k′ = 1 in the antecedent only. Signed formulas are classified by (principal) types (α, β, o). In the case of negation we decided to deviate from the usual tableaux scheme for reasons which will become clear later on. Since each component of a signed formula ⟨F, k⟩ contains an immediate sub-formula F′ of F a relation ≻ such that F′ ≻ F is induced. The transitive closure of ≻ shall be an ordering ≫. As usual, the formula tree of F is a graph with all sub-formulas of F as nodes and edges indicating ≻.

\begin{matrix}α & ⟨G_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} G_{2}, 0⟩ & ⟨F_{1}⊗F_{2}, 1⟩ & ⟨F_{1} −∘ G_{1}, 0⟩ \\ b_{1} & ⟨G_{1}, 0⟩ & ⟨F_{1}, 1⟩ & ⟨F_{1}, 1⟩ \\ b_{2} & ⟨G_{2}, 0⟩ & ⟨F_{2}, 1⟩ & ⟨G_{1}, 0⟩ \end{matrix} \begin{matrix}β & ⟨F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2}, 1⟩ & ⟨G_{1}⊗G_{2}, 0⟩ & ⟨G_{1} −∘ F_{1}, 1⟩ \\ b_{1} & ⟨F_{1}, 1⟩ & ⟨G_{1}, 0⟩ & ⟨G_{1}, 0⟩ \\ b_{2} & ⟨F_{2}, 1⟩ & ⟨G_{2}, 0⟩ & ⟨F_{1}, 1⟩ \end{matrix}

\begin{matrix}o & ⟨G_{1}^{⊥}, 1⟩ & ⟨F_{1}^{⊥}, 0⟩ \\ b_{1} & ⟨G_{1}, 0⟩ & ⟨F_{1}, 1⟩ \end{matrix}

Table 1. Principal types and polarities of formulas

With respect to some signed formula ⟨F, 0⟩ occurrences of sub-formulas are abbreviated uniquely by positions from a set Pos. We use type symbols as metavariables for positions abbreviating formulas of that type (e.g. α for a formula of type α), b for arbitrary types, and a for atomic formulas. The corresponding formula, its polarity, and its type can be retrieved from a position b by means of lab(b), pol(b), and Ptype(b), respectively. sform (b) shall denote the signed formula ⟨lab(b), pol(b)⟩. The relations ≻ and ≫ are defined like for formulas. succ(b) denotes the set of all positions b′ for which b′ ≻ b holds. A position tree for a formula F is obtained from the formula tree of F by, first, marking all nodes of the tree with positions thereby removing the old markings and, second, applying the rewrite rules 1–5 in Figure 2 as long as possible. The dashed lines may be replaced by an arbitrary number of positions of type o. These rewrite rules insert special positions ϕ (variable) and ψ (constant) from sets Φ_{L} and Ψ_{L} (both sets disjoint with Pos) into the tree. The inserted positions separate layers of α–type positions from layers of β–type positions and atomic positions from all other ones. During the separation of layers we do not care about positions of type o. Constant special positions mark the ports of β-layers. For instance, when rule 1 is applied to positions α and β where α ≫ β holds and only positions of type o occur between these positions a constant special position ψ is inserted as immediate predecessor of α. The motivation for the insertion of special positions will become clearer after the definition of σ_{L}-complementarity. Note, however, that special positions for MLL seperate layers of formulas instead of marking formulas with specific connectives which is done for intuitionistic logic [27].

1 α β  α ψ β  2 β α  β ϕ α  3 a α  a ϕ α  4 a β  a ϕ ψ β  5 a  a ϕ

Fig. 2. Construction of a position tree by insertion of special positions

For each position b we define the prefix of that position as the string pre(b) of special positions from the root of the tree to b.

Example 1. A position tree T for the formula ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥})⊗(B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} and the prefix of every position in the tree is depicted below.

α_{0} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{0}^{ϕ_{1} : ⊗^{0}}  ^{o_{9} : ^{⊥} ^{0}}^{β_{1} : ⊗^{0}}  ^{ϕ_{10} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{1}}^{ψ_{2} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{0}}  ^{ψ_{6} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{0}}  ^{β_{10} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{1}}^{α_{2} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{0}}  ^{α_{6} : ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{0}}  ^{ψ_{11} : A^{1}}  ^{ψ_{12} : B^{1}}^{ϕ_{3} : A^{0}} ^{o_{4} : ^{⊥} ^{0}} ^{ϕ_{7} : B^{0}} ^{ϕ_{8} : A^{0}}  ^{ϕ_{11} : A^{1}}  ^{ϕ_{12} : B^{1}}^{a_{3} : A^{0}} ^{ϕ_{5} : A^{1}} ^{a_{7} : B^{0}} ^{a_{8} : A^{0}}  ^{a_{11} : A^{1}}  ^{a_{12} : B^{1}} a_{5} : A^{1}  \begin{matrix}b & pre(b) \\ α_{0}, o_{9} \\ ϕ_{1}, β_{1} & ϕ_{1} \\ ψ_{2}, α_{2}, o_{4} & ϕ_{1}.ψ_{2} \\ ϕ_{3}, a_{3} & ϕ_{1}.ψ_{2}.ϕ_{3} \\ ϕ_{5}, a_{5} & ϕ_{1}.ψ_{2}.ϕ_{5} \\ ψ_{6}, α_{6} & ϕ_{1}.ψ_{6} \\ ϕ_{7}, a_{7} & ϕ_{1}.ψ_{6}.ϕ_{7} \\ ϕ_{8}, a_{8} & ϕ_{1}.ψ_{6}.ϕ_{8} \\ ϕ_{10}, β_{10} & ϕ_{10} \\ ψ_{11} & ϕ_{10}.ψ_{11} \\ ϕ_{11}, a_{11} & ϕ_{10}.ψ_{11}.ϕ_{11} \\ ψ_{12} & ϕ_{10}.ψ_{12} \\ ϕ_{12}, a_{12} & ϕ_{10}.ψ_{12}.ϕ_{12} \end{matrix}

Paths, Connections, Substitutions, and Complementarity. We define the paths (sets of positions) through a position tree T starting at the root b_{0} of T .

– {b_{0}} is a path.

– If p ∪ {b} is a path where b is neither a leaf-position nor of type β then p ∪ succ(b) is a path.

– If p ∪{β} is a path and succ(β)={b_{1}, b_{2}} then p ∪{b_{1}} and p ∪{b_{2}} are paths. A path which contains atomic positions only is called atomic path. A connection c is a two-element set of positions {a_{1}, a_{2}} for which a_{1}, a_{2} are leaf-positions, and lab(a_{1}) = lab(a_{2}) as well as pol(a_{1})≠pol(a_{2}) holds. We say that a path p contains a connection c if c ⊆ p holds.

A prefix substitution is an idempotent mapping σ_{L} : Φ_{L} → (Φ_{L} ∪ Ψ_{L})^{∗} which deviates from the identity on Φ_{L} only for a finite subset of Φ_{L}. We extend σ_{L} to Φ_{L}∪Ψ_{L} by the identity mapping on Ψ_{L} and denote the homomorphic extension to (Φ_{L} ∪Ψ_{L})^{∗} by σ_{L} as well. σ_{L} is admissible if σ_{L}(pre(b))=s_{1}.b holds for the image s= s_{1}.b.s_{2} of every prefix, i.e. substitutions shall be computed by unification.

We call a connection {a_{1}, a_{2}} σ_{L}-complementary iff the images of the prefixes of a_{1} and a_{2} are identical under an admissible substitution σ_{L} (i.e. iff σ_{L}(pre(a_{1})) = σ_{L}(pre(a_{2}))). A set C of connections is said to span a position tree T iff each path through T contains at least one connection from C. A spanning set C of connections is minimal for T iff removing any connection from C yields a set which is not spanning for T . T is relevant for C iff each atomic position of T is contained in at least one connection from C.

Definition 1 (Complementarity of a Formula Tree). A position tree T is complementary iff there exists a set of connections C and a prefix substitution σ_{L} such that all connections in C are σ_{L}-complementary, T is relevant for C, and C is spanning and minimal for T .

The σ_{L}-complementarity of a connection ensures that the members of a connection cannot be separated during context split and therefore occur in an initial sequent. Thus, unification guarantees the existence of an order of rule applications together with a context splitting which form a sequent proof rather than calculating one such order. Hereby avoiding redundancies due to permutabilities of rules, irrelevant reductions and notational redundancies.

Example 2. Consider the position tree in Example 1. The atomic paths through T are p_{1} ={a_{3}, a_{5}, a_{11}}, p_{2} ={a_{3}, a_{5}, a_{12}}, p_{3} ={a_{7}, a_{8}, a_{11}}, and p_{4} ={a_{7}, a_{8}, a_{12}}. p_{1} contains the connection c_{1} = {a_{3}, a_{5}} and p_{3} contains c_{2} = {a_{8}, a_{11}}. The set C = {c_{1}, c_{2}, {a_{7}, a_{12}}} spans T . The admissible prefix substitution

σ_{L} = {ϕ_{1}\ε, ϕ_{3}\ε, ϕ_{5}\ε, ϕ_{7}\ψ_{12}, ϕ_{8}\ψ_{11}, ϕ_{10}\ψ_{6}, ϕ_{11}\ε, ϕ_{12}\ε} makes all connections in C σ_{L}-complementary. T is complementary since C is spanning and minimal and since T is relevant for C.

From a prefix substitution σ_{L} a binary relation ⊏_{L} ⊆ Ψ_{L} ×Φ_{L} is constructed. If for some ϕ and some ψ there exist strings s_{1} and s_{2} such that σ_{L}(ϕ) = s_{1}.ψ.s_{2} then ψ⊏_{L}ϕ holds. The reduction ordering < = (≪ ∪⊏_{L})^{+} is the transitive closure of this relation and the tree ordering.

Irreflexivity of a reduction ordering would become a separate requirement only if – as in first order modal logics [27] – a combined substitution is used. We expect that such a substitution would be required for linear logics when the fragment will be extended. An equivalent theorem for the propositional modal logics in [27] could be shown similarly.

Theorem 2. If a set of connections C is σ_{L}-complementary for a position tree T then the reduction ordering < induced by σ_{L} is irreflexive. Proof. Assume that there exists a position b such that b<b holds. If any such position exists, there is one of type ϕ. Then for some index set {0, …, n − 1} (n > 1) there are positions ϕ_{i} and ψ_{i} (i ∈ {0, …, n − 1}, ϕ = ϕ_{0}) such that ϕ_{i} ≪ ψ_{i} and ψ_{i}⊏_{L}ϕ_{(i+1)mod n} holds. This implies that σ_{L} is not admissible for the image of some prefix and for some ψ_{i} – a contradiction.

We state the correctness and completeness of our characterization and sketch the proofs only due to limitations of space. The complete proofs can be found in [15]. All proofs are based on a sequent calculus for linear logic and do not use any criterions from proof nets. Thus, they can serve as a basis for extensions to other fragments of linear logic.

Lemma 3 (Correctness). If the position tree T corresponding to a formula F is complementary then F is valid. Proof sketch. Since T is complementary there is a set of connections C and a prefix substitution σ_{L} such that all complementarity conditions (relevance, spanning, minimality, and σ_{L}-complementarity) are satisfied. Using a reduction ordering induced by σ_{L} a sequent proof can be constructed in an analytic fashion. Connections become the elements of initial sequents in the sequent proof. This construction uses the sequent calculus K^{MLL} introduced in [15]. The correctness of the construction procedure is proven by induction on the weight of sequences. For the complete proof of the lemma we refer to [15].

Lemma 4 (Completeness). If F is a valid formula then the corresponding position tree T is complementary. Proof sketch. Since F is valid a sequent proof P for · ⊢ F exists. We construct a connection from every application of the axiom-rule in P. A partial ordering ⊏_{P} is constructed from P such that if a special position b is reduced before a position b′ then b ⊏_{P} b′ holds. We substitute ϕ by an ordered string of constant special positions such that for every position ψ in the string the label of ψ is reduced before ϕ but after every special position b ≪ ϕ. The lengthy proof in [15] that T is complementary for C and σ_{L} uses induction on the structure of P.

The following theorem is the foundation for matrix proof methods (based on our characterization) which prove the validity of linear logic formulas.

Theorem 5. A formula F in the multiplicative fragment of linear logic is valid iff the corresponding position tree T is complementary. Proof. Follows directly from Lemma 3 and 4.

Example 3. The position tree T of the formula ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥})⊗(B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} from Example 1 with the spanning set of connections C from Example 2 is depicted below. Connections are drawn as curved lines. The reduction ordering < induced by the substitution σ_{L} from Example 2 is depicted by arrows where straight arrows are induced by ≪ and curved arrows by ⊏_{L}. Since the position tree is complementary the formula is valid according to Theorem 5.

α_{0} ϕ_{1}  o_{9} β_{1}  ϕ_{10} ψ_{2}  ψ_{6}  β_{10} α_{2}  α_{6}  ψ_{11}  ψ_{12} ϕ_{3} o_{4} ϕ_{7} ϕ_{8}  ϕ_{11}  ϕ_{12} a_{3} ϕ_{5} a_{7} a_{8}  a_{11}  a_{12} a_{5}

During automated proof search a useful reduction of the search space can be achieved by focusing on linearity. A set of connections C is linear iff each atomic position of T is contained in at most one connection from C.

Lemma 6. If a position tree T is complementary for a set of connections C and an admissible substitution σ_{L}, then C is linear. Proof sketch. σ_{L}-complementarity guarantees that proper context splitting is possible. Minimality ensures that no unnecessary connections exist.

3 The Proof Procedure for MLL

According to the above matrix characterization the validity of a formula F can be proven by showing that all paths through the matrix representation of F, i.e. through the position tree, contain a complementary connection. In this section we will describe a general path checking algorithm as well as the corresponding complementarity test which involves an algorithm for T-string unification. Path Checking. One possibility to perform proof search is to use an algorithm based on analytic tableaux as done in [22] for intuitionistic logic. The path checking algorithm presented in the following is driven by connections instead of the logical connectives. Once a complementary connection has been identified all paths containing this connection are deleted. This is similar to Bibel’s connection method for classical logic and formulas in clausal form [4].

The theoretical basis of the following algorithm is described in detail in [21] where it is used for proof search in classical, intuitionistic and modal logics. Only a few modifications were necessary to adapt it to MLL. Definition 7 (α-related, β-related). Two positions u and v are α-/β-related, denoted u∼_{α}v/u∼_{β}v, iff u≠v and the greatest common ancestor of u and v, wrt. the tree ordering ≪, is of principal type α/β. A position u and a set of positions S are α-/β-related, denoted u∼_{α}S/u∼_{β}S, iff u∼_{α}v/u∼_{β}v for all v ϵ S. Remark. If two atoms are α-/β-related they appear side by side/one upon the other in the matrix representation (see example 4).

The main function Proof_{MLL}(F) in Figure 3 returns true iff the formula F is valid in the multiplicative linear logic MLL.

Function Proof_{MLL}(F)

Input: multiplicative formula F

Output: true, if, and only if, F is valid in MLL begin Proof_{MLL}; Con := ∅; valid := Subproof_{MLL}(F, ∅, ∅); return valid;

end Proof_{MLL}.

Fig. 3. Function Proof_{MLL}(F)

The function Proof_{MLL}(F) initializes the set of connections Con. After that the function Subproof_{MLL} is invoked.

The function Subproof_{MLL}(F, P, C) in Figure 4 implements the path checking algorithm where the set P is called the active path and the set C is called the proven subgoals. By A we denote the set of all atomic positions in the formula F. All variables except for A and Con are local.

Function Subproof_{MLL}(F, P, C) Input: formula F, active path P⊆A, proven subgoals C⊆A Output: true, if (P, C) wrt. F is provable (see [21]); false, otherwise

begin Subproof_{MLL}; if there is no A ϵ A where A∼_{α}P and A∼_{β}C then return true; E := ∅; Con′ := Con; repeat

select A ϵ A where A∼_{α}(P∪E) and A∼_{β}C; if there is no such A then return false; E := E ∪ {A}; D := ∅; valid := false; noconnect := false; repeat

select Ā ϵ A where Ā ϵ̸ D and Ā∼_{α}(P∪{A}) and

Complementary_{MLL}(F, Con′∪{{A, Ā}}) and Line(F, Con′∪{{A, Ā}}); if there is no such Ā

then noconnect := true

else D := D ∪ {Ā}; Con := Con′ ∪ {{A, Ā}}; valid := Subproof_{MLL}(F, P∪{A}, {Ā}); if valid=true then valid := Subproof_{MLL}(F, P, C∪{A}); if valid=true and P=∅ then valid := Mini Rele(F, Con);

until valid=true or noconnect=true; until valid=true; return true; end Subproof_{MLL}.

Fig. 4. Function Subproof_{MLL}(F, P, C)

During the proof search the active path P will specify those paths which are just being investigated for complementarity. All paths which contain the active path P and additionally one element of the proven subgoals C will already have been proven complementary. The only modifications wrt. [21] are an additional set Con which contains the connections computed so far and the two additional functions Line(F, Con) and Mini Rele(F, Con). Line returns true iff Con is linear wrt. F. Mini Rele returns true iff Con is minimal and relevant wrt. F and is invoked only after a spanning set Con has been found.^{4}

4 In this case linearity and relevance of Con implies minimality, if the following condition holds: |Con| = #_{β} + 1 where #_{β} is the number of β-type positions in the formula tree of F. This cardinality criterion optimizes proof search in MLL but may not generalize to larger fragments of linear logic (see [15] for details).

T-String Unification. In our path checking algorithm we have to ensure that after adding a connection to the current set Con there still is a (multiplicative) substitution σ_{L} under which all connections are complementary. Therefore the function Complementary_{MLL}(F, Con) is used, which returns true iff there is a substitution σ_{L} that unifies the prefixes of the connected atoms Con, i.e. iff the set of prefix-equations {pre(u) = pre(v) | {u, v} ϵ Con} is solvable.

To unify the set of prefixes Γ = {p_{1}=q_{1}, …, p_{n}=q_{n}} we use a specialized string unification which respects the restrictions on every two prefixes p and q: no character is repeated either in p nor in q and equal characters only occur within a common substring at the beginning of p and q. This restriction allows us to give an efficient algorithm computing a minimal set of most general unifiers. Similar to the ideas of Martelli and Montanari [16] rather than by giving a recursive procedure we consider the process of unification as a sequence of transformations.

We start with the given set of (prefix-) equations Γ = {p_{1}=q_{1}, …, p_{n}=q_{n}} and an empty substitution σ_{L}=∅. Each transformation step replaces the tuple Γ, σ_{L} by a modified tuple σ_{L}′(Γ′), σ_{L}′ in which one equation {p_{i}=q_{i}} in Γ is replaced by {p′_{i}=q′_{i}} and the (modified) substitution σ_{L}′ is applied to it. The algorithm is described by transformation rules “ {p_{i}=q_{i}}, σ_{L} → {p′_{i}=q′_{i}}, σ_{L}′ ” which can be applied nondeterministically to the selected equation {p_{i}=q_{i}} ϵ Γ.^{5} The set Γ is solvable, iff there are some transformation steps transforming Γ into the empty set Γ′=∅. In this case the (final) substitution σ_{L}′ represents an idempotent most general unifier for Γ. For technical reasons we divide the right part q_{i} of each equation into two parts q_{i}^{1}|q_{i}^{2} where the left part contains the substring which is not yet assigned to a variable. Therefore we start with the set of prefixes Γ = {p_{1} = ε|q_{1}, …, p_{n}=ε|q_{n}}.

Definition 8 (Transformation Rules for MLL). Let V be a set of variables, C a set of constants, and V′ a set of auxiliary variables with V ∩ V′=∅. The set of transformation rules for MLL is defined in Table 2.

R1. {ε = ε|ε}, σ_{L}  → {}, σ_{L}
R3. {Xs = ε|Xt}, σ_{L}  → {s = ε|t}, σ_{L}
R5. {V s = z|ε}, σ_{L}  → {s = ε|ε}, {V \z}∪σ_{L}
R8. {V s^{+} = ε|V_{1}t}, σ_{L} → {V_{1}t = V |s^{+}}, σ_{L}
R9. {V s^{+} = z^{+}|V_{1}t}, σ_{L} → {V_{1}t = V′|s^{+}}, {V \z^{+}V′}∪σ_{L}
R10. {V s = z|Xt}, σ_{L}  → {V s = zX|t}, σ_{L} (V ≠X, and s=ε or t≠ε or X ϵ C)

s, t and z denote (arbitrary) strings and s^{+}, z^{+} non-empty strings. X, V, and V_{1} denote single characters with X ϵ V ∪ C ∪ V′ and V, V_{1} ϵ V ∪ V′ (with V ≠V_{1}). V′ ϵ V′ is a new variable which does not occur in the substitution σ_{L} computed so far.

Table 2. Transformation Rules for Multiplicative Linear Logic (MLL)

These rules are identical with the rules used in [21] and [20] which deal with intuitionistic logic. Since the prefixes to be unified in MLL have either the form C_{1}V_{1}C_{2}V_{2} … C_{n}V_{n} or V_{1}C_{2}V_{2} … C_{n}V_{n} (where C_{i} ϵ C and V_{i} ϵ V for 1≤i≤n, n≥1), we do not need the rules R2, R4, R6, and R7 anymore.

5 To obtain an efficient unification procedure the order of the selected equations {p_{i}=q_{i}} is essential, i.e. must be selected according to the tree ordering ≪.

For a comprehensive treatment of the algorithm for T-string unification together with an intuitive graphical motivation we refer to [20].

Example 4. Let F ≡ ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥}) ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} as in Example 1. The proof of F below is marked in the matrix representation^{6} of F. Furthermore the set of connections Con as well as the (multiplicative) substitution σ_{L} is given. This substitution represents the most general unifier for the prefixes of the connected atoms. The substitution σ_{L} from Example 2 is a special instance which results from replacing ϕ_{1}, ϕ_{5}, ϕ_{11}, ϕ_{12}, and ϕ_{20} by the empty word ε.

A^{0} B^{0} A^{1} Ã^{0}  Ã^{1} B^{1}

Con := {{A^{0}, A^{1}}, {B^{0}, B^{1}}, {Ã^{1}, Ã^{0}}}
σ_{L} := {ϕ_{3}\ϕ_{5}, ϕ_{8}\ϕ_{20}ψ_{11}ϕ_{11}, ϕ_{7}\ϕ_{20}ψ_{12}ϕ_{12},

ϕ_{10}\ϕ_{1}ψ_{6}ϕ_{20}} where ϕ_{20} is a new variable.

4 Transforming MLL Matrix Proofs into Sequent Proofs

In [24, 25] we have developed a conversion procedure for transforming matrix proofs into conventional sequent proofs for classical and non-classical logics. When constructing this procedure our main emphasis was the uniformity of the approach according to the matrix characterizations for these logics [27]. To emphasize uniformity we have developed unified representations of matrix characterizations and sequent calculi which were divided into variant and invariant parts. The division resulted in an invariant transformation algorithm which consults a variant table system reflecting different properties of the logics.

We were able to adapt our uniform transformation procedure to MLL by extending its variant part while leaving its general structure unchanged. In order to convert MLL-matrix proofs into sequent proofs the procedure has to obtain a linearization of the partial reduction ordering <. Essentially this can be done by traversing < but certain non-permutabilities of sequent rules which are not yet represented in < have to be respected as well. Similar to [24], we have achieved a “completion” of < by dynamically adding wait-labels to certain nodes which prevent the corresponding sequent rules from being applied too early. This concept fills the gap between the target calculus Lin_{M} (Figure 1) of our conversion and a sequent calculus K^{MLL} [15] on which the matrix characterization is based.

Proof Reconstruction in MLL. Our algorithm takes as input a reduction ordering ∝^{⋆} which for technical reasons is generated from < by adding a new root w. While traversing ∝^{⋆} it will mark all the visited positions x as solved (solved [x] = ⊤). At the beginning, w is considered solved and its successor x is open for being solved next. Then the following process proceeds: an open position x will be selected and marked as solved if it is solvable. Afterwards the corresponding sequent rule will be constructed and the successor nodes of x will be added to the set of open positions. This means that the corresponding sub-formulas are now isolated in the actual sequent and may be reduced. This process is repeated until two solved positions form a connection which allows us to close the corresponding branch of the sequent proof with an axiom rule.

6 We use labels instead of positions and distinguish the two atoms A^{0}/A^{1} by a tilde.

In addition to the above traversal process there are a few subtle details that need to be taken care of. Before we explain these let us illustrate the reconstruction process by our running example.

Example 5. We take the formula ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥})⊗(A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} and the reduction ordering < from Example 3. We start traversal by selecting the only open position α_{0} in ∝^{⋆} and mark it as solved. From Ptype (α_{0}) = α and sform (α_{0}) = ⟨lab(α_{0}), pol(α_{0})⟩, with pol(α_{0}) = 0, we construct a sequent rule of type α reducing the operator ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} of lab(α_{0}) in the succedent, i.e. α(sform (α_{0})) = ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r. For computing the sub-formulas in the rule’s premises we consult Table 1.

After this step ϕ_{1} and o_{9}, the successors of α_{0}, become open in ∝^{⋆}. ϕ_{1} is not yet solvable since the principle of layer reductions has to be respected, which means that a series of open α- (or β-) and o-positions has to be reduced as long as possible. To express this additional non-permutability of Lin_{M}–rules we dynamically assign a wait-label to ϕ_{1} (a wait_{2}-label, to be precise). Hence, we will visit o_{9} next, construct ^{⊥}r, and mark the successor ϕ_{10} of o_{9} as open.

ϕ_{10} is not yet solvable since the unsolved node ψ_{6}, a successor of ϕ_{1}, has a higher priority wrt. ⊏_{L}. To express (ψ_{6}, ϕ_{10})^{∈} ⊏_{L}, a wait_{1}-label has been statically assigned to ϕ_{10} before the traversal process. Upon reaching this wait_{1}- label the algorithm will compute the ≪-greatest open predecessor of ψ_{6}, that is ϕ_{1}. This node can now be marked as solved since wait_{2}[ϕ_{1}] not longer holds. No rule will be constructed since ϕ_{1} is a special position which does not encode a sequent rule in Lin_{M}.

In the next step we reach the β-position β_{1} and construct the rule ⊗r which will cause the sequent proof to branch into two independent sub-proofs. In MLL the remaining resources (i.e. sequent formulas) will now have to be distributed over the new sub-branches. This additional process, called context splitting, yields ∅ for the left sub-branch and ⟨A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B, 1⟩ for right one. In the algorithm, context splitting is realized by an operation split (∝^{⋆}, β_{1}) which will divide the reduction ordering ∝^{⋆} into two sub-orderings [∝_{1′}^{⋆}, ∝_{2′}^{⋆}]. In our example ∝_{1′}^{⋆} has one open position ψ_{2} whereas ∝_{2′}^{⋆} contains two open position ψ_{6} and ϕ_{10}.

Proof reconstruction will now continue separately on each sub-ordering. For ∝_{2′}^{⋆} we continue by solving ψ_{6} and deleting the wait_{1}-label which blocks ϕ_{10} (called update). But now wait_{2}[ϕ_{10}] must be set dynamically since α_{6} is open (layer reduction). Solving α_{6} yields the rule ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r which prepares correct context splitting at the next β-position β_{10}. The reconstruction process will now continue as before and eventually yield the following Lin_{M}–proof.

\begin{matrix}A ⊢ A & axiom (a_{3}, a_{5}) \\ ⊢ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥} \end{matrix} ; ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} r, ^{⊥}r (α_{2}, o_{4})

A ⊢ A axiom (a_{11}, a_{8}) B ⊢ B axiom (a_{12}, a_{7})

A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ B, A ............................................................................................... l (β^{10})

A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A ............................................................................................... r (α^{6})

A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ⊢ (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥})⊗(B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A) ⊗r (β^{1})

⊢ ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥})⊗(B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)^{⊥} ............................................................................................... r, ^{⊥}r (α^{0}, o^{9})

Adapting the Conversion Algorithm to MLL. From the above example we develop the concepts for the conversion procedure. We omit formal details (see [24, 25]) in order to emphasize properties which are specific to MLL.

function TOTAL(∝^{⋆}, MLL) : S-list = for all x^{∈} positions (∝^{⋆}) do solved [x] := ⊥; solved [root (∝^{⋆})] := ⊤; return TOT(∝^{⋆}, MLL)

function TOT(∝^{⋆}, MLL) : S-list = proven_{∝⋆} := ⊥; S_{∝⋆} := []; compute P_{o}; for all x^{∈} positions (∝^{⋆}) do compute wait_{1}[x]; while not proven_{∝⋆} do x := select fair P_{o}; S_{∝⋆} := append (S_{∝⋆} , SOLVE (x, ∝^{⋆}, MLL)) return S_{∝⋆}

function SOLVE (x, ∝^{⋆}, MLL) : S-list =

(1) if wait_{1}[x] then select (y, x)^{∈} ⊏_{L}; (k, r) := free(y, ∝^{⋆}); return SOLVE (succ_{r}(k), ∝^{⋆}, MLL) else if wait_{2}[x] then y:= select fair {z^{∈} P_{o} | x≠z}; return SOLVE (y, ∝^{⋆}, MLL)

else solved [x] := ⊤; P_{o} := (P_{o} \ {x}) ∪ succ (x); if Ptype (x) = ψ then update (x, ∝^{⋆}); case Ptype (x) of {ϕ, ψ} : return [] {atom} : select {x, y}^{∈} C

if solved [y] then proven_{∝⋆} := ⊤; return [axiom (sform (x), sform (y))] else (k, r) = free(y, ∝^{⋆}); return SOLVE (succ_{r}(k), ∝^{⋆}, MLL)

{o, α} : return [Ptype (x) (sform (x))] {β} :

(2)  [∝1′^{⋆} , ∝2′^{⋆}] = split (∝^{⋆}, x); p_{0} = [β (sform (x), (∝1′^{⋆} , ∝2′^{⋆}))]; p_{1} = TOT (∝1′^{⋆} , MLL); p_{2} = TOT (∝2′^{⋆} , MLL);

proven_{∝⋆} := ⊤;
return append (p_{0}, append (p_{1}, p_{2}))

function update (x, ∝^{⋆}) = for all {y | (x, y)^{∈} ⊏_{L}} do ⊏_{L} := ⊏_{L} \ {(x, y)}; wait_{1}[y] := ⊥

Definitions:

open (x) ⇔ solved [pred (x)]
∧ ¬solved [x]
P_{o} = {x^{∈} positions (∝^{⋆}) | open (x)}
wait_{1}[x] ⇔ ∃y.(y, x)^{∈} ⊏_{L}
wait_{2}[x] ⇔ Ptype (x)^{∈} {ψ, ϕ}

∧ ∃y^{∈} P_{o}.Ptype (y)^{∉} {ψ, ϕ}

succ+_{j}(x) := {succ_{j}(x)}∪succ^{+}(succ_{j}(x))

free(x, ∝^{⋆}) computes an ancestor/rank pair (k, r) with the ≪-greatest ancestor k such that x^{∈} succ+_{r}(k) and open (succ+_{r}(k))

select fair denotes a fair selection strategy of open positions to guarantee termination wrt. the different wait-labels.

Fig. 5. The uniform transformation procedure adapted to MLL.

The set of immediate successors/predecessors of a position x wrt. ≪ is denoted by succ (x)/pred (x). succ^{+}(x)/pred^{+}(x) denotes all successors/predecessors of x. If succ (x)={x_{1}, x_{2}} we assume a unique selection function succ_{j}(x) = x_{j}, j^{∈} {1, 2}. The definitions on the right hand side of Figure 5 summarize the necessary concepts which we introduced informally in Example 5.

For context splitting at β-positions x we have adopted the operation split (∝^{⋆}, x) from [25]. It first divides ∝^{⋆} into two subrelations ∝_{1}^{⋆}, ∝_{2}^{⋆} where each ∝_{i}^{⋆} contains the successor tree of x having root x_{i} ^{∈} succ (x). The connections C_{i} and the relation ⊏_{L}_{i} are divided accordingly. Second, two non-normal form reductions will be applied to each ∝_{i}^{⋆} for correct context splitting and result in ∝_{i′}^{⋆}. For MLL we can simplify these reductions to the following MLL-reduction: Iteratively delete all subtrees with root y from ∝_{i}^{⋆} if y^{∈} P_{o} and there exists some b^{∈} succ^{+}(y) with b^{∉} c for all c^{∈} C_{i}. Using Lemma 3 and wait_{2}-labels we obtain.

Lemma 9. split (∝^{⋆}, x) is correct & complete for context splitting in Lin_{M}.

The resulting algorithm TOTAL adapted to MLL is depicted in Figure 5. The boxed area (1) focuses on integrating rule non-permutabilities into the conversion process. Box (2) summarizes the splitting process and recursive calls at β-positions. The procedure terminates with proven_{∝^{⋆}} and results a list of sequent rules S_{∝^{⋆}} forming the sequent proof in Lin_{M}. No search is needed for conversion, i.e. the Lin_{M} proof can be reconstructed in polynomial time in the size of the MLL matrix proof.

Theorem 10 (Completeness/Correctness). The procedure TOTAL for converting MLL matrix proofs into Lin_{M} sequent proofs is correct & complete. Proof sketch. Correctness follows from the correct construction of sequent rules at each position and correct context splitting (Lemma 9). For completeness the non-permutabilities of rule applications are captured by wait_{1}- and wait_{2}-labels where the latter fill the gap between Lin_{M} and K^{MLL} (Lemma 3), i.e.layer reductions. Finally, wait_{2}-labels do not cause deadlocks during traversal since by definition there always exists an open non-special position. TOTAL terminates because the set of unsolved positions is decreased by each step.

5 Conclusion

We have presented a matrix characterization of logical validity in the multiplicative fragment of linear logic MLL. On this basis we have extended our uniform proof search method [21] into a matrix-based proof procedure for MLL and our uniform transformation method [24] into a procedure for translating the resulting matrix proofs back into a sequent proof. Both methods could be adapted without modifications of the algorithmic structure. ‘Only’ the entries of logicdependent tables which are consulted by the algorithms had to be elaborated.

Some preliminary attempts for obtaining matrix characterizations in fragments of linear logic have been made on the basis of acyclic connection graphs [7, 8]. This acyclicity condition is very close to proof nets and these attempts will therefore very like have similar limitations. In contrast to that our approach is based on prefixes and unifies the advantages of several approaches to proof search in linear logic without sharing their problems. Like Andreoli’s focusing principle [1] and normal proofs [10] it avoids the permutabilities of sequent rules. Context splitting can be performed as efficiently as in resource management systems [5]. There is, however, no need for transformations in negational normal form or for following the connectives during proof search (an advantage also over Tammet’s proof search strategies [26]). Prefix-Unification is as efficient as the acyclicity test implicitly contained in [7] but yields informations which make the conversion into sequent proofs more efficient. Checking the cardinality criterion instead of an exponential test for minimality is another improvement.

The most striking feature ouf our approach, however, is its generality and uniformity. It is emphasized by the fact that both the proof search procedure and the algorithm for conversion into sequent proofs, which originally had been developed for dealing with classical, intuitionistic, and modal logics, could so easily be adapted to MLL, which semantically is entirely different. This makes us very confident that our method can be extended to further fragments of linear logic once a matrix characterization has been found. The similarities between sequent calculi for linear logics and those for the logics already characterized gives us additional evidence that extensions of our approach to larger fragments of linear logic will be possible. We believe that Wallen’s conjecture (see introduction) will eventually turn out to be true for linear logic. Currently we are developing a matrix characterization for MELL, the combination of MLL and exponentials and will investigate other fragments afterwards.

In the logics investigated so far the matrix characterization was always strongly related to the Kripke semantics of the logic. It may therefore become possible to follow this relation in the opposite direction and to construct a Kripke semantics for linear logic out of the matrix characterizations. We shall explore this possibility once a larger fragment of linear logic has been characterized.

References

1. J.-M. Andreoli. Logic programming with focussing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1993.

2. W. Bibel. On matrices with connections. Journal of the ACM, 28:633–645, 1981.

3. W. Bibel. A deductive solution for plan generation. New Generation Computing, 4:115–132, 1986.

4. W. Bibel. Automated theorem proving. Vieweg, 1987.

5. I. Cervesato, J.S. Hodas, F. Pfenning Efficient resource management for linear logic proof search. Extensions of Logic Programming, LNAI 1050, pp. 67–81, 1996.

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

7. B. Fronhöfer The action-as-implication paradigm, CS Press, 1996.

8. D. Galmiche Connection methods in linear logic fragments and proof nets construction. CADE–13 workshop on proof search in type-theoretic languages, 1996.

9. D. Galmiche, G. Perrier. A procedure for automatic proof nets construction. LPAR’92, LNAI 624, pp. 42–53, Springer Verlag, 1992.

10. D. Galmiche, G. Perrier. On proof normalization in linear logic. TCS, 135:67–110, 1994.

11. V. Gehlot, C. Gunter. Normal process representatives. In Proc. 5-th Annual IEEE Symposium on Logic in Computer Science, pp. 200–207, 1991

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

13. J.-Y. Girard. Proof-nets: the parallel syntax for proof-theory. In Logic and Algebra, LNPAM 150, pp. 97–124, 1996.

14. J.S. Hodas, D. Miller. Logic programming in a fragment of linear logic. Journal of Information and Computation, 110(2):327–365, 1994.

15. H. Mantel. Eine Matrixcharakterisierung für ein Fragment der linearen Logik. Diplomarbeit, TH-Darmstadt, Germany, 1996.

16. A. Martelli, U. Montanari.An efficient unification algorithm.ACM TOPLAS, 4:258–282, 1982.

17. M. Masseron, C. Tollu, J. Vauzielles Generating plans in linar logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pp. 63–75, Springer, 1990.

18. J. McCarthy, P.H. Hayes Some philosophical problems from the standpoint of Artificial Intelligence Machine Intelligence,4:463–502, 1969.

19. J. Otten, C. Kreitz. A connection based proof method for intuitionistic logic. 4^{th} TABLEAUX Workshop, LNAI 918, pp. 122–137, Springer Verlag, 1995.

20. J. Otten, C. Kreitz. T-string-unification: unifying prefixes in non-classical proof methods. 5^{th} TABLEAUX Workshop, LNAI 1071, pp. 244–260, Springer Verlag, 1996.

21. J. Otten, C. Kreitz. A uniform proof procedure for classical and non-classical logics. KI-96: Advances in Artificial Intelligence, LNAI 1137, pp. 307–319, Springer Verlag, 1996.

22. J. Otten. ileanTAP: An intuitionistic theorem prover. International Conference TABLEAUX’97, LNAI, Springer Verlag, 1997.

23. S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standard-sequent proofs. 4^{th} TABLEAUX Workshop, LNAI 918, pp. 106–121, Springer Verlag, 1995.

24. S. Schmitt, C. Kreitz. Converting non-classical matrix proofs into sequent-style systems. CADE–13, LNAI 1104, pp. 418–432, Springer Verlag, 1996.

25. S. Schmitt, C. Kreitz. A uniform procedure for converting non-classical matrix proofs into sequent-style systems. Journal of Information and Computation, submitted.

26. T. Tammet. Proof strategies in linear logic.Jour. of Automated Reasoning, 12:273–304, 1994.

27. L. Wallen. Automated deduction in non-classical logics. MIT Press, 1990.

This article was processed using the LaTEX macro package with LLNCS style