linTAP : A Tableau Prover for Linear Logic

Heiko Mantel^{1} Jens Otten^{2}

1 German Research Center for Artificial Intelligence (DFKI) Stuhlsatzenhausweg 3, 66123 Saarbrücken, Germany

                                        mantel@dfki.de

2 Fachgebiet Intellektik, Fachbereich Informatik, Darmstadt University of Technology Alexanderstr. 10, 64283 Darmstadt, Germany

                              jeotten@informatik.tu-darmstadt.de

Abstract. linTAP is a tableau prover for the multiplicative and exponential fragment M?LL of Girards linear logic. It proves the validity of a given formula by constructing an analytic tableau and ensures the linear validity using prefix unification. We present the tableau calculus used by linTAP, an algorithm for prefix unification in linear logic, the linTAP implementation, and some experimental results obtained with linTAP.

1 Introduction

Linear logic [12] can be regarded as a refinement of classical as well as of intuitionistic logic. It subsumes these logics because both of them can be embedded into linear logic. Mainly, linear logic has become known as a very expressive logic of action and change. It has found applications in logic programming [14,20], planing [19], modeling concurrent computation [11], and other areas. Its expressiveness, however results in a high complexity. Validity is undecidable for propositional linear logic. The multiplicative fragment is already N P-complete [16]. The complexity of the multiplicative exponential fragment (MELL) is still unknown. Consequently, proof search in linear logic is difficult to automate.

Various calculi have been developed for linear logic. Beginning with the sequent calculus and proof nets by Girard [12], several optimizations have been proposed. More recently, the connection method has been extended to fragments of linear logic [8,9,15,17]. In this article, we propose a tableau calculus for MELL and for M?LL which is the theoretical basis for our theorem prover linTAP.

linTAP is implemented in a very compact way but uses sophisticated techniques to reduce the search space and thus follows the idea of lean theorem proving. It was inspired by the classical tableau prover leanTAP [2,3] and by the intuitionistic tableau prover ileanTAP [21]. Like in ileanTAP, string unification is used to deal with the non-permutabilities specific to linear logic. This approach has been invented by Wallen in the context of matrix characterizations for non-classical logics [25]. The prefixes used by linTAP are motivated by a matrix characterization for MELL [17]. In our implementation of linTAP we use a leanTAP like technique for path checking and then try to unify the so-called prefixes of atoms which are closing the branches of the tableau proof like in ileanTAP. Some additional checks are required because of the resource sensitivity of linear logic. Some of these checks are tested already during proof construction.

After some preliminaries we propose a tableau calculus for MELL in Section 3. The application of a calculus rule to a formula de-constructs the formula and constructs a prefix for the resulting sub-formulas. An algorithm for the unification of such prefixes is presented in Section 4. A tableau calculus for M?LL, where ? and ! can only occur, respectively, positively and negatively, some details about our theorem prover linTAP, and some experimental results are discussed in Section 5. We conclude with some remarks on related and on future work.

2 Preliminaries

Linear logic [12] treats formulas like resources that disappear after their use unless they are explicitly marked as reusable. It can be seen as the outcome of removing the rules for contraction and weakening from the classical sequent calculus and re-introducing them in a controlled manner. Linear negation ^{⊥} is involutive like classical negation. The two traditions for writing the sequent rule for conjunction result in two different conjunctions ⊗ and & and two different disjunctions ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and ⊕. The constant true splits up into 1 and ⊤ and false into ⊥ and 0. The unary connectives ? and ! mark formulas for a controlled application of weakening and contraction. Quantifiers ∀ and ∃ are added as usual.

Linear logic can be divided into the multiplicative, additive, and exponential fragment. While in the multiplicative fragment resources are used exactly once, resource sharing is enforced in the additive fragment. Exponentials mark formulas as reusable. All fragments exist on their own right and can be combined freely. The full power of linear logic comes from combining all of them.

In this article we focus on multiplicative exponential linear logic (MELL and M?LL), the combination of the multiplicative and exponential fragments, leaving the additive fragment and the quantifiers out of consideration. ^{⊥}, ⊗, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , −∘, 1, ⊥, !, and ? are the connectives of MELL. In M?LL, ? and ! only occur, respectively, with positive and negative polarity. Linear negation ^{⊥} expresses the difference between resources that are to be used up and resources to be produced. In order to use up F^{⊥} a resource F must be produced. Having a resource F_{1}⊗F_{2} means having F_{1} as well as F_{2}. F_{1} −∘F_{2} allows the construction of F_{2} from F_{1}. F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2} is equivalent 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. A resource !F acts like a machine which produces any number of copies of F. During the construction of !F only such machines can be used. ? is the dual to !.

We adopt Smullyan’s uniform notation to MELL. A signed formula φ = F^{k} denotes an occurrence of F in Δ or Γ. Depending on the label F and its polarity k ∈ {+, −}, a signed formula will receive a type α, β, ν, π, o, τ, ω, or a according to the tables below. The functions succ_{1} and succ_{2} return the major signed subformulas of a signed formula. Note that during the decomposition of a formula the polarity switches only for ^{⊥} and −∘. We use type symbols as meta-variables for signed formulas of the respective type, e.g. α stands for a signed formula of type α and a stands for atomic formulas, i.e. signed predicates.

The validity of a linear logic formula can be proven syntactically by using a sequent calculus. For multi-sets Γ and Δ of formulas Γ ⟶ Δ is called a sequent.

\begin{matrix}a & A^{−} & A^{+} \\ τ & ⊥^{−} & 1^{+} \\ ω & 1^{−} & ⊥^{+} \end{matrix} α  (F_{1}⊗F_{2})^{−} (F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2})^{+} (F_{1}−∘F_{2})^{+}

succ_{1}(α)  F_{1}^{−}  F_{1}^{+}  F_{1}^{−}
succ_{2}(α)  F_{2}^{−}  F_{2}^{+}  F_{2}^{+}
β  (F_{1}⊗F_{2})^{+} (F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2})^{−} (F_{1}−∘F_{2})^{−}
succ_{1}(β)  F_{1}^{+}  F_{1}^{−}  F_{1}^{+}
succ_{2}(β)  F_{2}^{+}  F_{2}^{−}  F_{2}^{−}

o (F^{⊥})^{−} (F^{⊥})^{+}
succ_{1}(o) F^{+} F^{−}
ν  (!F)^{−} ?F^{+}
succ_{1}(ν) F^{−} F^{+}
π  (?F)^{−} !F^{+}
succ_{1}(π) F^{−} F^{+}

Table 1. Uniform notation for signed MELL formulas

It can be understood as the specification of a transformation which constructs Δ from Γ. The formulas in Γ are connected implicitly by ⊗ while the formulas in Δ are connected implicitly by ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} .

A sequent calculus Σ′_{1} for MELL based on our uniform notation is depicted in Table 2. Omitting the π-rule yields a calculus for M?LL. In a rule, the sequents above the line are the premises and the one below is the conclusion. A principal formula is a formula that occurs in the conclusion but not in any premise. Formulas that occur in a premise but not in the conclusion are called active. All other formulas compose the context. Σ′_{1} is correct and complete wrt. Girard’s original sequent calculus [12].

