Proof Search in First-order Linear Logic and Other Cut-free Sequent Calculi

Reprint from: Ninth Annual IEEE Symposium on Logic in Computer Science (LICS’94) to be

held in Paris, France, July 4-8 1994. Also appears in SRI Technical Report CSL-93-11.

P. D. Lincoln^{∗}  N. Shankar^{∗}

lincoln@csl.sri.com               shankar@csl.sri.com

SRI International Computer Science Laboratory 333 Ravenswood Ave

Menlo Park CA 94025 USA

Abstract

We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Herbrand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for firstorder MALL is in nexptime, and first-order MLL is in np. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability.

1 Introduction

Since proofs contain more information than the theorems they prove, the main challenge for automated reasoning is one of automatically finding proofs rather than merely proving theorems. We are therefore more interested in automated proof search than in automated theorem proving. Simply stated, the problem of proof search is to find a proof for a given conjecture.

There is a very simple but impractical approach to proof search: guess a formal proof of the given conjecture and check whether it is a correct proof. This approach is too nondeterministic. For example, it leaves open the choice of the formalism in which the proof is to be generated. We restrict our attention to sequent calculi since most logics can be formalized this way, and sequent calculi have certain structural advantages from the point of view of mechanization. We concentrate on cut-free sequent calculi so as to remove any guesswork regarding the choice of cut formulas. Most sequent calculi do exhibit cut-elimination theorems so that no theorems are lost by this restriction, even though some useful and compact proofs are typically ruled out. The latter disadvantage is outweighed by the ease with which cut-free sequent calculi can be mechanized.

The next level of nondeterminism is in the guessing of the term instantiating an existential quantifier. By employing Herbrand functions and unification, this guesswork can be eliminated. The Herbrand theorem [6] states that a formula A of first-order logic can be transformed into a quantifier-free formula A_{H} such that A is provable if and only if some finite disjunction of instances of A_{H} can be proved in classical propositional logic. The Herbrand theorem yields an effective semi-decision procedure for classical first-order logic, but cannot be applied directly to most logics, including intuitionistic, linear, and modal logics, which typically lack the transformations needed to convert A to A_{H}. The proof search procedures described in this paper eliminate the guesswork in the quantifier rules even in the absence of a Herbrand theorem.

The final level of nondeterminism in proof search has to do with the order in which the inference rules are applied. It is possible for the proof search to succeed with one ordering of the rules, and fail with some other ordering. A proof search procedure might therefore backtrack in order to try all possible orderings of the applicable proof rules. The relative ordering of the quantifier rules in a proof is particularly important because the rule of universal generalization must obey the eigenvariable condition. In many sequent calculi, the relative order of the structural and propositional rules is also crucial to the success of an attempted proof search. The permutability theorems [9] of a sequent calculus indicate when the relative order of two inference rules can be permuted without invalidating a proof. These permutabilities can be exploited to reduce the nondeterminism in the ordering of proof rules.

This paper studies the optimizations that can be applied to proof search in the general setting of cutfree sequent calculi. The point of these optimizations is to reduce the amount of backtracking in proof search. The general ideas are illustrated with the specific case of linear logic because, as is well known, it is possible to embed many logics into linear logic while preserving the structure of proofs [5, 12]. We present a series of proof search procedures for linear logic culminating in one where the permutability properties of linear logic are exploited to introduce an optimized form of dynamic Skolemization^{1} that significantly reduces the amount of nondeterminism in the proof search. The optimization of the quantifier steps in the proof can be very effectively combined with other optimizations that are also based on permutability. We also present the performance results of a Prolog implementation of these search procedures.

∗Work supported under NSF Grant CCR-9224858

The sequent proof search paradigm was previously used to analyze various fragments of propositional linear logic to show the undecidability of propositional linear logic, the pspace-completeness of multiplicative-additive linear logic (MALL), and the np-completeness of multiplicative linear logic (MLL) with unrestricted weakening [10]. Using similar techniques, Kanovich showed that multiplicative linear logic is np-complete [8]. Lincoln and Winkler demonstrated np-completeness of MLL using only the constants [13]. Lincoln and Scedrov had previously shown this fragment of linear logic to be nexptime-hard [11]. By extending this proof search paradigm, we are able to show here that the first-order version of MALL is decidable in nexptime. We also observe that firstorder MLL is np-complete and hence of the same complexity as its propositional counterpart.

The naive form of dynamic Skolemization has been studied by a number of authors. Cerrito [2] presents a related system for linear logic. Shankar [15] presents an optimized form of dynamic Skolemization for the intuitionistic sequent calculus LJ . In this paper, we generalize this technique to arbitrary cut-free sequent calculi with the subformula property and conventional quantifier rules. We also provide rigorous proofs of the soundness and completeness of this procedure for the specific case of linear logic. These proofs can easily be adapted for other cut-free sequent calculi. Finally, we present experimental evidence that the proof systems discussed here directly lead to efficient proof search procedures for linear logic.

2 Proof Search Examples from Linear Logic

Using the proof rules for linear logic given in Appendix B and the standard definition of linear negation, we can illustrate the relevant ideas underlying sequent proof search. A specific instance of a proof rule is called a step. First consider the example of the linear sequent ⊢ (p^{⊥} � q^{⊥}) � (q ⊗ p). This sequent has only one possible cut-free proof, namely

\underline{\overline{⊢ p^{⊥}, p}^{Id} \overline{⊢ q^{⊥}, q}^{Id}}_{⊗}

\underline{⊢ p^{⊥}, q^{⊥}, q ⊗ p}_{�} \underline{⊢ p^{⊥} � q^{⊥}, q ⊗ p} _{�}

