Foundations of Proof Search Strategies Design in Linear Logic^{∗}

D. Galmiche and G. Perrier

CRIN-CNRS & INRIA Lorraine Campus Scientifique - B.P. 239 54506 Vandœuvre-les-Nancy Cedex France e-mail: galmiche{perrier}@loria.fr

Abstract

In this paper, we investigate automated proof construction in classical linear logic (CLL) by giving logical foundations for the design of proof search strategies. We propose common theoretical foundations for top-down, bottom-up and mixed proof search procedures with a systematic formalization of strategies construction using the notions of immediate or chaining composition or decomposition, deduced from permutability properties and inference movements in a proof. Thus, we have logical bases for the design of proof strategies in CLL fragments and then we can propose sketches for their design.

1 Introduction

Linear Logic is a powerful and expressive logic with connections to various topics in computer science as logic programming [9, 10], concurrency [12] or typed concurrent functional programming [1]. For these applications in various fragments of Classical Linear Logic (CLL), it is important to propose efficient proof search procedures knowing that theorem proving is significantly more difficult for CLL than for classical logic since there is no convenient normal forms. Some works have been devoted to theorem proving and decision procedures in such fragments [4, 5, 11, 14] and to linear logic programming [2, 8, 9], including various notions or proposals, mainly with a bottom-up approach. Considering proof construction in linear sequent calculus, regardless of proof direction, we point out the necessity to systematically study permutability properties because they can justify nondeterminism reduction (inference application order) and support efficient proof search strategies proposals by defining, for example, complete and tractable subclasses of normal proofs. Thus, it appears that notions as inference movement, proof transformation and normal proof are logical foundations for the conception of proof search strategies [5, 6]. In previous works, we have worked on an automated deduction procedure in the MALL fragment with a bottom-up approach by defining complete and tractable subclasses of proofs [5]. But what about logical bases for bottom-up, top-down or mixed proof directions in full linear logic ? In this paper, we propose common theoretical foundations of proof search procedures, for a given direction, with a systematic formalization of strategies construction using the notions of immediate or chaining composition or decomposition. At first, we analyze non-determinism factors and then propose, from permutability analysis, results about the immediate decomposition and chaining decomposition principles which are bases for bottom-up proof search design and in a dual way (duality is an important point in CLL), we do the same for the top-down approach with results on immediate and chaining composition principles. Then, we have a global logical analysis that leads to finer strategies, depending on the fragment and on the proof direction. Moreover, it allows to study fruitful combinations of them. The compromise between expressiveness and efficiency of proof search for a given fragment can be analyzed from these results. Thus, we have logical bases for the design of proof strategies in fragments of CLL and then we can propose sketches for their design. Adaptations or proposals for other proof methods in CLL, their relationships, mixing or optimization would be considered from these results.

∗International Symposium on Logical Foundations of Computer Science, Logic at St. Petersburg ’94, Lecture Notes in Computer Science 813, pp 101-113

2 Permutability properties in CLL proofs

Linear logic (LL) is a logic of actions, introducing notions like controlled and strict resource management [7]. The language and the inference system are given in appendix A. Considering proof search in this linear sequent calculus, we observe the necessity to study permutability properties of inferences because they can justify non-determinism reduction (inference application order) and support efficient proof search strategies proposals [13, 15]. They are partially used in works on proof search analysis [3] but often without a precise definition. Intuitively, it means the possibility to invert two inferences in a proof without disturbing the rest of the proof (the parts below and above the inferences). We have proposed a corresponding formal definition and we have studied the permutability properties in full linear logic [6] (see appendix B). Let us precise some definitions to consider permutation potentialities.

Definition 2.1 (i) A principal formula of an inference is a formula of the conclusion that is not in the premises. (ii) The principal part of an inference I is the multiset of its principal formulas. (iii) An active formula of an inference is a formula in a premise that is not in the conclusion. (iv) The active part of an inference premise is the multiset of its active formulas.

(v) The context of an inference premise is the complement of its active part.

Having defined inference permutation, it is natural to iterate it upwards or downwards and to study up and down inference movements in a proof. The up movement in a proof is not a linear sequence of permutations. Each time the inference moving up crosses an inference of & type, it is divided into two inferences that have their own movement. Then, many inferences move up in distinct branches of the proof tree. The down movement being the reverse operation of the previous one, we have the opposite phenomenon that is the contraction of several inferences into one, depending on the number of & inferences crossed downwards.

3 Proof transformation and strategies

From permutability properties we can order the inferences inside a proof by sequences of up and down movements. The principal aim consists in reducing the non-determinism during the proof search of a given sequent by defining adequate proof forms that can define complete and tractable proof subclasses.

3.1 Choice criteria for inference movement