⟶ A^{+}, A^{−} axiom  ⟶ τ τ  {⟶ Υ \atop ⟶ Υ, ω} ω  {⟶ Υ, succ_{1}(o) \atop ⟶ Υ, o} o
⟶ Υ, succ_{1}(α), succ_{2}(α) ⟶ Υ, α α  ⟶ Υ_{1}, succ_{1}(β) ⟶ Υ_{2}, succ_{2}(β) ⟶ Υ_{1}, Υ_{2}, β β
{⟶ Υ, succ_{1}(ν) \atop ⟶ Υ, ν} ν  {⟶ ν, succ_{1}(π) \atop ⟶ ν, π} π  {⟶ Υ \atop ⟶ Υ, ν} w  {⟶ Υ, ν, ν \atop ⟶ Υ, ν} c

Table 2. Sequent calculus Σ′_{1} for MELL in uniform notation

In analytic proof search, one starts with the sequent to be proven and reduces it by application of rules until the axiom-rule or the τ-rule can be applied. There are several choice points within this process. As in classical logic, first, a principal formula must be chosen. Unless the principal formula has type ν, this choice determines which rule must be applied. Formulas of type ν are generic. They can be duplicated using the contraction rule c and are removed by the weakening rule w. When the β-rule is applied the context of the sequent must be split, i.e. Υ_{1} and Υ_{2} must be a partition of the context. Several solutions have been proposed in order to optimize these choices [1,10,23,6,13]. Additional difficulties arise from the rules axiom, τ, and π. The rules axiom and τ require an empty context which expresses that all formulas must be used up in a proof. The π rule requires that all formulas in the context are of type ν. The careful handling of the context reflects the resource sensitivity of linear logic.

Example 1. Figure 1 presents a Σ′_{1}-proof of φ = (((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥}))^{+}. We abbreviate occurrences of subformulas of φ by position markers as shown in the table on the right. Note that any proof of φ requires that the contraction rule c is applied before the β-rule.

\begin{matrix}⟶ a_{1111}, a_{1211} & axiom \\ ⟶ a_{1111}, o_{121} \end{matrix} ; o ; ⟶ a_{1111}, ν_{12} ; ν ; ⟶ a_{1111}, ω_{1112}, ν_{12} ; ω ; ⟶ α_{111}, ν_{12} ; α \begin{matrix}⟶ a_{1121}, a′_{1211} & axiom \\ ⟶ a_{1121}, o′_{121} \end{matrix} ; o ; ⟶ a_{1121}, ν′_{12} ; ν ; ⟶ π_{112}, ν′_{12} ; π

⟶ β_{11}, ν_{12}, ν′_{12} β

⟶ β_{11}, ν_{12} c

⟶ α_{1} α

\begin{matrix}lab(φ′) & φ′ \\ ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥}) & α_{1} \\ (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A & β_{11} \\ A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥ & α_{111} \\ A & a_{1111} \\ ⊥ & ω_{1112} \\ !A & π_{112} \\ A & a_{1121} \\ ?(A^{⊥}) & ν_{12}, ν′_{12} \\ A^{⊥} & o_{121}, o′_{121} \\ A & a_{1211}, a′_{1211} \end{matrix}

Fig. 1. An example Σ′_{1}-proof.

3 A Tableau Calculus

The tableau calculus presented in this section is motivated by a matrix characterization for MELL [17]. Basic Definitions. We assume disjoint sets Φ^{M}, Ψ^{M}, Φ^{E}, and Ψ^{E} of characters. ϕ^{M}, ψ^{M}, ϕ^{E}, and ψ^{E} are used as meta-variables for characters from the respective set. Elements of Φ^{M} and Ψ^{M} are called multiplicative and elements of Φ^{E}, and Ψ^{E} are called exponential. Characters in Φ^{M} and Φ^{E} are called variable and characters in Ψ^{M} and Ψ^{E} are called constant. The intuition is that variable characters can be substituted while constant characters cannot. A prefix s is a string over these sets, i.e. s ∈ (Φ^{M} ∪ Ψ^{M} ∪ Φ^{E} ∪ Ψ^{E})^{∗}. A multiplicative string substitution is a mapping σ_{M} : Φ^{M} → (Φ^{M} ∪ Ψ^{M})^{∗}. An exponential string substitution is a mapping σ_{E} : Φ^{E} → (Φ^{M} ∪ Ψ^{M} ∪ Φ^{E} ∪ Ψ^{E})^{∗}. A string substitution is a mapping σ : (Φ^{M} ∪ Φ^{E}) → (Φ^{M} ∪ Ψ^{M} ∪ Φ^{E} ∪ Ψ^{E})^{∗} such that the restriction of σ to Φ^{M} is a multiplicative string substitution and the restriction to Φ^{E} is an exponential string substitution. We extend σ homomorphically to strings from (Φ^{M} ∪ Ψ^{M} ∪ Φ^{E} ∪ Ψ^{E})^{∗} where σ is the identity on constant characters.^{1}

A position p is a string from P = {l, r}^{∗} ∪{0}. p is a sub-position of a position p′ if p′ is a proper prefix of p, e.g. lrl is a sub-position of lr. A multiplicity μ is a function which assigns natural numbers to positions, i.e. μ : P → IN. Using multiplicities, we determine the number of duplicates of generic formulas in a tableau. We mark each occurrence of a formula in a tableau proof with a position. In a tableau for φ, φ is marked with position 0. If φ is marked with p then the left and right subformula of φ are marked with p ∘ l and p ∘ r, respectively. For a generic formula φ the jth instance of the subformula is marked with p ∘ l^{j}. Definition 2. Let φ be a signed formula, s be a prefix, and p be a position. Then φ : s (p) is called a prefixed formula. If φ is of type a, τ, ω, or ν then [φ] : s (p) is prefixed formula as well. We refer to the later kind as marked prefixed formulas.

The type of a prefixed formula φ : s (p) is the type of φ. We use the same meta-variables for prefixed formulas as for signed formulas. If necessary, we will point out what kind of formula is denoted by a specific meta-variable. Definition 3. A connection is a one-element set containing a marked prefixed formula of type τ or a two-element set containing two marked atomic prefixed formulas with the same label and opposite signs. A weakening map is a set of marked prefixed formulas of type ω and of type ν with multiplicity 0.

1 For M?LL the set Ψ^{E} is not needed. Thus, Φ^{M} and Φ^{E} need not be distinguished.

For example, {[1]^{+} : s′ (p′)} and {[A]^{+} : s′′ (p′′), [A]^{−} : s′′′ (p′′′)} are connections; ∅, {[⊥]^{+} : t′ (q′)}, and {[?F]^{+} : t′′ (q′′), [1]^{−} : t′′′ (q′′′)} are weakening maps.

Note, that Definition 3 imposes the same restrictions on the elements of a connection as the Σ′_{1}-rules τ and axiom do for the principal formulas in order to close a branch. It requires the same properties for the elements of a weakening map as the Σ′_{1}-rules ω and w do for the principal formulas in order to remove a formula. This resembles the relation between a proof according to the connection method and the set of sequent proofs represented by it [17]. It should be helpful to keep this in mind in order to grasp the intuition behind the following definitions.

Complementarity Conditions and Closed Tableaux. We now define some complementarity conditions which are crucial for our definition of closed tableaux in MELL. Each condition is motivated by a property of the sequent calculus Σ′_{1} in Table 2 and, if possible, an intuitive explanation based on the resource sensitivity of linear logic is given. In the following we always assume C to be a set of connections, W to be a weakening map, and σ to be a string substitution.

– Resources can be used at most once and disappear after their use. In Σ′_{1} this is reflected by the lack of a general rule for contraction and by the context split in the β-rule. C is linear if each prefixed formula occurs in at most one connection. C and W are linear if C is linear and p is not a sub-position of p′ for any φ : s (p) which occurs in a connection from C and any φ′ : s′ (p′) ∈ W. Intuitively, this linearity condition says that a formula cannot contribute to an axiom in a corresponding sequent proof if it has been weakened and that it cannot contribute to more than one axiom.

– Resources cannot disappear without a reason. They must be consumed. In Σ′_{1} this is reflected by the lack of a general rule for weakening and by the requirement of an empty context in the rules axiom and τ. C and W are relevant for a set of prefixed formulas Υ if each φ : s (p) ∈ Υ occurs at least in one connection or a φ′ : s′ (p′) ∈ Υ occurs in W where p is a sub-position of p′. Intuitively, relevance demands for a corresponding sequent proof that a formula must contribute to an axiom unless it has been weakened.

– In Σ′_{1}, the context only is divided by the application of a β-rule. Let β be a set of prefixed formulas of type β and let β_{W} = {(β : s (p)) ∈ β | there is no (φ : s′ (p′)) ∈ W such that p is a sub-position of p′}. C and W have the right cardinality for β if |C| = |β_{W} | + 1.

– In Σ′_{1}, certain rule applications can be permuted while others cannot. The non-permutability of rules for linear logic has been investigated e.g. in [10]. The existence of a suitable order of non-permutable rule applications is expressed by the unifiability of prefixes. C and W are unified by σ if

• for each c ∈ C the prefixes of all elements of c are identical under σ and • for each φ ∈ W there is a c ∈ C such that the prefix of φ is an initial

substring of the prefix of the elements of c under σ.

Definition 4. Let φ be a prefixed formula.

1. The one-branch tree φ is a tableau for φ.

2. If T is a tableau for φ and T^{∗} results from T by the application of a tableau expansion rule from Table 3 then T^{∗} is a tableau for φ.

α-rules

\begin{matrix}(F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2})^{+}: & s & (p) \\ F_{1}^{+} : & s ∘ s′ & (p ∘ l) \\ F_{2}^{+} : & s ∘ s′ & (p ∘ r) \end{matrix} \begin{matrix}(F_{1}⊗F_{2})^{−}: & s & (p) \\ F_{1}^{−} : & s ∘ s′ & (p ∘ l) \\ F_{2}^{−} : & s ∘ s′ & (p ∘ r) \end{matrix} \begin{matrix}(F_{1} −∘ F_{2})^{+}: & s & p \\ F_{1}^{−} : & s ∘ s′ & (p ∘ l) \\ F_{2}^{+} : & s ∘ s′ & (p ∘ r) \end{matrix} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
ν-rules (for μ(F_{1}) > 0)