⊢ (p^{⊥} � q^{⊥}) � (q ⊗ p)

By the subformula property of cut-free proofs, the � step must be the lowest one in the proof. For the next step of the search, we have a choice between the � rule and the ⊗ rule. It is easy to see that an application of the ⊗ rule at this point causes the proof search to fail, whereas the search succeeds with the application of the � rule below the ⊗ rule. This shows that the ⊗ step cannot always be permuted below the � step.

Next, consider a first-order variant of the above example that is not a theorem: ⊢ (∃x.q^{⊥}(x) � p^{⊥}), (∀y.q(y)) ⊗ p. We have already seen that in any proof of such a formula, the � step must occur below the ⊗ step. By the subformula property, the ∃ step must occur below the � step and the ∀ step must occur above the ⊗ step. The only likely proof is the following:

\underline{\overline{⊢ p^{⊥}, p}^{Id}  \begin{matrix}\overline{⊢ q^{⊥}(c), q(c)} & Id \\ \overline{⊢ q^{⊥}(c), (∀y.q(y))} & ∀ \end{matrix}}_{⊗}
⊢ p^{⊥}, q^{⊥}(c), (∀y.q(y)) ⊗ p
\overline{⊢ p^{⊥} � q^{⊥}(c), (∀y.q(y)) ⊗ p} ^{�}
\overline{⊢ (∃x.p^{⊥} � q^{⊥}(x)), (∀y.q(y)) ⊗ p} ^{∃}

This proof clearly violates the eigenvariable condition because the parameter generalized in the ∀ step appears free in the conclusion of the step. Note that static Skolemization on the conclusion of this proof causes the proof search to (erroneously) succeed. The Skolemized form of the conclusion is ⊢ p^{⊥} � q^{⊥}(v), q(c) ⊗ p, which is easily proved in propositional linear logic when c instantiates v. With the naive form of dynamic Skolemization where quantifiers are replaced by Herbrand variables or functions during the proof search, the proof search rightly fails, as shown below.

⊢ p^{⊥}, p Id

unify fails \overline{⊢ q^{⊥}(v), q(h(v))}

\overline{⊢ q^{⊥}(v), (∀y.q(y))}^{∀} ⊗
⊢ p^{⊥}, q(v)^{⊥}, (∀y.q(y)) ⊗ p
\overline{⊢ p^{⊥} � q^{⊥}(v), (∀y.q(y)) ⊗ p} ^{�}
\overline{⊢ (∃x.p^{⊥} � q^{⊥}(x)), (∀y.q(y)) ⊗ p} ^{∃}

Note that the Herbrand variable v dominates the Herbrand function h since v is introduced below h in the search. The occurs check at the unification fails indicating a potential transgression of the eigenvariable condition. We can also successfully apply dynamic Skolemization to the positive example, ⊢ p^{⊥} � (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p).

1The use of Herbrand functions in proof search is colloquially called Skolemization.

\underline{\overline{⊢ p^{⊥}, p}^{Id}  \{v ← c\} ; \overline{⊢ q^{⊥}(v), q(c)} ; \overline{⊢ (∃x.q^{⊥}(x)), q(c)}^{∃}}_{⊗}

⊢ p^{⊥}, (∃x.q^{⊥}(x)), q(c) ⊗ p

\overline{⊢ p^{⊥}, (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p)}^{∀}
\overline{⊢ p^{⊥} � (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p)} ^{�}

The above form of dynamic Skolemization is still inefficient since it is not flexible relative to the permutabilities of the sequent calculus. For instance, it permits a similar proof search (shown below) with a slightly different order of the rules to fail.

⊢ p^{⊥}, p Id (unify fails) / (\overline{⊢ q^{⊥}(v), q(h(v))}) ⊗

⊢ p^{⊥}, q^{⊥}(v), q(h(v)) ⊗ p

\overline{⊢ p^{⊥}, q^{⊥}(v), (∀y.q(y) ⊗ p)}^{∀}
\overline{⊢ p^{⊥}, (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p)}^{∃}
\overline{⊢ p^{⊥} � (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p)} ^{�}

By paying attention to the permutabilities, it is possible to obtain an optimized form of dynamic Skolemization where even the latter order of proof search can succeed. In this case, the ∃ rule is clearly permutable above the ∀ rule so that the Herbrand function introduced in place of the ∀ quantifier need not depend on the Herbrand variable replacing the ∃ quantifier. The resulting “proof” has the form:

\underline{\overline{⊢ p^{⊥}, p}^{Id}  \{v ← c\} ; \overline{⊢ q^{⊥}(v), q(c)}} _{⊗}

⊢ p^{⊥}, q^{⊥}(v), q(c) ⊗ p

\overline{⊢ p^{⊥}, q^{⊥}(v)), (∀y.q(y) ⊗ p)}^{∀}
\overline{⊢ p^{⊥}, (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p)}^{∃}
\overline{⊢ p^{⊥} � (∃x.q^{⊥}(x)), (∀y.q(y) ⊗ p)} ^{�}

The point here is that even though the unifier is such that the proof search violates the eigenvariable condition, it is possible to permute the steps so as to obtain a valid proof. By thus allowing more of the search paths to succeed, it is possible to reduce the need for backtracking in proof search. We can also check that the same optimized procedure applied to ⊢ (∃x.p^{⊥} � q^{⊥}(x)), (∀y.q(y)) ⊗ p does fail.

⊢ p^{⊥}, p Id

unify fails \overline{⊢ q^{⊥}(v), q(h(v))}

\overline{⊢ q^{⊥}(v), (∀y.q(y))}^{∀} ⊗

⊢ p^{⊥}, q^{⊥}(v), (∀y.q(y)) ⊗ p