How to determine which inference can be moved up or down ? A first criterion is the facility to do it and we can have some ideas about it by analyzing the permutation results. Thus, the inference types ℘, &, ∀, w? and ⊥ can be easily moved down and the inference types cut, ⊗, ⊕, w? and ∃ can be easily moved up. In a particular fragment, the behavior of the inference types can change as well as the movement possibilities. For example, in a fragment without &, the inferences of ⊕ type are no more blocked in the down movement, that might be interesting for a bottom-up strategy. Moreover, in a fragment without !, the inferences of ⊕, ⊗ and ∃ are not blocked in an up movement. A second criterion is the direction of proof search because some inferences are as easy to move up as to move down. For a top-down construction it would be better to move up the inferences that we are able to determine from their premises and to move down the others. For a bottom-up construction, it would be better to move down inferences that we are able to choose from their conclusion. For illustration, the conclusion of c? gives no information to know if it is a contraction but it is not the case for the premises where we have necessarily a formula with ? as principal operator and that is duplicated. Thus, for opposite reasons, we have to move up as far as possible the contractions in proof, either with bottom-up or top-down strategy.

3.2 How far to move an inference ?

When we have fixed the inference type we want to move up in a proof, we can ask what does it mean to move up or down an inference as far as possible ? For up movement, we have three cases, i.e., (i) The inference I, during the movement, meets an inference with which it is in permutation position but it is not permutable. (ii) The active part of the premise of I, which is in the branch where we try to move up I, is not empty and I is blocked by an inference which introduces one of its active formulas. (iii) The active part of the premise of I, which is in the branch where we try to move up I, is empty and I can be moved up to the axioms. For down movement, we have dual conditions, i.e, (i′) The inference I, during the movement, meets an inference with which it is in permutation position but it is not permutable. (ii′) The principal part of I is not empty and I is blocked by an inference where its principal formula becomes active. (iii′) The principal part of I is empty and I can be moved down to the bottom of the proof. It is similar when the principal part of I is in the proof conclusion. In fact, we cannot consider separately these up and down movements and thus have to examine the coherence between these dual movements, i.e., how the effect of a movement can be destroyed by another movement.

4 Composition and decomposition principles

Taking into account the previous analysis, we will always try to move inferences up just after the inferences producing their active formulas. It leads, during a bottom-up construction process to the chaining decomposition notion: when we try to decompose a formula we go on by decomposing its components (focusing [2, 5] and backchaining [9] notions propose similar treatment). In a top-down construction, it leads to the immediate composition notion: when the components of a formula appear in intermediate conclusions we can apply the inference introducing it immediately. In a dual way, we will always try to place the inferences to move down immediately before the inferences using their principal formulas as active formulas. It leads, during the bottom-up construction, to the immediate decomposition notion: when a formula of a certain type appears in a goal it can immediately be decomposed (invertibility notion [14] is also a justification). In a top-down construction, it leads to the chaining composition notion: when we start to compose a formula we go on in composing the formula from which it is an immediate subformula.

4.1 Chaining decomposition

We apply this principle to inferences that are easy to move up in a bottom-up manner, i.e, the ones of type ⊗, ⊕_{1}, ⊕_{2}, ∃ and ? that can be blocked by ! inferences, except ?.

Theorem 4.1 (chaining decomposition 1) Let Π be a proof of ⊢ F, Δ′ and F is produced by an inference of type ⊗, ⊕_{1}, ⊕_{2}, ∃, ? there exists a proof of ⊢ F, Δ′ where the inferences introducing F are immediately preceded by the inferences producing their active formulas when they do not have ? as principal operator.

In a bottom-up strategy it is impossible to predict a priori the contractions we have to do. It is judicious to do them as late as possible and thus to move up at maximum in the proof. But we can possibly be prevented from moving them just after the inferences introducing their active formulas either by ⊗ inferences or by ? inferences. By adding possible weakenings, we can restrict the use of c? only immediately after the ⊗ and ? rules. Then we can merge them with these two types of rules [14]. It leads to replace in the inference system the ⊗ and ? rules by the ⊗′ and ?′ rules, where Δ_{1} and Δ_{2} do not contain ?F formulas.

\frac{⊢ F_{1}, Δ_{1},?Δ′ ⊢ F_{2}, Δ_{2},?Δ′}{⊢ F_{1} ⊗ F_{2}, Δ_{1}, Δ_{2},?Δ′} ⊗′  \frac{⊢ F,?F, Δ′}{⊢?F, Δ′} ?′

For similar reasons as in the contraction case, it is better to move up as far as possible the w? inferences in the proof. But taking into account the permutability properties and the absence of active formulas, we can move them just after the axioms. We can propose another modification with the axioms Id and 1 being replaced by the axioms Id′ and 1′

\overline{⊢ A, A^{⊥},?Δ} Id′  \overline{⊢ 1,?Δ} 1′

Let us mention that the successive modifications of the inference system conserve the correctness and completeness of the initial one. In fact, even if their form is particular, they are, as chaining decomposition, only applications of up inference movements to w? and c? rules.

4.2 Immediate decomposition

This principle will allow to strongly restrict the choices during the proof search process. It leads to construct specific proof forms where we moved down as far as possible the inferences that can be moved in this direction, that are the ones of type &, ℘, ∀ or ⊥.