\begin{aligned}(!F_{1})^{−} & : & s & (p) \\ (F_{1}^{1})^{−} & : & s ∘ s′ ∘ ϕ_{p∘l}^{E} & (p ∘ l) \\ ⋮ & & ⋮ & ⋮ \\ (F_{1}^{μ(F_{1})})^{−} & : & s ∘ s′ ∘ ϕ_{p∘l^{μ(F_{1})}}^{E} & (p ∘ l^{μ(F_{1})}) \end{aligned} \begin{aligned}(?F_{1})^{+} & : & s & (p) \\ (F_{1}^{1})^{+} & : & s ∘ s′ ∘ ϕ_{p∘l}^{E} & (p ∘ l) \\ ⋮ & & ⋮ & ⋮ \\ (F_{1}^{μ(F_{1})})^{+} & : & s ∘ s′ ∘ ϕ_{p∘l^{μ(F_{1})}}^{E} & (p ∘ l^{μ(F_{1})}) \end{aligned}

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
w-rules (for μ(F_{1}) = 0)
\frac{(!F_{1})^{−} : s (p)}{[!F_{1}]^{−} : s ∘ s′ (p ∘ l)}  \frac{(?F_{1})^{+} : s (p)}{[?F_{1}]^{+} : s ∘ s′ (p ∘ l)}
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
ω-rules
\frac{1^{−} : s (p)}{[1]^{−} : s ∘ s′ (p ∘ l)}  \frac{⊥^{+} : s (p)}{[⊥]^{+} : s ∘ s′ (p ∘ l)}
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
a-rules
\frac{A^{−} : s (p)}{[A]^{−} : s ∘ s′ ∘ ϕ_{p}^{M}(p ∘ l)}  \frac{A^{+} : s (p)}{[A]^{+} : s ∘ s′ ∘ ϕ_{p}^{M}(p ∘ l)}
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
τ-rules
\frac{⊥^{−} : s (p)}{[⊥]^{−} : s ∘ s′ ∘ ϕ_{p}^{M}(p ∘ l)}  \frac{1^{+} : s (p)}{[1]^{+} : s ∘ s′ ∘ ϕ_{p}^{M}(p ∘ l)}
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

s′ = ψ_{p}^{M} if s = s̃ ∘ ϕ with ϕ ∈ Φ^{E} ∪ Φ^{M} s′ = ε if s = s̃ ∘ ψ with ψ ∈ Ψ^{E} ∪ Ψ^{M}

β-rules
\frac{(F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2})^{−} : s (p)}{F_{1}^{−} : s ∘ s′′ (p ∘ l) F_{2}^{−} : s ∘ s′′ (p ∘ r)} \frac{(F_{1}⊗F_{2})^{+} : s (p)}{F_{1}^{+} : s ∘ s′′ (p ∘ l) F_{2}^{+} : s ∘ s′′ (p ∘ r)}

\frac{(F_{1} −∘ F_{2})^{−} : s (p)}{F_{1}^{+} : s ∘ s′′ (p ∘ l) F_{2}^{−} : s ∘ s′′ (p ∘ r)}

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
π-rules
\begin{matrix}(!F_{1})^{+} : & s & (p) \\ F_{1}^{+} : & s ∘ s′′ ∘ ψ_{p∘l}^{E} & (p ∘ l) \end{matrix}  \begin{matrix}(?F_{1})^{−} : & s & (p) \\ F_{1}^{−} : & s ∘ s′′ ∘ ψ_{p∘l}^{E} & (p ∘ l) \end{matrix}
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

s′′ = ϕ_{p}^{M} if s = s̃ ∘ ψ with ψ ∈ Ψ^{E} ∪ Ψ^{M} s′′ = ε if s = s̃ ∘ ϕ with ϕ ∈ Φ^{E} ∪ Φ^{M}

o-rules
\begin{matrix}(F_{1}^{⊥})^{+} : & s & (p) \\ F_{1}^{−} : & s & (p ∘ l) \end{matrix}  \begin{matrix}(F_{1}^{⊥})^{−} : & s & (p) \\ F_{1}^{+} : & s & (p ∘ l) \end{matrix}

Table 3. A prefixed-based tableau calculus for MELL

Expansion rules are applied as usual [7]. The application of a rule de-constructs a formula, possibly enlarges the prefix, and constructs a position. A tableau is strict if each occurrence of a formula is reduced at most once on a branch. In a strict tableau, prefixed formulas can be uniquely identified by their positions. In the sequel, we will consider only strict tableaux and will extensively use the isomorphism between formulas in a given tableaux and their positions.

Definition 5. A branch of a tableau is closed by a connection c if all elements of c occur on that branch.

Let T be a tableau for φ, Υ_{T} be the set of prefixed formulas of type a, τ, ω, and ν (with multiplicity 0) which occur in T, and β_{T} be the set of prefixed formulas of type β in T. Further, let C be a set of connections where the elements of connections are from Υ_{T}. Let W be a weakening map with elements from Υ_{T}. Let σ be a string substitution. Then C and W fulfill linearity in T if C and W are linear. C and W fulfill relevance in T if C and W are relevant for Υ_{T}. C and W fulfill cardinality in T if C and W have the right cardinality for β_{T}. C, W, and σ fulfill unifiability for T if C and W are unified by σ.