\overline{⊢ p^{⊥} � q^{⊥}(v), (∀y.q(y)) ⊗ p} ^{�}
\overline{⊢ (∃x.p^{⊥} � q^{⊥}(x)), (∀y.q(y)) ⊗ p} ^{∃}

Here, since the ∃ quantifier governs the � which is not permutable above the ⊗ governing the ∀, the Herbrand function introduced for the ∀ is dominated by the Herbrand variable replacing the ∃.

The completeness of both dynamic Skolemization and its optimization are straightforward since if there is a proof of the given conjecture, then both search procedures can succeed by nondeterministically applying the inference rules in the same order as the given proof. The soundness of the optimization is somewhat more delicate since it succeeds even when the order of inference rules in the search could violate the eigenvariable condition. We present these search procedures and demonstrate their soundness and completeness. For concreteness, these theorems will be stated in terms of linear logic, but their generalization to other cut-free sequent calculi will be apparent from the proofs. We also obtain complexity results for some first-order fragments of linear logic.

3 Linear Logic

We will be assuming the basic terminology of sequent calculus, linear logic, and unification theory [3, 5]. We will only be dealing with idempotent substitutions U so that U(U(t)) = U(t), for any t. The composition of substitutions will be such that (U ∘ V)(t) = U(V (t)), for any t. A substitution U is less general than V, in symbols U < V, if and only if there exists a W such that U = W ∘V. As our starting point, we use a small variant of linear logic shown in Appendix B where the weakening rule is built into the axiom rule, and the contraction rule is built into the dereliction and ⊗ rules. It is easy to see that the modified system is equivalent to the more conventional presentation of linear logic.

We then modify LL slightly to obtain LLG where each sequent additionally contains a list of free variables T and a substitution U, and the quantifier and Identity rules are modified. The ∃ and ∀ rules have the form

\begin{matrix}\underline{_{\{t/v\}∘U} ⊢_{T ∪\{v\}} A\{v/x\}, Γ} & ∃ \\ _{U} ⊢_{T} (∃x.A), Γ \end{matrix}  \begin{matrix}\underline{_{U} ⊢_{T} A\{h(T)/x\}, Γ} & ∀ \\ _{U} ⊢_{T} (∀x.A), Γ \end{matrix}

where v is a new^{2} Herbrand variable, h is a new Herbrand function, and if T = {v_{1}, …, v_{n}}, then h(T) is h(v_{1}, …, v_{n}) so that each v_{i} in T dominates h. The Id rule is also modified as

\begin{matrix}U(A) ≡ U(B) \\ \overline{_{U} ⊢_{T} ?Γ, A, B^{⊥}} & Id \end{matrix}

where A and B are atomic. The other rules remain unchanged and preserve the parameters U and T from conclusion to premises. For a complete list of proof rules, see Appendix C. The system LLG is introduced only as a step leading to LLV and LLO, which are the systems of real interest.

Let the eigenvariables in LL be labeled a_{1}, …, a_{n}, … and the Herbrand functions in LLG be h_{1}, …, h_{n}, . . .. The notation \underline{Γ} denotes the result of replacing every term of the form h_{i}(…) in Γ by the corresponding a_{i}. Lemma 3.1 If T contains all the free Herbrand variables in Γ, then LL proves ⊢ \underline{U(Γ)} if and only if LLG proves _{U} ⊢_{T} Γ.

2By a new Herbrand variable or Herbrand function, we mean one that does not occur in the input substitution U, the governing Herbrand variables T, or in any of the formulas in the conclusion sequent of the rule.

In LLG, the parameter U is given as an input substitution to the proof search and augmented at every ∃ step. We next introduce another variant LLV where we add another parameter, an output substitution V, so that a sequent in LLV has the form _{U}^{V} ⊢_{T} Γ. The Id rule now has the form

\overline{_{U}^{V} ⊢_{T} ?Γ, A, B^{⊥}}^{Id}

provided V is a unifier for A and B under the substitution U. The binary rules for ⊗ and & are also modified so that a rule of the form \frac{⊢Γ_{1} ⊢Γ_{2}}{⊢Γ} becomes

\frac{_{U}^{W} ⊢_{T} Γ_{1} _{W}^{V} ⊢_{T} Γ_{2}}{_{U}^{V} ⊢_{T} Γ} .

The quantifier rules in LLV have the form:

\begin{matrix}\underline{_{U}^{V} ⊢_{T ∪\{v\}} A\{v/x\}, Γ} & ∃ \\ _{U}^{V} ⊢_{T} (∃x.A), Γ \end{matrix} \begin{matrix}\underline{_{U}^{V} ⊢_{T} A\{h(T)/x\}, Γ} & ∀ \\ _{U}^{V} ⊢_{T} (∀x.A), Γ \end{matrix}

where v and h are new. For a complete list of proof rules, see Appendix D.

Lemma 3.2 If LLV proves _{U1∘U}^{V} ⊢_{T} Γ, then it proves _{U}^{V} ⊢_{T} Γ.

Theorem 3.3

1. If LLG proves _{U} ⊢_{T} Γ, then for some V, LLV proves _{U}^{V} ⊢_{T} Γ.

2. If LLV proves _{U}^{V} ⊢_{T} Γ, then for some W, LLG proves _{W} ⊢_{T} Γ.

3.1 Complexity Results