Theorem 4.2 (immediate decomposition 1) Let Π be a proof of ⊢ F, Δ′ with F having &, ℘, ∀ or ⊥ as principal connective, there exists a proof Π′ of ⊢ F, Δ′ ending with an inference having F as principal formula.

Even if it is for different reasons, we obtain a similar result for !.

Theorem 4.3 (immediate decomposition 2)

Let Π be a proof of ⊢!F,?Δ′, there exists a proof Π′ of it ending with the inference I_{!} \frac{⊢ F,?Δ′}{⊢!F,?Δ′} .

4.3 Immediate composition

This principle will allow to obtain deterministic steps during the proof search process. For its application as soon as possible, we have to construct specific proofs where we move up as far as possible the possible inferences, i.e., the ones of type ⊗, ⊕_{1}, ⊕_{2}, ∃ or ?.

Theorem 4.4 (immediate composition 1)

(i) Let Π be a proof of ⊢ Δ with an intermediate conclusion ⊢ F′, Δ′ such that F′ is active (for producing a formula F) in an inference of type ⊕_{1}, ⊕_{2}, ∃ or ? and does not have ? as principal

connective, then there exists a proof Π′ of ⊢ Δ including the inference \frac{⊢ F′, Δ′}{⊢ F, Δ′}

(ii) Let Π be a proof of ⊢ Δ with two intermediate conclusions ⊢ F_{1}, Δ_{1} and ⊢ F_{2}, Δ_{2} such that F_{1} and F_{2} are active (to produce a formula F) in a same inference of ⊗ type and do not have ? as principal connective, then there exists a proof Π′ of ⊢ Δ including the inference

\frac{⊢ F_{1}, Δ_{1} ⊢ F_{2}, Δ_{2}}{⊢ F_{1} ⊗ F_{2}, Δ_{1}, Δ_{2}}

We can treat the inference of ℘ type in a similar way. When we try to move it up as far as possible, it can be blocked by some inferences of ! or ⊗ type. In the last case, it means that the active formulas of the inference to move up have been produced in two distinct branches of an ⊗ inference. But, for a top-down strategy, it is not a bad point because the observation of existing intermediate conclusions indicates us if the active formulas are in the same conclusion or not and thus if they can act or not.

Theorem 4.5 (immediate composition 2) Let Π be a proof of ⊢ Δ with an intermediate conclusion ⊢ F_{1}, F_{2}, Δ′ such that F_{1} and F_{2} are active (for producing a formula F) in an inference of ℘ type and do not have ? as principal

connective, then there exists a proof Π′ of ⊢ Δ including the inference \frac{⊢ F_{1}, F_{2}, Δ′}{⊢ F_{1}℘F_{2}, Δ′}

The inferences of type ! can be moved up in a proof by jumps even it is not possible step by step as mentioned in the following theorem

Theorem 4.6 (immediate composition 3) Let be Π a proof of ⊢ Δ in CLL \ {&} with an intermediate conclusion ⊢ F′,?Δ′ such that F′ is active (for producing a formula F) in an inference of ! type and ? is not its principal connective,

then there exists a proof Π′ of ⊢ Δ with the inference \frac{⊢ F′,?Δ′}{⊢!F′, Δ′}

Let us recall that the c? can be moved up or down in a proof but the interest is to move them up to treat them as soon as possible in a top-down strategy.

Theorem 4.7 (immediate composition 4) Let Π be a proof of ⊢ Δ with an intermediate conclusion ⊢?F′,?F′, Δ′ such that both F′ are active (for producing a formula F) in a contraction, then there exists a proof Π′ of ⊢ Δ with the

inference \frac{⊢?F′,?F′, Δ′}{⊢?F′, Δ′}

Let us remark that sometimes the immediate composition principle can strongly reduce the non-determinism. In the multiplicative fragment MLL (extended with ⊕) we have only nondeterminism in the way to associate literals in the axioms.

Remark 4.1 All the previous theorems are proved by induction, with the same proof schema, using the permutability theorem (appendix B) to move up or down some inferences. For theorem 4.3, starting from the root, we replace !F by F in all intermediate conclusions until the inferences producing !F that we suppress. Thus we add the inference I_{!} at the end of the proof.

4.4 Chaining composition

We want to apply it to inferences that are difficult to move up or that we want to treat as late as possible in a top-down strategy. It concerns the inferences of &, ∀ type and also w? that are easy to be moved up or down. We decide to move them down because of top-down strategy and thus try to treat them as late as possible, knowing that they are difficult to control. There exists another form of weakening, the one associated with the axiom ⊤, that can disturb the top-down approach. It allows to produce an infinity of ⊢ ⊤, Δ′ sequents and sub-formula property can not reduce this number. A solution of this problem consists in modifying the inference system by separating the axiom ⊢ ⊤ from the weakening. Then we merge this weakening form with the standard one and the ⊤ rule into the rule w:

\frac{⊢ Δ}{⊢ F, Δ} w with F ≡ ?F′ or ⊥ or with ⊢ Δ being a weakenable sequent. The notion of weakenable sequent introduced in [14] can be simply defined.

Definition 4.1 (weakenable sequent)