Definition 6. Let T be a tableau for a prefixed formula φ. Further, let C be a set of connections, W be a weakening map, and σ be a string substitution. T is closed by C, W, and σ iff the following conditions hold:

– Each branch of T is closed by a connection from C.

– C, W, and σ fulfill linearity, relevance, cardinality, and unifiability for T.

Example 7. A tableau T for ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥}) is depicted in Figure 2. The set of connections C={{0llll, 0rlll}, {0lrll, 0rllll}} closes the branches of the tableau. Let W = {0llrl} be a weakening map and σ be a substitution with σ(ϕ_{0rl}^{E}) = ϕ_{0l}^{M}ψ_{0ll}^{M}ϕ_{aux1}^{M}, σ(ϕ_{0lll}^{M}) = ϕ_{aux1}^{M}ψ_{0rll}^{M}ϕ_{0rll}^{M}, σ(ϕ_{0rll}^{E}) = ϕ_{0l}^{M}ψ_{0lrl}^{E}ϕ_{aux2}^{M}, and σ(ϕ_{0lrl}^{M}) = ϕ_{aux2}^{M}ψ_{0rlll}^{M}ϕ_{0rlll}^{M}. Then T is closed by C, W, and σ.

The following theorems state that the tableau calculus in Table 3 is correct and complete. In order to follow the proof sketches prior knowledge of [17] is required.

Theorem 8 (Correctness). If there is a closed tableau for a prefixed formula φ = F^{+} : ψ_{0}^{M} (0) for some multiplicity μ then F is valid.

Proof Sketch: Let T be a tableau for φ with multiplicity μ which is closed by C, W, and σ. We construct a matrix proof for the matrix M of φ. The correctness of the matrix characterization in [17] then implies that φ is valid.

For every prefixed formula φ′ in T there is a corresponding node n in M with the same label, polarity, type, and ancestors which are equivalent under this relation. Let m be an injective mapping which assigns to a formula in T a corresponding node in M. All non-special nodes in M are in the image of m. We define the application of m to sets as the application of m to the elements. For any path of leaves P through M there is branch B in T with marked formulas Υ_{B} such that m(Υ_{B}) ⊆ P holds. Let C_{M} = m(C) and W_{M} = m(W). Since all branches of T are closed by C, C_{M} is spanning for M. C_{M} and W_{M} are linear,

\begin{matrix}11 : [⊥]^{+} : & ψ_{0}^{M} ϕ_{0l}^{M} ψ_{0ll}^{M} & (0llrl) \\ 12 : [A]^{+} : & ψ_{0}^{M} ϕ_{0l}^{M} ψ_{0ll}^{M}ϕ_{0lll}^{M} & (0llll) \\ 13 : [A]^{−} : & ψ_{0}^{M} ϕ_{0rl}^{E}ψ_{0rll}^{M}ϕ_{0rll}^{M} & (0rlll) \end{matrix}^{ω on (9) a on (8), (10) 10 : A^{−} : ψ_{0}^{M} ϕ_{0rl}^{E} (0rll)}^{o on (4) \begin{matrix}8 : A^{+} : & ψ_{0}^{M} ϕ_{0l}^{M} ψ_{0ll}^{M} & (0lll) \\ 9 : ⊥^{+} : & ψ_{0}^{M} ϕ_{0l}^{M} ψ_{0ll}^{M} & (0llr) \end{matrix}}^{α on (6) 6 : (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)^{+} : ψ_{0}^{M} ϕ_{0l}^{M} (0ll)}  _{_{_{\begin{matrix}16 : [A]^{+} : & ψ_{0}^{M} ϕ_{0l}^{M} ψ_{0lrl}^{E}ϕ_{0lrl}^{M} & (0lrll) \\ 17 : [A]^{−} : & ψ_{0}^{M} ϕ_{0rll}^{E}ψ_{0rlll}^{M}ϕ_{0rlll}^{M} & (0rllll) \end{matrix}^{a on (14), (15) 15 : A^{−} : ψ_{0}^{M} ϕ_{0rll}^{E} (0rlll)}}^{o on (5) 14 : A^{+} : ψ_{0}^{M} ϕ_{0l}^{M} ψ_{0lrl}^{E} (0lrl)}}^{π on (7) 7 : (!A)^{+} : ψ_{0}^{M} ϕ_{0l}^{M} (0lr)}} [figure: β on (2); β on (2); \begin{matrix}4 : (A^{⊥})^{+} : & ψ_{0}^{M} ϕ_{0rl}^{E} & (0rl) \\ 5 : (A^{⊥})^{+} : & ψ_{0}^{M} ϕ_{0rll}^{E} & (0rll) \end{matrix}]^{ν on (3) \begin{matrix}2 : (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A^{+} : & ψ_{0}^{M} & (0l) \\ 3 : ?(A^{⊥})^{+}  : & ψ_{0}^{M} & (0r) \end{matrix}}^{α on (1) 1: ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥})^{+} : ψ_{0}^{M} (0)}

Fig. 2. An example tableau

relevant, and have the cardinality property for M. Marked formulas of type a, τ, ω, and ν have the same prefix (under renaming) as the correspondent nodes in M. Therefore, σ is a unifier for C_{M} and W_{M} in M. Thus, M is complementary for C_{M}, W_{M}, and σ.

Theorem 9 (Completeness). If a formula F is valid then there exists a closed tableau for the prefixed formula φ = F^{+} : ψ_{0}^{M} (0). Proof Sketch: From any matrix proof of the matrix M of φ a closed tableau for φ can be constructed. The completeness of the matrix characterization then implies that a tableau for any valid formula exists.

The crucial step is that if there is a complementary matrix M′ for φ with multiplicity μ′ then there is a multiplicity μ, a set of connections C, a weakening map W without elements of type ϕ^{E}, and a string substitution σ such that the matrix M for φ with multiplicity μ is complementary for C, W, and σ. Using C, W, and σ, a closed tableau for φ can be constructed.

4 Prefix Unification

The computation of a string substitution σ is one of the key components necessary to perform proof search in the prefix-based tableau calculus introduced in the previous section. A single string substitution σ has to unify the prefixes of each connection in the set C. Furthermore the weakening map W has to fulfill the unifiability condition under this substitution σ. This condition can be reduced to unification since a prefix s is an initial substring of a prefix t iff s ∘ V and t can be unified where V is a new variable.

String unification in general is rather complicated but fortunately unifying prefixes is much easier since there are two restrictions on prefixes: prefixes are strings without duplicates and in any two prefixes (corresponding to atoms of the same formula) equal characters can only occur within a common substring at the beginning of the prefixes. In [22] we introduced a prefix unification algorithm, so-called T-String Unification, to unify prefixes in matrix based proof methods for non-classical logics, i.e. intuitionistic logic and the modal logics D, K, D4, K4, S5, and T. Only minor modifications are necessary to adapt this algorithm to deal with the prefixes arising in our tableau calculus for MELL: we have to distinguish between characters (i.e. positions) of type ϕ^{M}/ψ^{M} and type ϕ^{E}/ψ^{E}.