Using LLV, the multiplicative-additive fragment of first-order linear logic (MALL1) can be shown to be decidable in nexptime. This follows from the fact that any MALL1 proof has a depth that is bounded by the number of connectives in the conclusion. This means that the number of axiom nodes in such a proof is bounded by an exponential in the size of the conclusion. Since LLV introduces a Herbrand term of the form h(T) for each universal quantifier in the conclusion, where T is itself bounded by the number of existential quantifiers in the conclusion, each axiom sequent is at most quadratic in the size of conclusion. Since unification is linear [14], one can build a nondeterministic procedure to guess and check a proof in time that is exponential in the size of the conclusion. Lincoln and Scedrov [11] have shown that the decidability of MALL1 is nexptime-hard so we now have a tight bound on the complexity. Theorem 3.4 MALL1 is nexptime-complete.

The multiplicative fragment of first-order linear logic (MLL1) can be shown to be decidable in np by the same method. The number of axiom nodes in a MLL1 proof is linear in the size of the conclusion, and each axiom node in the search has size at most quadratic in the size of the conclusion. This results in a tight bound since the propositional fragment MLL is np-complete [8]. Theorem 3.5 MLL1 is np-complete.

4 An Optimization

We now present an optimization of LLV called LLO that exploits the permutabilities of linear logic. As is clear from the table in Appendix A, there are only a few pairs of impermutable rules in LL. A rule R1 is said to be impermutable below R2, that is R1/R2, if there is a Γ such that the principal formulas of R1 and R2 occur as distinct formulas in Γ, but ⊢ Γ can only be proved with R2 below R1. Otherwise, R1 is said to be permutable below R2, or equivalently, R2 is permutable above R1. One way to exploit the permutabilities is to restrict the backtracking in proof search to those rules that might not permute below others [1]. As we have already seen, the permutabilities can also be used to reduce the dependencies between Herbrand variables and Herbrand functions. For any impermutability R1/R2, if an R2 step occurs below an R1 step in the proof search, then the Herbrand variables governing the principal formula of the R2 step should also govern the principal formula of the R1 step. A Herbrand variable introduced in place of the existential quantifier in (∃x.A) also governs all subformulas of A in the proof. A Herbrand variable governs a formula if it dominates all the Herbrand functions replacing universal quantifiers in subformulas of the given formula in the proof.

In LLV, a universal quantifier is replaced by an application of a new Herbrand function to all the Herbrand variables that happen to have been introduced at that point in the proof. The point of the optimized system LLO is to reduce the set of Herbrand variables used in this construction to only those Herbrand variables which necessarily govern the universal formula. In a formula like (∃x.P (x)) � (∀y.P^{⊥}(y)) a possible LLO proof proceeds by reducing �, then ∃, and then ∀. This proof is not acceptable in LLV, as the Herbrand variable replacing x would appear in the term replacing y, causing occur-check failure of unification. However, LLO is sensitive to the fact that the Herbrand variable replacing x does not govern the universal term. The key property is that the LLO proof could have been carried out in such a way that the existential formula was reduced above the universal one. Another way to view this is that the LLV impermutability ∃/∀ has been eliminated in LLO.

This optimization is important because proof search may succeed more quickly on true theorems as there are fewer failures of unification, and thus it is more likely in nondeterministic proof search, to find a successful proof. For example, in the pure multiplicative fragment, all quantifier rules can be applied immediately. This is in contrast to LLV where one must try all possible orderings of the quantifier rules.

One way to track the dependencies between impermutable rules is to maintain a set of Herbrand variables corresponding to every pair of impermutable rules. Since only three rules !S, �, and & occur in the R2 position of any LL impermutabilities of the form R1/R2, where R1 is not !S, it is sufficient to maintain three sets of variables R, S, and T, and treat !S specially. A sequent in LLO therefore consists of the two substitutions U and V, and three sets of variables: R, the set of !S Herbrand variables, S, the � Herbrand variables, and T, the & Herbrand variables. In addition, each sequent formula is decorated with the Herbrand variables that govern it. The quantifier rules have the form

\begin{matrix}\underline{_{U}^{V} ⊢_{R,S,T} Γ, [XvT : A\{v/x\}]} & ∃ \\ _{U}^{V} ⊢_{R,S,T} Γ, [X : (∃x.A)] \end{matrix} ; \begin{matrix}\underline{_{U}^{V} ⊢_{R,S,T} Γ, [X : A\{h(X)/x\}]} & ∀ \\ _{U}^{V} ⊢_{R,S,T} Γ, [X : (∀x.A)] \end{matrix}

where v and h are new. The ∃ rule encodes the fact that the formula A is governed by the newly introduced Herbrand variable v and by those Herbrand variables that govern any & connective that is analyzed below the ∃ steps, thus encoding the impermutability ∃/ & . The ∀ rule is more straightforward. The other rules similarly encode the various impermutabilities by suitably augmenting either the sets R, S, or T, or the variable sets that are local to the sequent formulas.

The completeness of LLO is established by the following lemma which can be proved by induction on LLV proofs.

Theorem 4.1 Let Γ be of the form A_{1}, …, A_{n}. If LLV proves _{U}^{V} ⊢_{T′} Γ, then for any R, S, T, X_{1}, …, X_{n} ⊆ T′, there exists a W such that LLO proves _{U}^{W} ⊢_{R,S,T} [X_{1} : A_{1}], …, [X_{n} : A_{n}].

We outline the soundness argument, and refer to a forthcoming full paper for the details. To prove the soundness of LLO, we need to show that when the LLO proof search succeeds and returns a unifier V, then the original goal sequent is provable in LL. The main obstacle is that if LLO proves a sequent, the resulting “proof” can contain violations of the eigenvariable condition in the following sense: the conclusion _{U}^{V} ⊢_{R,S,T} [X : (∀x.A)], Γ of a ∀ step introducing the Herbrand function h can be such that V (Γ) contains occurrences of h. This must be because some Herbrand variable v in Γ is introduced by an ∃ step that occurs below the ∀ step introducing h, where V (v) contains h. Let such an ∃ step be labeled bad, and let a proof containing bad ∃ steps be labeled a bad proof. We clearly need to permute the order of such quantifier steps in order to rid the given LLO proof of bad ∃ steps to construct an LL proof.