(i) Any sequent including the ⊤ formula is weakenable. (ii) Any sequent conclusion of an inference, different from ! or ∀ with only one premise that is weakenable, is weakenable. (iii) Any sequent conclusion of an ⊗ inference with one weakenable premise is weakenable. (iv) Any sequent conclusion of an & inference with both premises that are weakenable is weakenable.

The motivation here is to move down as far as possible the weakenings because they are difficult to control. With such an adaptation of the inference system we can start the proof search from a finite set of axioms.

Theorem 4.8 (chaining composition 1) Let Π be a proof of ⊢ Δ including an inference of type &, ∀ or w with ⊢ F, Δ′ as conclusion and such that F does not become active in an ℘ inference, there exists a proof Π′ of ⊢ Δ where this inference can be only immediately followed by an inference where F is active.

In the next sections, we consider the design of proof search strategies by emphasizing the duality between the bottom-up and top-down directions. For a given proof direction, the analysis schema is the following: studying non-determinism factors and applying the composition or decomposition principles to normalize proofs.

5 Design of bottom-up proof strategies

Let us consider a sequent ⊢ Δ to prove in CLL, a bottom-up proof strategy consists in starting from the final conclusion ⊢ Δ and applying step by step inference rules to construct a proof tree, the nodes of which constitute subgoals to prove at each step and that is closed by axioms.

5.1 Non-determinism factors

With bottom-up strategy, we have to fix three choices, at each step of the search process:

a) Choice of the goal to prove. It is not important from the correctness point of view and it corresponds to a ”don’t care” non-determinism that has consequences in terms of cost and termination of the proof search process. We have to choose goals for which we can conclude that they are provable or not.

b) Choice of the principal formula(s). It corresponds to a ”don’t know” non-determinism and often determines the inference choice that will be done. But if the principal formula has the form ?F we can apply three types of rules: w?, c? and ?. In other cases, its principal connective determines the inference rule to apply and its components, the active formulas of the premises.

c) Choice of the subgoals replacing the goal to prove. We have to consider such choice only in two particular cases: (i) when the principal formula has the form F_{1} ⊕ F_{2}. The goal to prove has the form ⊢ F_{1} ⊕ F_{2}, Δ′ and can be replaced either by ⊢ F_{1}, Δ′ or ⊢ F_{2}, Δ′. (ii) when the principal formula has the form F_{1} ⊗ F_{2}. The goal to prove has the form ⊢ F_{1} ⊗ F_{2}, Δ′ and can be replaced by 2^{n} possibilities (n being the number of formulas in Δ′) of the subgoals ⊢ F_{1}, Δ′_{1} and ⊢ F_{2}, Δ′_{2} where {Δ′_{1}, Δ′_{2}} is a partition of Δ′.

5.2 Basic principles

For reducing such non-determinism factors, we use the immediate decomposition principle that allows to strongly restrict the choices during the bottom-up proof search process. It corresponds to design proofs where we move down, as far as possible, the inferences of type &, ℘, ∀ and ⊥. Moreover, we apply the chaining decomposition principle to inferences that are easy to move up, i.e. the ones of ⊗, ⊕_{1}, ⊕_{2}, ∃ or ? type.

5.3 An example

To describe the application of these principles to bottom-up proof strategies design, we consider the following example, that consists in proving in intuitionistic logic the following formula (∀x¬A(x)) ∨ B ⇒ ∀x(¬A(x) ∨ B). As we can translate intuitionistic logic into linear logic, it consists in proving in CLL the following sequent:

⊢ ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}) ℘ ∀x(!(?A(x)^{⊥}℘ 0) ⊕ !B).

The applications of the immediate and chaining decomposition principles will correspond, during the proof construction process, to deterministic phases alternating with non-deterministic phases.

1) Deterministic phase: we apply the immediate decomposition principle to the sequent and thus successively suppress the external connectives ℘ and ∀. The sequent to prove is now

⊢ ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}), !(?A(x)^{⊥}℘ 0) ⊕ !B.

2) Non-deterministic phase: we have to choose the principal formula of the new inference having this sequent as conclusion. This choice can lead to failure and thus backtracking might be necessary. Here we have two possibilities: ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}) or !(?A(x)^{⊥}℘ 0) ⊕ !B. Only the first one leads to a success but we cannot know it a priori.

3) Deterministic phase: we decompose ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}) by application of the ? and & rules (we have, at the same time, applications of immediate decomposition and chaining decomposition principles). At this step, we have the following partial proof tree with Δ ≡ ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}), !(?A(x)^{⊥}℘ 0) ⊕ !B

\frac{\frac{\frac{\frac{⊢ ?(∃x(!A(x) ⊗ ⊤)), Δ  ⊢ ?B^{⊥}, Δ}{⊢ ?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}, Δ} &}{⊢ ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}), !(?A(x)^{⊥}℘ 0) ⊕ !B} ?′}{⊢ ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}), ∀x(!(?A(x)^{⊥}℘ 0) ⊕ !B)} ∀}{⊢ ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}) ℘ ∀x(!(?A(x)^{⊥}℘ 0) ⊕ !B)} ℘