Similar to the ideas of Martelli and Montanari [18] we consider the process of unification as a sequence of transformation steps. We start with the given set of (prefix-) equations Γ = {p_{1}=t_{1}, …, p_{n}=t_{n}} and an empty substitution σ=∅. Each transformation step replaces the tuple (Γ, σ) by a modified tuple (Γ′, σ′) where Γ′ is the result of replacing one equation {p_{i}=t_{i}} in Γ by {p′_{i}=t′_{i}} and applying the substitution σ′ to the resulting equation set. The algorithm is described by transformation rules “ {s_{i}=t_{i}}, σ → {s′_{i}=t′_{i}}, σ′ ” which can be applied nondeterministically to the selected equation {s_{i}=t_{i}} ϵ Γ. The set Γ is solvable, iff there are some transformation steps transforming the tuple (Γ, ∅) into the tuple (∅, σ̃). In this case the substitution σ̃ represents an idempotent most general unifier for Γ. The set of all resulting most general unifiers is minimal. For technical reasons we divide the right part t_{i} of each equation into two parts t_{i}^{1}|t_{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 Γ = {s_{1}=ε|t_{1}, …, s_{n}=ε|t_{n}}.

Definition 10. Let V=Φ^{M}∪Φ^{E} be a set of variables, C=Ψ^{M}∪Ψ^{E} be a set of constants, Ṽ^{M} and Ṽ^{E} be disjoint sets of auxiliary variables, V′=Ṽ^{M}∪Ṽ^{E} (with V∩V′=∅), V^{M}=Φ^{M}∪Ṽ^{M}, and V^{E}=Φ^{E}∪Ṽ^{E}. The set of transformation rules for MELL is defined in Table 4.

R1. {ε = ε|ε}, σ  → {}, σ
R2. {ε = ε|t^{+}}, σ  → {t^{+} = ε|ε}, σ
R3. {Xs = ε|Xt}, σ  → {s = ε|t}, σ
R4. {Cs = ε|V t}, σ  → {V t = ε|Cs}, σ
R5. {V s = z|ε}, σ  → {s = ε|ε}, {V \z}∪σ
R6. {V s = ε|C_{1}t}, σ → {s = ε|C_{1}t}, {V \ε}∪σ
R7. {V s = z|C_{1}C_{2}t}, σ → {s = ε|C_{2}t}, {V \zC_{1}}∪σ  (V ϵ V^{E} or C_{1} ϵ Ψ^{M})
R8. {V s^{+} = ε|V_{1}t}, σ → {V_{1}t = V |s^{+}}, σ  (V_{1} ϵ V^{E} or V ϵ V^{M})
R8′. {V s^{+} = ε|V_{1}t}, σ → {V_{1}t = V |s^{+}}, {V \Ṽ^{M}}∪σ  (V_{1} ϵ V^{M} and V ϵ V^{E})
R9. {V s^{+} = z^{+}|V_{1}t}, σ → {V_{1}t = V′|s^{+}}, {V \z^{+}V′}∪σ
(if V_{1},V ϵ V^{E} then V′ ϵ Ṽ^{E} else V′ ϵ Ṽ^{M})
R10. {V s = z|Xt}, σ  → {V s = zX|t}, σ  (V ϵ V^{E} or X ϵ (V^{M} ∪Ψ^{M}))
R10′. {V s = z|Xt}, σ  → {V s = zX|t}, {X\Ṽ^{M}}∪σ  (V ϵ V^{M} and X ϵ V^{E})

s,t,z ϵ (V∪C∪V′)^{∗} denote (arbitrary) strings, s^{+},t^{+},z^{+} ϵ (V∪C∪V′)^{+} denote non-empty strings. X, V, V_{1}, C, C_{1} and C_{2} denote single characters with X ϵ V∪C∪V′, V ,V_{1} ϵ V∪V′ (with V ≠V_{1}), and C, C_{1}, C_{2} ϵ C. V′ and Ṽ^{M} ϵ Ṽ^{M} are new variables which do not occur in the substitution σ computed so far. To apply rule R10 or R10′ the following must hold: V ≠X, and s=ε or t≠ε or X ϵ C.

Table 4. Transformation rules for MELL

These rules are identical with the transformation rules presented in [22]. We only added rules R8′ and R10′ (which are applied instead of rules R8 and R10 in certain cases) and some additional restrictions for the rules R7 and R9 (characters X ϵ V^{E}∪Ψ^{E} cannot be assigned to variables V ϵ V^{M}). We use the notation {x\t | σ(x)=t and x≠t} to specify a substitution σ and omit the string concatenation operator “∘”. See [22] for a graphical motivation of these rules, a more detailed description of the algorithm, and some complexity results.

Example 11. Consider the formula ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥)⊗!A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥}) from Example 7 and the unification of the two prefixes ψ_{0}^{M}ϕ_{0l}^{M}ψ_{0lrl}^{E}ϕ_{0lrl}^{M} and ψ_{0}^{M}ϕ_{0rll}^{E}ψ_{0rlll}^{M}ϕ_{0rlll}^{M}. To keep the notation simple we substitute each character ϕ_{p} and ψ_{p} by V_{|p|} and C_{|p|}, respectively, i.e. we start the unification process with the tuple {C_{0}^{M}V_{2}^{M}C_{4}^{E}V_{4}^{M}= ε|C_{0}^{M}V_{4}^{E}C_{5}^{M}V_{5}^{M}}, {} and apply the transformation rules according to Table 4:

{C_{0}^{M}V_{2}^{M}C_{4}^{E}V_{4}^{M} = ε|C_{0}^{M}V_{4}^{E}C_{5}^{M}V_{5}^{M}}, {} ⟶^{R3} {V_{2}^{M}C_{4}^{E}V_{4}^{M} = ε|V_{4}^{E}C_{5}^{M}V_{5}^{M}}, {}

⟶^{R8} {V_{4}^{E}C_{5}^{M}V_{5}^{M} = V_{2}^{M}|C_{4}^{E}V_{4}^{M}}, {} ⟶^{R10} {V_{4}^{E}C_{5}^{M}V_{5}^{M} = V_{2}^{M}C_{4}^{E}|V_{4}^{M}}, {}

⟶^{R9} {V_{4}^{M} = V′|C_{5}^{M}V_{5}^{M}}, {V_{4}^{E}\V_{2}^{M}C_{4}^{E}V′} ⟶^{R10} {V_{4}^{M} = V′C_{5}^{M}|V_{5}^{M}}, {V_{4}^{E}\V_{2}^{M}C_{4}^{E}V′}

⟶^{R10} {V_{4}^{M} = V′C_{5}^{M}V_{5}^{M}|ε}, {V_{4}^{E}\V_{2}^{M}C_{4}^{E}V′}

⟶^{R5} {ε = ε|ε}, {V_{4}^{E}\V_{2}^{M}C_{4}^{E}V′, V_{4}^{M}\V′C_{5}^{M}V_{5}^{M}}

⟶^{R1} {}, {V_{4}^{E}\V_{2}^{M}C_{4}^{E}V′, V_{4}^{M}\V′C_{5}^{M}V_{5}^{M}}

The only successful transformation sequence, leading to a tuple {}, σ̃, yields the substitution σ̃ = {V_{4}^{E}\V_{2}^{M}C_{4}^{E}V′, V_{4}^{M}\V′C_{5}^{M}V_{5}^{M}}. Applying rule R10 instead of rule R8 (which is the only nondeterministical choice) does not lead to any successful transformation sequence. Thus the only (most general) unifier is {ϕ_{0rll}^{E}\ϕ_{0l}^{M}ψ_{0lrl}^{E}V′, ϕ_{0lrl}^{M}\V′ψ_{0rlll}^{M}ϕ_{0rlll}^{M}} where V′ is a new introduced variable.