We will be constructing the LL proof by induction on the structure of the given LLO proof. The LL proof is constructed by applying permutations to the LL subproofs obtained from the induction hypothesis. We therefore need to keep track of which inference steps in the constructed LL proof remain permutable. This information is actually implicit in the original LLO proof. We therefore set up a correspondence between the steps in the LLO proof and those in the resulting LL proof. This many-to-many correspondence is preserved by the permutations. It is possible to obtain a strict partial ordering on the steps in the given LLO proof so that step Q1 < Q2 if and only if one of the following is true in the LLO proof:

1. Q1 occurs below Q2 and Q2/Q1 is an LL impermutability.

2. The principle formula of Q2 is a subformula of Q1.

3. Q1 is a ∀ step introducing Herbrand function h, and Q2 is an ∃ step introducing Herbrand variable v, where V (v) contains h.

4. There is some Q3 such that Q1 < Q3 and Q3 < Q2.

We show that it is possible to construct an LL proof from a given LLO proof that is consistent with the above strict partial ordering so that any steps Q1′ and Q2′ in the LL proof corresponding to Q1 and Q2 in the LLO proof, Q2′ occurs below Q1′ whenever Q1 < Q2. Furthermore, if Q1′ and Q2′ in the LL proof are such that we have for the corresponding steps in the LLO proof that Q1 ≮ Q2, then Q1′ is permutable above Q2′ in the LL proof. Note that an LL proof consistent with the strict partial ordering does not contain any bad ∃ steps.

In constructing the LL proof by induction on structure of the given LLO proof, we only examine the case when the concluding inference in the LLO proof is an ∃ step since the other cases are straightforward. We therefore suppose that we are given an LLO proof of the form

Π

\underline{_{U}^{V} ⊢_{R,S,T} A\{v/x\}, Γ}_{∃}
_{U}^{V} ⊢_{R,S,T} (∃x.A), Γ

where the concluding ∃ step is bad in that V (v) contains occurrences of Herbrand functions introduced by ∀ steps in Π. We label the latter ∀ steps as injured by the bad ∃ step. By induction, we can construct an LL proof Π′ from Π that is consistent with the strict partial ordering derived from the LLO proof and hence, does not contain any bad ∃ steps. Every proof step Q′ in Π′ (corresponding to Q in Π) that occurs above this bad ∃ step and below any corresponding injured ∀ step is either permutable below the bad ∃ step (a low step) or above the injured ∀ step (a high step), since otherwise, we would have a cycle in the LLO proof of the form ∀ < ∃ < Q < ∀ thus violating the strictness of the partial order. It is clear that the high steps must be permuted above the injured ∀ steps, and the low steps and the injured ∀ steps must be permuted below the bad ∃ step. In performing the above permutations, it should be noted that certain permutations introduce copies of subproofs. For example, the permutation of a ⊗ step above a & step copies one of the subproofs of the ⊗ step. For example, proofs of the form

\begin{matrix}\underline{\begin{matrix}\underline{⊢ A, C, Σ ⊢ A, D, Σ} & & \\ ⊢ A, C & D, Σ \end{matrix} ⊢ B, Δ} & ⊗ \\ ⊢ A ⊗ B, C & D, Σ, Δ \end{matrix}

can be permuted to the form

\begin{matrix}\underline{⊢ A, C, Σ ⊢ B, Δ} & ⊗ \\ ⊢ A ⊗ B, C, Σ, Δ \end{matrix}  \begin{matrix}\underline{⊢ A, D, Σ ⊢ B, Δ} & ⊗ \\ ⊢ A ⊗ B, D, Σ, Δ \end{matrix} & ⊢ A ⊗ B, C & D, Σ, Δ

At the cost of duplicating the proof of ⊢ B, Δ. For structural reasons, this kind of duplication of subproofs can only arise when a binary (2-premise) rule is permuted above another binary rule.

Since the permutation of binary steps can introduce duplication of subproofs, the permutation of bad proofs into good ones must be done carefully to achieve termination. In the first stage of the procedure, the binary high steps are permuted above the injured ∀ steps, with the highest binary high step first, so that no high binary steps below an injured ∀ are duplicated in the process. All the high binary steps can be eliminated in this manner, but this might create duplicates of the injured ∀ steps or the low steps. Next, we permute all the low binary steps below the bad ∃ step, with the lowest low steps first in order to avoid duplication of the low binary steps. This last step could create copies of the bad ∃ step. The only remaining high and low steps are unary steps. It is easy to permute these unary steps so that we get an LL proof of _{U}^{V} ⊢_{R,S,T} (∃x.A), Γ that does not contain any bad ∃ steps. No bad ∃ steps are introduced by these permutations since each permutation preserves the consistency of the strict partial ordering derived from the LLO proof.

Given an LLO sequent _{U}^{V} ⊢_{R,S,T} Γ, let \underline{_{U}^{V} ⊢_{R,S,T} Γ} represent the LL sequent ⊢ \underline{V (A_{1})}, …, \underline{V (A_{n})}, for each [X_{i} : A_{i}] in Γ, where \underline{B} represents the result of replacing each Herbrand term of the form h_{i}(…) in B by the corresponding eigenvariable a_{i}. The following lemmas are proved by induction on LLO proofs.

Lemma 4.2 Given any idempotent substitution U, and an LLO proof of _{U}^{V} ⊢_{R,S,T} Γ, there is a strict partial ordering on the steps in this proof respecting the subformula property, the eigenvariable condition, and the impermutabilities in this proof.