Let us describe now the rest of the proof construction, considering the left-hand side branch of the proof tree. We do a similar proof for the second branch.

4) Non-deterministic phase: we choose a principal formula among the three possible ones in ⊢ ?(∃x(!A(x) ⊗ ⊤)), ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}), !(?A(x)^{⊥}℘ 0) ⊕ !B. The third one we choose is the only one that leads to a success. The property of logical neutrality (see 5.4) allows us to keep !(?A(x)^{⊥}℘ 0) rather than !B.

5) Deterministic phase: we apply the chaining decomposition principle to !(?A(x)^{⊥}℘ 0) and thus we apply the ! and ℘ rules. The new goal is then ⊢ ?(∃x(!A(x) ⊗ ⊤)), ?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}),?A(x)^{⊥}, 0.

6) Non-deterministic phase: we have three possibilities for choosing the principal formula of the next inference: we will choose the first one.

7) Deterministic phase: the application of the chaining decomposition leads to successively apply the ?, ∃, ⊗′ and ! rules and the end of this proof is immediate. We notice Δ ≡ ⊢ ?F, !(?A(x)^{⊥}℘ 0) ⊕ !B with F ≡ ?F′&B^{⊥} with F′ ≡ ∃x(!A(x) ⊗ ⊤). Thus the left-hand side branch of the proof tree is the following:

\frac{\frac{\overline{⊢ A(x), A(x)^{⊥},?A(x)^{⊥},?F,?F′} Id′}{⊢ A(x),?A(x)^{⊥},?F,?F′} ?′}{⊢ !A(x),?A(x)^{⊥},?F,?F′} ! \overline{⊢ ⊤, 0,?A(x)^{⊥},?F,?F′} ⊤ ⊗′

\frac{\frac{\frac{\frac{\frac{⊢!A(x) ⊗ ⊤,?A(x)^{⊥}, 0,?F,?F′}{⊢ ∃x(!A(x) ⊗ ⊤),?A(x)^{⊥}, 0,?F,?F′} ∃}{⊢?(∃x(!A(x) ⊗ ⊤)),?A(x)^{⊥}, 0,?F} ?′}{⊢?(∃x(!A(x) ⊗ ⊤)),?A(x)^{⊥}℘ 0,?F} ℘}{⊢?(∃x(!A(x) ⊗ ⊤)),!(?A(x)^{⊥}℘ 0),?F} !}{⊢?(∃x(!A(x) ⊗ ⊤)), !(?A(x)^{⊥}℘ 0) ⊕ !B,?F} ⊕

Remark 5.1 To ensure the strategy completeness we can fix a bounded number of contractions in each branch of the proof tree, c? contractions being connected to the ?′ rule.

5.4 Limits of strategies

The use of permutability properties allows to reduce one of the three factors of non-determinism, about the choice of the principal formula. But it does not help for the third one, i.e., the choice of subgoals to replace the current goal after application of the ⊗′ or ⊕ rule. In the first case, the non-determinism about the partition of the context is important. If we want to prove ⊢ F_{1} ⊗ F_{2}, Δ with F_{1} ⊗ F_{2} as principal formula of the last inference, we can begin to try to prove ⊢ F_{1}, Δ without using necessarily all the formulas of Δ. The ones that are not used in the proof will constitute the context Δ_{2} for proving ⊢ F_{2}, Δ_{2} [9]. If it fails, we have to try a new proof of ⊢ F_{1}, Δ. Thus, backtracking is not suppressed but reduced. Another way to reduce non-determinism issued from the ⊕ and ⊗ rules consists in using a property of logical neutrality of the provable sequents. Such property can be given in the following manner: each effective literal of a provable sequent must be related to its dual in this sequent. We call effective literal a literal for which we can determine a priori that it will be introduced by an axiom of the form ⊢ A, A^{⊥} in any proof of the sequent. The non-determinism concerning the principal formula choice may remain important when there are many formulas with ? as main connective.

6 Design of top-down proof strategies

Let us consider a given sequent ⊢ Δ to prove in CLL, a top-down proof strategy consists in applying step by step inference rules from axioms to build a set of partial proofs until we find one with ⊢ Δ as conclusion. In this case, we do not use here backtracking and thus we can produce non-useful partial proofs.

6.1 Non-determinism factors

Each step of the process consists in applying an inference rule to intermediate conclusions obtained from the previous steps and in checking if the new conclusion is not the final conclusion ⊢ Δ. We have non-determinism factors that lead to fix four choices.

a) Choice of a premise of the next inference, among the conclusions of partial proofs already produced. This choice has a meaning only if the next inference is not an axiom. It is determinant regarding the efficiency of the strategy and also its termination and completeness, because some partial proofs are useless. Unfortunately, the non-determinism corresponding to this choice increases proportionally to the number of partial proofs produced during the process.

b) Choice of the active part of the premise we choose. Depending on the inference rule that will be applied, it can include 0, 1 or 2 formulas. It correspond to a ”don’t know” non-determinism in the sense that it can lead to failure.