For the fragment M?LL of linear logic (on which we will focus in the following section of this paper) we do not need to deal with characters of type ϕ^{E} or ψ^{E}. Furthermore all prefixes to be unified have the form C_{1}V_{1}C_{2}V_{2}...C_{n}V_{n} (where V_{i} ϵ V and C_{i} ϵ C), allowing us to drop rules R2, R4, R6, and R7 (see also [15]).

Definition 12. Let V=Φ^{M} be a set of variables, C=Ψ^{M} be a set of constants, and V′ be a set of auxiliary variables (with V∩V′=∅). The set of transformation rules for M?LL is defined in Table 5.

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

s,t,z ϵ (V∪C∪V′)^{∗} denote (arbitrary) strings, s^{+},z^{+} ϵ (V∪C∪V′)^{+} denote 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 σ computed so far.

Table 5. Transformation rules for M?LL

5 A Tableau Prover

In this section we present an implementation of the tableau calculus for the fragment M?LL. We first present the calculus and repeat some definitions.

A Tableau Calculus for M?LL. The tableau calculus for M?LL is similar to the calculus for MELL presented in Table 3. Since ? and ! can only occur, respectively, with positive and negative polarity we do not need the π-rule anymore. Because of that there are no positions of type ϕ^{E} or ψ^{E} anymore. Furthermore the ν-rules use a stepwise contraction and the τ- and ω-rules are modified. Let A_{F} be the set of all predicate symbols in the formula F. A tableaux for a formula F is defined as usual (see Definition 4) but with the tableau expansion rules from Table 6 where A_{p} ϵ A′ is a predicate symbol and X_{p} ϵ X is a predicate variable. Let T be a tableau, σ:Φ^{M}→(Φ^{M} ∪ Ψ^{M}) be a string substitution, and σ_{X}:X →(A_{F} ∪ A′) be a predicate substitution.

Definition 13. A branch of T is closed iff it contains a complementary connection, i.e {[A]^{−} : s (p), [B]^{+} : t (q)} where σ(s)=σ(t) and σ_{X} (A)=σ_{X} (B).

Let T be a tableau, C be a set of connections, α_{T} and β_{T} be the set of all positions of formulas of type α and β, respectively, in T.

Definition 14. A tableau T is closed iff (1.) every branch of T is closed by a c ϵ C under σ and σ_{X}, (2.) if {a, b} ϵ C and {a, c} ϵ C then b=c (linearity), (3.) 2|C| = |α_{T} | + |β_{T} | + 1 (relevance), and (4.) 2|C| = 2|β_{T} | + 2 (cardinality).

Theorem 15 (Correctness & Completeness). A formula F is valid in the fragment M?LL iff there is a closed tableau for the prefixed formula F^{+} : ψ_{0} (0).

Proof (Sketch). We show that our calculi for M?LL and MELL (without using rule π) are equivalent for the fragment of M?LL: both ν-rules are equivalent (consider an appropriate multiplicity μ); rules τ and ω are correct and complete, i.e 1^{+} ≡⊥^{−}≡ (A−∘A)^{+} for a new predicate symbol A and ⊥^{+}≡ 1^{−} ≡ (X−∘X)^{−} for an arbitrary predicate symbol X (so that one-element connections are omited and the weakening map is empty), since both 1^{+}/⊥^{−} and (A−∘A)^{+} lead to leafs in the sequent proof and the rules for ⊥^{+}/1^{−} can always applied at the leafs in the sequent proof; linearity and cardinality conditions are identical (with empty weakening map); if C is linear and 2|C|=|α_{T} |+|β_{T} |+1 then every atomic formula occurs in C (relevance condition), since the number of leaves in the (binary) formula tree is equal to the number of inner nodes plus one.

The linTAP Implementation. The previous calculus has been implemented in Prolog (see Table 7). For the syntax of formulas we use the logical connectives “~” (negation ^{⊥}), “*” (conjunction ⊗), “@” (disjunction ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ), “@>” (implication −∘), the exponentials “?” and “!”, the constants “1” (for 1) and “0” (for ⊥), and Prolog atoms for atomic formulas. For example to express the formula ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥ )⊗!A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥}) we use the Prolog term ((a@0)*!a)@ ?(~a).

We use 0 and 1 to present the polarities + and −, respectively. Positions are constructed from right to left and prefixes are represented by Prolog lists. Like in ileanTAP we use two predicates for path checking: fml and prove.

α-rules

\begin{matrix}(F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{3})^{+} : & s & (p) \\ F_{1}^{+}  : & s ∘ s′ & (p ∘ l) \\ F_{3}^{+}  : & s ∘ s′ & (p ∘ r) \end{matrix}  \begin{matrix}(F_{1} ⊗ F_{3})^{−} : & s & (p) \\ F_{1}^{−}  : & s ∘ s′ & (p ∘ l) \\ F_{3}^{−}  : & s ∘ s′ & (p ∘ r) \end{matrix}

\begin{matrix}(F_{1}−∘F_{3})^{+} : & s & (p) \\ F_{1}^{−}  : & s ∘ s′ & (p ∘ l) \\ F_{3}^{+}  : & s ∘ s′ & (p ∘ r) \end{matrix}  s′= \{ \begin{matrix}ψ_{p} , & if s=s̃ ∘ ϕ, ϕ ϵ Φ^{M} \\ ε , & else \end{matrix}

β-rules

\frac{(F_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} F_{2})^{−} : s (p)}{F_{1}^{−} : s ∘ s′ (p ∘ l) F_{2}^{−} : s ∘ s′ (p ∘ r)}  \frac{(F_{1} ⊗ F_{2})^{+} : s (p)}{F_{1}^{+} : s ∘ s′ (p ∘ l) F_{2}^{+} : s ∘ s′ (p ∘ r)}