Lemma 4.3 An LLO proof of _{U}^{V} ⊢_{R,S,T} Γ can be transformed to an LL proof of \underline{_{U}^{V} ⊢_{R,S,T} Γ} with no bad ∃ steps but with possible violations of the eigenvariable condition.

The soundness theorem is an easy consequence of the above lemma.

Theorem 4.4 If Γ does not contain any Herbrand functions or variables, then an LLO proof of _{U}^{V} ⊢_{R,S,T} Γ can be transformed to an LL proof of \underline{_{U}^{V} ⊢_{R,S,T} Γ}.

The soundness argument as outlined above is quite general and applies to any cut-free sequent calculus with the subformula property and conventional quantifier rules.

4.1 Other Cut-Free Sequent Calculi

One can generate a dynamic skolemization system along the lines of LLV for many other sequent calculi. For sequent calculi with cut-elimination theorem, subformula property, and the usual quantifier rules, one can replace the quantifier rules with the quantifier rules of LLV, decorate every sequent with set of governing variables, and input and output unifiers, and allow unification at any identity-like rules (that is, any rules requiring two formulas to be identical). The resulting LLV-like system replaces the guesswork of the usual existential rule with unification. Thus any cutfree first-order sequent system with the subformula property, the usual quantifier rules, and some finite depth bound on the sequent proof tree is decidable. Note that full linear logic (with !,?), relevance logic, first-order intuitionistic logic, and first-order classical logic, do not exhibit a finite depth bound on sequent proofs, due to the contraction rule. However, a proof system like LLV may still be of direct interest when considering logic programming in non-classical sequent systems.

It is also straightfoward to generate an optimized sequent system along the lines of LLO for any firstorder cut-free sequent-calculi with the subformula property and the usual quantifier rules. The process begins with the analysis of the propositional permutabilities (such as displayed in Appendix A for linear logic). Then for each R2 rule (rules which do not always permute upward) a list of variables is created (like the R,S, and T for !S, �, and & in LLO). Then for each rule R2, for each rule R1 that does not permute below R2, the R2 variables are added to the governing variables of the subformulas of the principal formula. A system generated in this way will have no quantifier impermutabilities.

5 Implementation

We have implemented Prolog proof search procedures for the constant-free multiplicative-additive fragments of LLV, LLO, and a version of LLO called LLOpt where we have optimized the backtracking to exploit some propositional permutabilities. These optimizations are similar to those proposed by Andreoli [1], Galmiche and Perrier [4], Hodas and Miller [7], and Tammet [16]. The combination of LLO with optimizations based on propositional permutabilities is a delicate matter. The usual optimization is that if we have a rule R2 that is always permutable below any other rule, then it is safe to apply this rule immediately in the proof search. In the context of LLO, this would mean that for an impermutability R1/R2, the Herbrand variables governing R2 would always govern R1 so that proof attempts that might have succeeded with R1 below R2 now fail because of the occur check. For instance, given the provable sequent ⊢ (∃x.p(x) � q(x)), r, (r^{⊥} ⊗ (∀y.p^{⊥}(y) ⊗ (^{⊥}q(y)))), the LLO proof search fails if the � step occurs below all the ⊗ steps.

The LLO search procedure backtracks on all the rules. We can optimize this to avoid backtracking on �, ∀, and & rules provided there is backtracking on applications of the ∃ rule. The � and ∀ steps can be applied immediately, but immediate reductions of the & steps could lead to larger proofs. The most significant optimization is in the treatment of the ⊗ rule. LLO tries all possible partitions of the context, whereas it turns out to be far more effective to allow the left branch of the rule to use up some part of the context and to pass along the unused part of the context to the right branch of the ⊗ rule.

We show the timings for these procedures on some theorems and non-theorems in order to demonstrate the efficacy of the above optimizations. We first compare these procedures on provable sequents of the form ⊢ p^{⊥}, (∃x.q_{1}^{⊥}(x)), …, (∃x.q_{n}^{⊥}(x)), (∀x.q_{1}(x)⊗ … q_{n}(x) ⊗ p), for n = 1, 2, 3, 4. The run times are given to the nearest millisecond on BINProlog on a Sparcstation 10-41. The Prolog code is anonymously FTPable from FTP.CSL.SRI.COM in the file

pub/shankar/mall.pl.

n  LLV  LLO LLOpt
1  17  0  0
2  200  0  0
3 10433  17  0
4 1117383 83  17

The table above does not sufficiently emphasize the utility of LLOpt over LLO since there is a small overhead cost for LLOpt over LLO. The value of LLOpt is more apparent when the same experiment is attempted with the unprovable sequent ⊢ p^{⊥}, (∃x.q_{1}^{⊥}(x)), …, (∃x.q_{n}^{⊥}(x)), (∀x.q_{1}(x) ⊗ … q_{n}(x) ⊗ r), for n = 1, 2, 3, 4.

n LLV LLO LLOpt
1  33  17  0
2 916  1700  83
3 80783 199634 1300
4  -  -  33300

Note that in the case of a failed proof search, LLO actually performs worse than LLV because both procedures carry out the same search but LLO has the additional overhead of tracking impermutabilities. Note also that we have deliberately ordered the sequent so as to trigger the worst backtracking behavior with LLV in order to compare the worst-case performances of these procedures. Several further optimizations are currently being studied.

6 Conclusion