c) Choice of the principal part to produce. The proofs built here verify the sub-formula property. That is why generally the selected active part completely determinates the principal part to produce. It is not right only in two cases: (i) if the inference is a weakening, thus the active part is empty and it is impossible to control the production of the principal formula from the chosed premise. (ii) if the inference is an axiom, thus it has no premises. In the cases of Id and 1, the subformula property allows to limit the possible principal parts. It is not the case for the ⊤ axiom where the number of possible principal parts is infinite, but the weakenable sequent notion solved this point.

d) Choice of the other premise, when the principal formula we produce is a conjunction. This choice is mainly determinated by the knowledge of the first premise and of the principal formula to produce.

6.2 Basic principles

To study how to normalize proofs to reduce such non-determinism factors, we will use the immediate composition principle that allows to obtain deterministic steps during the top-down proof search process. It corresponds to design proofs where we move up, as far as possible, the inferences candidates for such a movement, i.e., the ones of type ⊗, ⊕_{1}, ⊕_{2}, ∃ or ?. Moreover, we apply the chaining composition principle to inferences that are difficult to move up, i.e. the ones of &, ∀ type or that we decide to treat as late as possible, i.e. the ones of w? type, in a top-down strategy. Let us describe, through an example, the concrete use of a top-down strategy based on these principles and the problems to be dealt with.

6.3 An example

We consider here the example previously developed in the case of a bottom-up strategy, that consists in proving in CLL the following sequent:

⊢?(?(∃x(!A(x) ⊗ ⊤)) & ?B^{⊥}) ℘ ∀x(!(?A(x)^{⊥}℘ 0) ⊕ !B).

A top-down strategy will consist in building a set of partial proofs, the conclusions of which being multi-sets of subformulas of the final conclusion. To describe the construction, it is not necessary to keep the complete trace of partial proofs but only the set of their conclusions, denoted E_{c}. The application of the chaining and immediate composition principles will lead to a succession of deterministic phases (where E_{c} will be modified without increasing) and non-deterministic phases (where E_{c} will increase).

1) At the beginning, E_{c} is composed by all the axioms necessary for the proof of the sequent. Thus E_{c} = {⊢ A(x), A(x)^{⊥}, ⊢ B, B^{⊥}, ⊢ ⊤}.

2) Deterministic phase: by application of the immediate composition principle, we have E_{c} = {⊢ ⊤, ⊢ F_{1},?A(x)^{⊥}, ⊢ F_{2},?B^{⊥}} with F_{1} ≡?(∃x(!A(x) ⊗ ⊤)) and F_{2} ≡!(?A(x)^{⊥} ℘ 0)⊕!B.

3) Non-deterministic phase: we add to E_{c} a new intermediate conclusion by application of the w rule to the first sequent that is weakenable and thus E_{c} = {⊢ ⊤, ⊢ F_{1},?A(x)^{⊥}, ⊢ F_{1},?A(x)^{⊥}, 0 , ⊢ F_{2},?B^{⊥}}.

4) Deterministic phase: by application of the immediate composition principle, we obtain E_{c} = {⊢ ⊤, ⊢ F_{1},?A(x)^{⊥}, ⊢ F_{1}, F_{2}, ⊢ F_{2},?B^{⊥}}.

5) Non-deterministic phase: we add to E_{c} new intermediate conclusions by application of the ∀ and & rules. In fact, we construct the sequent ⊢ F_{1}&?B^{⊥}, F_{2},?A(x)^{⊥} by the & rule application but we suppress it by the P_{sub} property (see 6.4). Thus we obtain E_{c} = {⊢ ⊤, ⊢ F_{1},?A(x)^{⊥}, ⊢ F_{1}, F_{2}, ⊢ F_{2},?B^{⊥}, ⊢ F_{1}&?B^{⊥}, F_{2} , ⊢ F_{1}, ∀xF_{2} , ⊢ ∀xF_{2},?B^{⊥}}.

6) Deterministic phase: the application of either immediate composition principle or chaining composition principle leads to replace ⊢ F_{1}&?B^{⊥} in E_{c} by ⊢?(F_{1}&?B^{⊥}), F_{2}.

7) Final phase: we have only to apply the ∀ (non-deterministic) and ℘ (deterministic) rules for producing the final conclusion.

Remark 6.1 Moreover, to ensure the completeness of the strategy, we fix a bounded size for intermediate conclusions and we increase it in case of failure.

6.4 Limits of top-down strategies

If the strategy we have described is efficient for certain fragments of CLL as the multiplicative one, in the general case the non-determinism can be important due to weakenings that are difficult to control. We can reduce the number of unuseful intermediate conclusions by analyzing the subformulas of a formula that are present and by using the following property P_{sub}: If F_{1} and F_{2} are formulas of the same intermediate conclusion and if they do not correspond (in the final conclusion) to sub-formulas in the scope of a connective ?, then F_{1} is not a sub-formula of F_{2} and F_{1}, F_{2} cannot be in each component of a conjunction. We can also eliminate the intermediate conclusions deduced from others by simple weakening.