\frac{(F_{1}−∘F_{2})^{−} : s (p)}{F_{1}^{+} : s ∘ s′ (p ∘ l) F_{2}^{−} : s ∘ s′ (p ∘ r)}  s′= \{ \begin{matrix}ϕ_{p} , & if s=s̃ ∘ ψ, ψ ϵ Ψ^{M} \\ ε , & else \end{matrix}

ν-rules

\begin{matrix}(!F_{1})^{−}: & s & (p) \\ ⊥^{−} : & s & (p) \end{matrix} \begin{matrix}(!F_{1})^{−}: & s & (p) \\ F_{1}^{−} : & s ∘ s′ & (p ∘ l) \\ (!F_{1})^{−}: & s ∘ s′ & (p ∘ r) \end{matrix} \begin{matrix}(?F_{1})^{+}: & s & (p) \\ ⊥^{+} : & s & (p) \end{matrix} \begin{matrix}(?F_{1})^{+}: & s & (p) \\ F_{1}^{+} : & s ∘ s′ & (p ∘ l) \\ (?F_{1})^{+}: & s ∘ s′ & (p ∘ r) \end{matrix}

s′= \{ \begin{matrix}ψ_{p} , & if s=s̃ ∘ ϕ, ϕ ϵ Φ^{M} \\ ε , & else \end{matrix}

o-rules

\begin{matrix}(F_{1}^{⊥})^{+} : & s & (p) \\ F_{1}^{−} : & s & (p ∘ l) \end{matrix}  \begin{matrix}(F_{1}^{⊥})^{−} : & s & (p) \\ F_{1}^{+} : & s & (p ∘ l) \end{matrix}

τ-rules

\begin{matrix}⊥^{−}  : & s & (p) \\ (A_{p}−∘A_{p})^{+} : & s & (p ∘ l) \end{matrix}  \begin{matrix}1^{+}  : & s & (p) \\ (A_{p}−∘A_{p})^{+} : & s & (p ∘ l) \end{matrix}

ω-rules

\begin{matrix}1^{−}  : & s & (p) \\ (X_{p}−∘X_{p})^{−} : & s & (p ∘ l) \end{matrix}  \begin{matrix}⊥^{+}  : & s & (p) \\ (X_{p}−∘X_{p})^{−} : & s & (p ∘ l) \end{matrix}

a(tom)-rules

\begin{matrix}A^{+} : & s & (p) \\ [A]^{+}: & s∘s′∘ϕ_{p} & (p) \end{matrix} \begin{matrix}A^{−} : & s & (p) \\ [A]^{−}: & s∘s′∘ϕ_{p} & (p) \end{matrix}  s′= \{ \begin{matrix}ψ_{p} , & if s=s̃ ∘ ϕ, ϕ ϵ Φ^{M} \\ ε , & else \end{matrix}

Table 6. A prefixed-based tableau calculus for M?LL

fml(F,Pol,P,F1,F2,F3,PrN,Ctr) is used to specify the rules of our prefixbased tableau calculus. It succeeds if there is a rule to expand the formula F. Pol is the polarity, P, F1, F2, F3, and PrN are the position p, formulas F_{1}, F_{2}, F_{3}, and the new prefix character s′, respectively. Ctr is bound to c if a contraction (rule) is applied. According to our calculus we need 18 clauses to specify all rules.

%%% Specification of Tableau Rules
fml(A,   Pol, P,[A,Pol],[],      [],[P],0):-var(A).
fml((A@B), 0, P, (A,0), [],   (B,0),[P],0).          fml((A@B), 1, _, (A,1), (B,1),[],[_],0).
fml((A*B), 1, P, (A,1), [],   (B,1),[P],0).          fml((A*B), 0, _, (A,0), (B,0),[],[_],0).
fml((A@>B),0, P, (A,1), [],   (B,0),[P],0).          fml((A@>B),1, _, (A,0), (B,1),[],[_],0).
fml((!A),  1, P, (A,1), [],((!A),1),[P],c).          fml((!_),  1, _, (1,1), [],   [], [],0).
fml((?A),  0, P, (A,0), [],((?A),0),[P],c).          fml((?_),  0, _, (0,0), [],   [], [],0).
fml(0,     1, P, (P,0), [],   (P,1),[P],0).          fml(1,     1, _, (X,0), (X,1),[],[_],0).
fml(1,     0, P, (P,0), [],   (P,1),[P],0).          fml(0,     0, _, (X,0), (X,1),[],[_],0).
fml((~A),  0, _, (A,1), [],      [], [],0).          fml((~A),  1, _, (A,0), [],   [], [],0).
fml(A,   Pol, P,[A,Pol],[],      [],[P],0).
%%% Path Checking
prove([(F,Pol),Pre,P],UnExp,Lits,Exp,ExpLim,PU,At,Bt,C,C1) :-
   fml(F,Pol,P,F1,F2,F3,PrN,Ctr), append(_,[Lp],Pre),                  % look up tableau rule
   ( Ctr=c -> Exp<ExpLim, Exp1 is (Exp+1) ; Exp1=Exp, ! ),             % control contraction
   ( (F2\=[],var(Lp);F2=[],\+var(Lp)) -> Pre1=Pre;append(Pre,PrN,Pre1) ),% Pre1 is new prefix
   ( F3=[] -> UnExp1=UnExp, At=At3;
              UnExp1=[[F3,Pre1,r(P)]|UnExp], At=[P|At3] ),             % update UnExp1
   prove([F1,Pre1,l(P)],UnExp1,Lits,Exp1,ExpLim,PU1,At1,Bt1,C,C2),     % continue with F1
   ( F2=[] -> PU=PU1, At3=At1, Bt=Bt1, C1=C2 ;
     prove([F2,Pre1,r(P)],UnExp1,Lits,Exp1,ExpLim,PU2,At2,Bt2,C2,C1),  % continue with F2
     append(PU1,PU2,PU), union(At1,At2,At3), union([P|Bt1],Bt2,Bt) ).
prove([[Lit,Pl],Pr,P],_,[[[L,Pl1],Pr1,P1]|Lits],_,_,PU,At,Bt,C,C1) :-  % close branch
   ( Lit=L, Pl is 1-Pl1, Lit=L,  At=[], Bt=[],                 % connection found ?
     (member([P,S],C)  -> (S=P1 -> C1=C, PU=[]) ;              % relevance condition
     (member([P1,S],C) -> (S=P  -> C1=C, PU=[]) ;
      PU=[[Pr,_]=[Pr1,_]], C1=[[P,P1],[P1,P]|C])) ) ;          % add prefixes and connection
   prove([[Lit,Pl],Pr,P],[],Lits,_,_,PU,At,Bt,C,C1).           % otherwise check next literal
prove(Lit,[Next|UnExp],Lits,Exp,ExpLim,PU,At,Bt,C,C1) :-       % add Lit to current branch
   prove(Next,UnExp,[Lit|Lits],Exp,ExpLim,PU,At,Bt,C,C1).      % expand Next formula
%%% T-String Unification
t_string_unify([]).
t_string_unify([S=T|G]):- flatten(S,S1,[]), flatten(T,T1,[]),         % flatten prefix lists
                          tunify(S1,[],T1), t_string_unify(G).        % solve first equation
tunify([],[],[]).                                                     % transfor. rule R1
tunify([X1|S],[],[X2|T])      :- X1==X2, !, tunify(S,[],T).           %      -''-      R3
tunify([V|S],Z,[])            :- V=Z, tunify(S,[],[]).                %      -''-      R5
tunify([V,X|S],[],[V1|T])     :- var(V1), tunify([V1|T],[V],[X|S]).   %      -''-      R8
tunify([V,X|S],[Z1|Z],[V1|T]) :- var(V1), append([Z1|Z],[Vnew],V),    %      -''-      R9
                                 tunify([V1|T],[Vnew],[X|S]).
tunify([V|S],Z,[X|T])         :- (S=[]; T\=[]; \+var(X)) ->           %      -''-      R10
                                 append(Z,[X],Z1), tunify([V|S],Z1,T).
flatten(A,[A|B],B) :- (var(A); A\=[], A\=[_|_]), !.                   % flatten list
flatten([],A,A).
flatten([A|B],C,D) :- flatten(A,C,E), flatten(B,E,D).

Table 7. The source code of linTAP

   prove([(F,Pol),Pre,P],UnExp,Lits,Exp,ExpLim,PU,At,Bt,C,C1) per-

forms the actual proof search. (F,Pol) is the formula currently expanded, Pre its prefix s, P its position p. UnExp and Lits represent lists of formulas not yet expanded and the atomic formulas on the current branch of the tableau. Exp is the number of contractions on the current branch, ExpLim the maximum number of contractions allowed on a branch, PU a list of prefix equations, At and Bt represent the sets α_{T} and β_{T}, and C represents the current set of connections C (more precisely each connection is stored twice, i.e. C= ⋃_{{p,q}ϵC}[ [p, q], [q, p] ]).

After a tableau has been found the prefix equations in PU have to be solved.

This is done by t_string_unify(PU) and tunify(S,[],T) where PU is a system

of string equations to be unified, S and T are two strings to be unified (see [22]).

The following goal succeeds if the formula F is valid in M?LL using not more than ExpLim contractions on each branch:

prove([(F,0),[0],0],[],[],0,ExpLim,PU,At,Bt,[],C),
    length(Bt,Nbt), length(C,Nc), Nc=:=(2*Nbt)+2,       % cardinality
    length(At,Nat), Nc=:=Nat+Nbt+1,                     % linearity
    t_string_unify(PU).                    % unifiability of prefixes

Some experimental results. There are only a few provers and even fewer examples available for M?LL. Table 8 contains some problems for M?LL. The timings for these (valid) formulas are given in Table 9.^{2} We compare linTAP^{3} (with iterative deepening) with the sequent calculus provers llprover (implemented in Prolog; see [24]) and linseq, and with the resolution prover linres (both lastmentioned provers are implemented in Scheme and compiled to C; see [23]).

F_{1} ((A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ⊥) ⊗ A)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ?(A^{⊥})
F_{2} !(A ⊗ C−∘B)⊗!(B ⊗ D ⊗ D−∘C ⊗ D) ⊗ A ⊗ C ⊗ D ⊗ D−∘C ⊗ D
F_{3} (C_{1}^{⊥} ⊗ (C_{2}^{⊥} ⊗ (… (C_{11}^{⊥} ⊗ C_{12}^{⊥})..)))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (C_{12}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (C_{11}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} …^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (C_{2}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C_{1})..))
F_{4} (C_{1}^{⊥} ⊗ (C_{2}^{⊥} ⊗ (… (C_{11}^{⊥} ⊗ C_{12}^{⊥})..))) ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ((C_{12} ⊗ (D_{12}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D_{12}^{⊥}))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}
((C_{11} ⊗ (D_{11}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D_{11}^{⊥}))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} …^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ((C_{2} ⊗ (D_{2}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D_{2}^{⊥}))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (C_{1} ⊗ (D_{1}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} D_{1}^{⊥})))..))
F_{5} D⊗!(D−∘C ⊗ Q)⊗!(D ⊗ Q ⊗ Q−∘I)−∘C⊗?Q
F_{6} D ⊗ D ⊗ D⊗!(D−∘C ⊗ Q)⊗!(D ⊗ Q ⊗ Q−∘I)−∘C ⊗ I ⊗ C
F_{7} D ⊗ D ⊗ D ⊗ D ⊗ Q ⊗ Q⊗!(D−∘C ⊗ Q)⊗!(D ⊗ Q ⊗ Q−∘I)−∘C ⊗ I ⊗ C ⊗ I
F_{8} D ⊗ D ⊗ D ⊗ Q ⊗ Q ⊗ Q⊗!(D−∘C ⊗ Q)⊗!(D ⊗ Q ⊗ Q−∘I)−∘C ⊗ I ⊗ X