We have presented some optimized proof search procedures that can be applied to a wide variety of cut-free sequent calculi. We have presented rigorous informal arguments for the soundness and completeness of these optimizations. These optimized search procedures have been naively implemented in Prolog. The full paper will contain more informative versions of the proofs and more detailed empirical comparisons of the various optimizations. Acknowledgments. We thank Sam Owre, Dale Miller, Andre Scedrov, Gopalan Nadathur, and James Harland for their help and guidance, and Serenella Cerrito for sharing an early draft of her paper [2] with us.

References

[1] J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992. To appear.

[2] S. Cerrito. Herbrand methods in linear logic. 1992.

[3] C.-L. Chang and R.C-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

[4] D. Galmiche and G. Perrier. Foundations of proof search strategies design in linear logic. In Symposium on Logical Foundations of Computer Science, St. Petersburg, 1994. To appear.

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

[6] J. Herbrand. Investigations in proof theory. In J. van Heijenoort, editor, From Frege to Gödel: A Sourcebook of Mathematical Logic, 1879–1931, pages 525–581. Harvard University Press, Cambridge, MA, 1967. First published 1930.

[7] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 32–42. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Information and Computation.

[8] M. Kanovich. Horn programming in linear logic is NPcomplete. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 200– 210. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[9] S.C. Kleene. Permutability of inferences in Gentzen’s calculi LK and LJ. Memoirs of the AMS, 1952.

[10] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals Pure Appl. Logic, 56:239–311, 1992. Special Volume dedicated to the memory of John Myhill.

[11] P. Lincoln and A. Scedrov. First order linear logic without modalities is NEXPTIME-hard. To Appear in TCS, 1993. Available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/mall1.dvi.

[12] P. Lincoln, A. Scedrov, and N. Shankar. Linearizing intuitionistic implication. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 51–62. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Annals of Pure and Applied Logic.

[13] P. Lincoln and T. Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. To Appear in TCS, 1993.

[14] A. Martelli and U. Montanari. An efficient unification algorithm. ACM Trans. on Prog. Lang. and Systems, 4(2), Feb. 1982.

[15] N. Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, Automated Deduction: CADE-11, volume 607 of lncs, pages 522–536, Berlin, 1992. Springer-Verlag.

[16] T. Tammet. Proof search strategies in linear logic. Programming Methodology Group Report 70, Chalmers University, 1993.

A LL Permutabilities

An impermutability R1/R2 is represented in the table below on column labeled R1 and row labeled R2. For example ⊗/ � is indicated by the numeral 1. A numeral in the table should be read as “the connective of this column cannot always permute below the connective of this row”. Below the table are a short list of examples of sequents which exhibit each impermutability. Impermutability 7 is present in most firstorder logics. Classical logic enjoys all other possible permutabilities.

⊗ � & ⊕ ?D ! ⊥ ∀ ∃
⊗  0
�  1  0
& 2  3 4 0  5

?D

!  6
⊥  0
∀ 0 7
∃  0
0 various examples
1 ⊢ (A � B), (A^{⊥} ⊗ B^{⊥})
2 ⊢ (A&B), (⊥ ⊗ ⊤), A^{⊥}, B^{⊥}
3 ⊢ (A&B), (A^{⊥} ⊕ B^{⊥})
4 ⊢ ((!A)&A),?A^{⊥}
5 ⊢ (A(t)^{⊥}&A(u)^{⊥}), ∃x.A(x)
6 ⊢!(A^{⊥} ⊕ B),?A
7 ⊢ ∀y.(A(y) ⊕ B), ∃x.A(x)^{⊥}

B LL Proof Rules

I  \overline{⊢?Δ, A, A^{⊥}}

Cut  \frac{⊢ Σ, A  ⊢ Γ, A^{⊥}}{⊢ Σ, Γ}

⊗  \frac{⊢?Δ, Σ, A  ⊢?Δ, B, Γ}{⊢?Δ, Σ, (A ⊗ B), Γ}

�  \frac{⊢ Σ, A, B}{⊢ Σ, (A � B)}

⊕ \begin{aligned}⊢ Σ, A & ⊢ Σ, B \\ ⊢ Σ, (A ⊕ B) & ⊢ Σ, (A ⊕ B) \end{aligned}

&  \frac{⊢ Σ, A  ⊢ Σ, B}{⊢ Σ, (A & B)}

?D  \frac{⊢ Σ,?A, A}{⊢ Σ,?A}

!S  \frac{⊢?Σ, A}{⊢?Σ,!A}

⊥  \frac{⊢ Σ}{⊢ Σ, ⊥}
1  \overline{⊢?Δ, 1}
⊤  \overline{⊢ Σ, ⊤}

∀  \frac{⊢ Σ, A\{a/x\}}{⊢ Σ, ∀x.A}

∃  \frac{⊢ Σ, A\{t/x\}}{⊢ Σ, ∃x.A}

C LLG Proof Rules

I  \frac{U(A) ≡ U(B)}{_{U} ⊢_{T}?Δ, A, B^{⊥}}

Cut  \frac{_{U} ⊢_{T} Σ, A  _{U} ⊢_{T} Γ, A^{⊥}}{_{U} ⊢_{T} Σ, Γ}

⊗  \frac{_{U} ⊢_{T}?Δ, Σ, A  _{U} ⊢_{T}?Δ, B, Γ}{_{U} ⊢_{T}?Δ, Σ, (A ⊗ B), Γ}

�  \frac{_{U} ⊢_{T} Σ, A, B}{_{U} ⊢_{T} Σ, (A � B)}
⊕ \begin{matrix}_{U} ⊢_{T} Σ, A & _{U} ⊢_{T} Σ, B \\ _{U} ⊢_{T} Σ, (A ⊕ B) & _{U} ⊢_{T} Σ, (A ⊕ B) \end{matrix}