7 Conclusion

From results about decidability in various fragments of CLL [11], some works have been devoted to theorem proving, with a bottom-up approach, in CLL [2, 14] or in particular fragments [4, 5, 9, 8] with different motivations. In [2] the inference rules are classified into two disjoint classes from the invertibility and the focusing properties. In [14] these properties are used but one focus on resolution method for proof search. In [8, 9] the notion of uniform proof for particular fragments of CLL is the basis to build efficient theorem provers. In fact, we propose in this paper a complete and global analysis of proof search design in full linear logic, for both proof directions, with general concepts (immediate or chaining composition or decomposition) that can be refined in specific fragments. In further work, it would be interesting to compare strategies with different proof directions; for example, we observe that bottom-up strategies are not efficient for the ⊗ treatment but it is the opposite for the ?. It could lead us to combine both sorts of strategies: for example, we can start with the bottom-up one by decomposing any formula of the sequent with ℘, &, ∀ or ⊥ as principal connector and then end with the top-down approach. We can also imagine more elaborated combinations. Thus, we have basic results to systematically study the various fragments of CLL adequate to theorem proving and its applications in linear logic.

References

[1] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1-2):3–58, 1993.

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

[3] G. Bellin. Proof nets for multiplicative and additive linear logic. Technical Report ECS-LFCS 91-161, Department of Computer Science, Edinburgh University, May 1991.

[4] J. Chirimar and J. Lipton. Provability in tbll: a decision procedure. In CSL’91, LNCS 626, pages 53–65, Bern, October 1991.

[5] D. Galmiche and G. Perrier. Automated deduction in additive and multiplicative linear logic. In Logic at Tver ’92, Logical Foundations of Computer Science Symposium, LNCS 620, pages 151–162, Tver, Russia, July 1992.

[6] D. Galmiche and G. Perrier. On proof normalisation in linear logic. Research report 93-R-059, CRIN-CNRS, 1992. To be published in Theoretical Computer Science.

[7] J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

[8] J. Harland and D. Pym. On resolution in fragments of classical linear logic. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 30–41, St. Petersburg, Russia, July 1992.

[9] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.

[10] N. Kobayashi and A. Yonezawa. Acl - a concurrent linear logic programming paradigm. In Int. Symposium on Logic Programming, pages 279–294, Vancouver, October 1993.

[11] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56:239–311, 1992.

[12] J. Meseguer and N. Marti-Oliet. From petri nets to linear logic. In Category Theory and Computer Science, LNCS 389, pages 313–340, Manchester, September 1989.

[13] N. Shankar. Proof search in the intuitionistic sequent calculus. In 11th Conference on Automated DEduction, LNAI 607, pages 522–536, Saratoga Springs, June 1992.

[14] T. Tammet. Proof search strategies in linear logic. Programming Methodology Group Report 70, Chalmers University Group, University of Göteborg, 1993.

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

A The Linear sequent calculus

The inference system we use is the classical linear sequent calculus [7]. The language considered consists of

a) a set of finite terms T erm[V] on a countable set V of variables (x, y, z, ..),

b) a countable set At of atoms (a,b,..) each having an arity. It allows to construct a set Atom of atomic formulas (A,B,..): if n is the arity of the atom a and t_{1}, t_{2}, ..., t_{n} ∈ T erm[V] then a(t_{1}, t_{2}, ..., t_{n}) is an atomic formula,

c) a set of logical operators Op = {0, 1, ⊥, ⊤, ()^{⊥},!,?, ⊗, ℘, &, ⊕, ∀, ∃}. It allows to construct a set F orm of formulas (F,G,..) that are the formulas of LL, following the grammar

F ::= 0|1| ⊥ |⊤|A|A^{⊥}|?F |!F |F ⊗ F |F ℘F |F &F |F ⊕ F |∀xF |∃xF.

Before presenting the inference rules of the linear sequent calculus, we consider the linear negation that is essential for the symmetrical character of LL. The negation of formula is defined by the following equalities: F^{⊥⊥} = F, 1^{⊥} =⊥, ⊥^{⊥} = 1, ⊤^{⊥} = 0, 0^{⊥} = ⊤, (F ⊗ G)^{⊥} = F^{⊥}℘G^{⊥} and (F ℘G)^{⊥} = F^{⊥} ⊗ G^{⊥}, (F &G)^{⊥} = F^{⊥} ⊕ G^{⊥} and (F ⊕ G)^{⊥} = F^{⊥}&G^{⊥}, (∀xF)^{⊥} = ∃xF^{⊥} and (∃xF)^{⊥} = ∀xF^{⊥}, (!F)^{⊥} =?F^{⊥} and (?F)^{⊥} =!F^{⊥}.

1) \underline{Identity and structural rules}

\overline{⊢ A, A^{⊥}} Id  \frac{⊢ F, Γ ⊢ F^{⊥}, Δ}{⊢ Γ, Δ} Cut  \frac{⊢ Δ}{⊢?F, Δ} w?  \frac{⊢?F,?F, Δ}{⊢?F, Δ} c?