Table 8. Some problems for M?LL

F_{i} llprover linseq linres linTAP
F_{1}  0.08 0.02 0.02 < 0.01
F_{2}  61.05 0.17 0.05 0.03
F_{3}  −  0.33 0.08 0.05
F_{4}  −  −  −  0.28

F_{i} llprover linseq linres linTAP
F_{5}  0.95 0.03 0.03 < 0.01
F_{6}  −  0.15 0.05 0.13
F_{7}  −  4.63 0.07 13.67
F_{8}  n/a n/a n/a 11.75

Table 9. Timings for the problems from Table 8

2 Measured on a Sun SPARC10 in seconds; “–” means that no proof was found within 100 seconds. F_{2} is the most difficult example from [24] (linTAP solves all other problems from [24] in less than 30ms); F_{3} is from [23]. The predicates in F_{5} to F_{8} can be interpreted as follows: D=”dollar”, Q=”quarter”, C=”Coke”, I=”ice-cream”. Formula F_{6}, e.g., then expresses the following situation: for one dollar I can buy a Coke and get a quarter back, and for one dollar and two quarters I can buy an ice-cream; so if I have three dollars I can buy two Cokes and one ice-cream (see [5] for a similar approach on deductive planning). It is possible to use (free) variables: formula F_{8} contains a variable X which will be bound to an appropriate predicate symbol (i.e. I) to make the formula valid (only linTAP offers this feature).

3 The linTAP implementation uses an additional technique to simplify formulas of type α of the form F ⊙ω or ω⊙F replacing them by F (where ⊙ ϵ {^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , ⊗, −∘}).

6 Conclusion

We have presented prefix-based tableau calculi for MELL and M?LL. We encoded the additional non-permutabilities arising in multiplicative linear logic by an additional string unification. These calculi are the basis for our tableau prover linTAP. linTAP is not only a very compact implementation but compares favorable with other (larger) implementations. Due to the compact code the program can easily be modified for special purposes or applications.

Future work include the extension to larger fragments of linear logic and the comparison of linTAP with a connection driven proof search procedure (see [15]).

Besides the original leanTAP implementation for classical first-order logic, lean tableau provers are also available for various non-classical logics, i.e. firstorder intuitionistic logic (ileanTAP, [21]), and the propositional modal logics K, KD, KT, and S4 (ModLeanTAP, [4]). The linTAP implementation fills the gap for the multiplicative linear logic. The source code of linTAP can be obtained at

http://www.intellektik.informatik.tu-darmstadt.de/~jeotten/linTAP/.

References

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

2. B. Beckert, J. Posegga. leanTAP: Lean Tableau-Based Theorem Proving. 12^{t}^{h} Conference on Automated Deduction, LNAI 814, pp. 793–797. Springer, 1994.

3. B. Beckert, J. Posegga. leanTAP: Lean Tableau-Based Deduction. Journal of Automated Reasoning, 15 (3), pp. 339–358, 1995.

4. B. Beckert, R. Goré. Free Variable Tableaux for Propositional Modal Logics. Proc. 6^{th} TABLEAUX Conference, LNAI 1227, pp. 91–106, Springer 1997.

5. W. Bibel. Let’s plan it deductively!. In IJCAI-97, Morgan Kaufmann, 1997.

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

7. M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996.

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

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

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

11. V. Gehlot and C. Gunter. Normal process representatives. Sixth Annual Symposium on Logic in Computer Science, pages 200–207, 1991.

12. J.-Y. Girard. Linear logic. TCS, 50:1–102, 1987.

13. J. Harland and D. Pym. Resource-Distribution via Boolean Constraints. 14^{t}^{h} Conference on Automated Deduction, LNCS 1249, pp. 222–236. Springer, 1997.

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. C. Kreitz, H. Mantel, J. Otten, S. Schmitt. Connection-Based Proof Construction in Linear Logic. 14^{t}^{h} Conference on Automated Deduction, LNCS 1249, pp. 207–221. Springer, 1997.

16. P. Lincoln and T. Winkler. Constant-only multiplicative linear logic is NP-complete. TCS, 135:155–169, 1994.

17. H. Mantel, C. Kreitz. A Matrix Characterization for MELL. Logics in Artificial Intelligence, JELIA ’98, LNAI 1489, pp. 169–183, Springer, 1998.

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

19. M. Masseron, C. Tollu, J. Vauzeilles. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS, Springer,1991.

20. D. Miller. FORUM: A Multiple-Conclusion Specification Logic. TCS, 165(1):201-232, 1996.

21. J. Otten. ileanTAP: An Intuitionistic Theorem Prover. Proc. 6^{th} TABLEAUX Conference, LNAI 1227, pp. 307–312, Springer 1997.

22. J. Otten, C. Kreitz. T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. Proc. 5^{th} TABLEAUX Workshop, LNAI 1071, pp. 244–260, 1996.

23. T. Tammet. Proof strategies in linear logic. JAR, 12:273–304, 1994.

24. N. Tamura. User’s Guide of a Linear Logic Theorem Prover (llprover). Technical report. Faculty of Engineering, Kobe University, Japan, 1995.

25. L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.