&  \frac{_{U} ⊢_{T} Σ, A  _{U} ⊢_{T} Σ, B}{_{U} ⊢_{T} Σ, (A & B)}
?D  \frac{_{U} ⊢_{T} Σ,?A, A}{_{U} ⊢_{T} Σ,?A}
!S  \frac{_{U} ⊢_{T}?Σ, A}{_{U} ⊢_{T}?Σ,!A}
⊥  \frac{_{U} ⊢_{T} Σ}{_{U} ⊢_{T} Σ, ⊥}
1  \overline{_{U} ⊢_{T}?Δ, 1}
⊤  \overline{_{U} ⊢_{T} Σ, ⊤}

∀  \frac{_{U} ⊢_{T} Σ, A\{h(T)/x\}}{_{U} ⊢_{T} Σ, ∀x.A}

∃  \frac{_{\{t/v\}∘U} ⊢_{T ∪\{v\}} A\{v/x\}, Σ}{_{U} ⊢_{T} Σ, ∃x.A}

D LLV Proof Rules

I  \overline{_{U}^{mgu(A,B,U)} ⊢_{T}?Δ, A, B^{⊥}}

⊗ \frac{_{U}^{W} ⊢_{T}?Δ, Σ, A _{W}^{V} ⊢_{T}?Δ, B, Γ}{_{U}^{V} ⊢_{T}?Δ, Σ, (A ⊗ B), Γ}

�  \frac{_{U}^{V} ⊢_{T} Σ, A, B}{_{U}^{V} ⊢_{T} Σ, (A � B)}

⊕  \frac{_{U}^{V} ⊢_{T} Σ, A}{_{U}^{V} ⊢_{T} Σ, (A ⊕ B)}

⊕  \frac{_{U}^{V} ⊢_{T} Σ, B}{_{U}^{V} ⊢_{T} Σ, (A ⊕ B)}

&  \frac{_{U}^{W} ⊢_{T} Σ, A _{W}^{V} ⊢_{T} Σ, B}{_{U}^{V} ⊢_{T} Σ, (A & B)}

?D  \frac{_{U}^{V} ⊢_{T} Σ,?A, A}{_{U}^{V} ⊢_{T} Σ,?A}

!S  \frac{_{U}^{V} ⊢_{T}?Σ, A}{_{U}^{V} ⊢_{T}?Σ,!A}

⊥  \frac{_{U}^{V} ⊢_{T} Σ}{_{U}^{V} ⊢_{T} Σ, ⊥}
1  \overline{_{U}^{U} ⊢_{T} 1}
⊤  \overline{_{U}^{U} ⊢_{T} Σ, ⊤}

∀  \frac{_{U}^{V} ⊢_{T} Σ, A\{h(T)/y\}}{_{U}^{V} ⊢_{T} Σ, ∀y.A}

∃  \frac{_{U}^{V} ⊢_{T ∪\{v\}} Σ, A\{v/y\}}{_{U}^{V} ⊢_{T} Σ, ∃y.A}

E LLO Proof Rules

I  \overline{_{U}^{mgu(A,B,U)} ⊢_{R,S,T}?Δ, [X : A], [Y : B^{⊥}]}

⊗ \frac{_{U}^{W} ⊢_{R,S,T}?Δ, Σ, [XST : A] _{W}^{V} ⊢_{R,S,T}?Δ, [XST : B], Γ}{_{U}^{V} ⊢_{R,S,T}?Δ, Σ, [X : (A ⊗ B)], Γ}

�  \frac{_{U}^{V} ⊢_{R,S∪X,T} Σ, [X : A], [X : B]}{_{U}^{V} ⊢_{R,S,T} Σ, [X : (A � B)]}

⊕  \frac{_{U}^{V} ⊢_{R,S,T} Σ, [XT : A]}{_{U}^{V} ⊢_{R,S,T} Σ, [X : (A ⊕ B)]}

⊕  \frac{_{U}^{V} ⊢_{R,S,T} Σ, [XT : B]}{_{U}^{V} ⊢_{R,S,T} Σ, [X : (A ⊕ B)]}

&  \frac{_{U}^{W} ⊢_{R,S,T ∪X} Σ, [X : A] _{W}^{V} ⊢_{R,S,T ∪X} Σ, [X : B]}{_{U}^{V} ⊢_{R,S,T} Σ, [X : (A & B)]}

?D  \frac{_{U}^{V} ⊢_{R,S,T} Σ, [X :?A], [XT R : A]}{_{U}^{V} ⊢_{R,S,T} Σ, [X :?A]}

!S  \frac{_{U}^{V} ⊢_{R∪X,S,T}?Σ, [Y : A]}{_{U}^{V} ⊢_{R,S,T}?Σ, [X :!A]}

⊥  \frac{_{U}^{V} ⊢_{R,S,T} Σ}{_{U}^{V} ⊢_{R,S,T} Σ, [X : ⊥]}

1  \overline{_{U}^{U} ⊢_{R,S,T} [X : 1]}

⊤  \overline{_{U}^{U} ⊢_{R,S,T} Σ, [X : ⊤]}

∀  \frac{_{U}^{V} ⊢_{R,S,T} Σ, [X : A\{h(X)/y\}]}{_{U}^{V} ⊢_{R,S,T} Σ, [X : ∀y.A]}

∃  \frac{_{U}^{V} ⊢_{R,S,T} Σ, [XvT : A\{v/y\}]}{_{U}^{V} ⊢_{R,S,T} Σ, [X : ∃y.A]}

Where h is new in the ∀ rules, v is new in the ∃ rules, and mgu(A, B, U) returns the composition with U of a most general unifier of U(A) and U(B). The Y governing the formula A in the hypothesis of the !S rule is the union of S, T, and every Z such that [Z : B] occurs in the conclusion.