\frac{⊢ F_{1}, Γ_{1} ⊢ F_{2}, Γ_{2}}{⊢ F_{1} ⊗ F_{2}, Γ_{1}, Γ_{2}} ⊗  \frac{⊢ F_{1}, F_{2}, Γ}{⊢ F_{1}℘F_{2}, Γ} ℘  \overline{⊢ 1} 1  \frac{⊢ Γ}{⊢ ⊥, Γ} ⊥
\frac{⊢ F_{1}, Γ ⊢ F_{2}, Γ}{⊢ F_{1}&F_{2}, Γ} &  \frac{⊢ F_{1}, Γ}{⊢ F_{1} ⊕ F_{2}, Γ} ⊕_{1}  \frac{⊢ F_{2}, Γ}{⊢ F_{1} ⊕ F_{2}, Γ} ⊕_{2}  \overline{⊢ ⊤, Δ} ⊤

\frac{⊢ F,?Γ}{⊢!F,?Γ} !  \frac{⊢ F, Γ}{⊢?F, Γ} ? \frac{⊢ F [y/x], Γ}{⊢ ∀xF, Γ} ∀  \frac{⊢ F [t/x], Γ}{⊢ ∃xF, Γ} ∃

3) \underline{Logical rules} ∘ Multiplicative rules ∘ Additive rules ∘ Exponential and quantifier rules In ∀ rule, y is not free in ⊢ ∀xF, Γ.

B Permutability properties

Definition B.1 Let us consider a proof Π in CLL, we say that I_{1} and I_{2} two inferences of Π are in permutation position if they verify the conditions: (i) I_{2} follows directly I_{1} in Π, (ii) the principal part in I_{1} is disjoint of the active part of I_{2}’s j-th premise of I_{2} where it appears.

Definition B.2 Let us consider a proof Π in CLL, I_{1} and I_{2} inferences of Π being in permutation position, I_{1} is permutable with I_{2} in Π if there exists inferences I′_{1} and I′_{2} such that

(i) type(I′_{1}) = type(I_{1}) and type(I′_{2}) = type(I_{2}), (ii) the conclusion of I′_{2} coincides with a premise of I′_{1}, (iii) if type(I_{2}) = & and J_{1} is the other inference immediately preceding I_{2} in Π then type(J_{1}) = type(I_{1}). (iv) if type(I_{1})= & there exists another inference J′_{2}, such that type(J′_{2}) = type(I_{2}) and the conclusion of which coincides with the second premise of I′_{1}.

(v) Let us consider the derivation (called permutation object) composed by I_{1} (and J_{1} if type(I_{2}) = &) followed by I_{2} and the derivation (called permutation result) composed by I′_{2} (and J′_{2} if type(I_{1})= &) followed by I′_{1}, both have the same conclusion and the same hypotheses modulo a duplication of some of them and a renaming of certain free variables. In the other cases, we say that I_{1} and I_{2} are not permutable.

Theorem B.1 (permutability theorem) Let t_{1} and t_{2} be two types of inference, in the following array,

(i) the case(t_{1}, t_{2}) in the following array contains p if and only if for any inferences I_{1} and I_{2} of type t_{1} and t_{2} being in permutation position in a proof Π, I_{1} is permutable with I_{2}. (ii) the case(t_{1}, t_{2}) contains np if and only if there exists two inferences I_{1} and I_{2} of type t_{1} and t_{2} being in permutation position in a proof Π, which are not permutable. (iii) the case(t_{1}, t_{2}) contains a cross × if and only if for any inferences I_{1} and I_{2} of type t_{1} and t_{2} in a proof Π, I_{1} is never in permutation position with I_{2}.

\begin{matrix}t_{2}\t_{1} & cut & ⊗ & ℘ & & & ⊕ & ? & w? & c? & ! & ∀ & ∃ & ⊥ \\ cut & p & p & p & p & p & p & p & p & np & p & p & p \\ ⊗ & p & p & p & p & p & p & p & p & np & p & p & p \\ ℘ & np & np & p & p & p & p & p & p & np & p & p & p \\ & & np & np & np^{∗} & np^{∗} & np & np & np & np^{∗} & np & np^{∗} & np & np^{∗} \\ ⊕ & p & p & p & p & p & p & p & p & np & p & p & p \\ ? & p & p & p & p & p & p & p & p & p & p & p & p \\ w? & p & p & p & p & p & p & p & p & p & p & p & p \\ c? & np & np & p & p & p & p & p & p & p & p & p & p \\ ! & np & × & × & × & × & np & p & p & × & × & × & × \\ ∀ & np & p & p & p & p & p & p & p & np & p & np & p \\ ∃ & p & p & p & p & p & p & p & p & np & p & p & p \\ ⊥ & p & p & p & p & p & p & p & p & np & p & p & p \end{matrix}

Let us remark that the np^{∗} in the & line indicate that the non-permutability is relative to our formal definition and can be overcome with a specific treatment.

Proof B.1 A complete proof is given in [6].