Dealing with additives in MALL proof search^{∗}

D. Galmiche & J.Y. Marion CRIN-CNRS & INRIA Lorraine, Campus Scientifique, BP 239, F-54506 Vandœuvre-lès-Nancy, France, e-mail: Didier.Galmiche{Jean-Yves.Marion}@loria.fr

1 Introduction

Some recent works have been devoted to proof search procedures in various fragments of linear logic (we refer to [5, 7] for backgrounds on linear logic). Knowing about some results on complexity for them (for example, Multiplicative Linear Logic - MLL - is NP-complete and Multiplicative and Additive Linear Logic - MALL - is PSPACE-complete) [8, 9], they are based on various approaches as resolution [10], tableaux methods [2, 6] or canonical proofs [4, 5]. Even if the later one allows to reduce some non-determinism sources, through particular proof forms, it does not propose a good management of the additive connectives [4]. Thus, to increase the pruning of the proof search tree in MALL, continuing works of [1, 2, 3, 6, 11], we propose a tableaux-like proof search method, based on a specific deducibility relation dealing with additive and multiplicative contexts. To improve proof search, we can propose strategies in this new proof system.

2 Additives management in proof search

Let us start to present some motivations of this work and the induced choices concerning proof search in MALL. The decision procedure we consider is a tableaux-like method [1] that is based on the following ideas: during the proof search, there are non-deterministic choices which come from the additive connectors and might be seen in the rule

\frac{Γ, E_{i} ⊢ Δ}{Γ, E_{1}&E_{2} ⊢ Δ} i ∈ \{1, 2\}

We might choose between E_{1} and E_{2}, choice that is not invertible. Thus, we would like to delay it and try to accumulate a great deal of information before exploring such or such branches of the proof tree. Henceforth, with a better backtracking mechanism, the number of proof failures would decrease. Then, we propose a deducibility relation represented by the statement A; Γ⇒Δ; B, with A, B being what we call additive contexts (sets of formulae which keeps track of possible choices of hypothesis and conclusions). Γ, Δ are as usual both multisets of formulae called multiplicative contexts. In fact, A; Γ⇒Δ; B will hold if there exists two formulae A ∈ A and B ∈ B such that the sequent A, Γ ⊢ Δ, B holds in MALL.

2.1 A new proof system

This new deducibility relation is defined with the following proof system, in which, as usual, a proof is made by successive rule applications until no rule is applicable.

∗In proceedings of 2nd Workshop on Non-Standard Logics and Logical Aspects of Computer Science, Irkutsk, Russia, june 1995

\frac{; A⇒A;}{⊥} ⊥

\frac{A; Γ⇒Δ, F_{1}&F_{2}; B}{A; Γ⇒Δ, F_{1}; B and A; Γ⇒Δ, F_{2}; B} &_{mR}  \frac{; Γ, E_{1}&E_{2}⇒Δ; B}{E_{1}, E_{2}; Γ⇒Δ; B} &_{mL}

\frac{A; Γ⇒Δ, F_{1} ⊕ F_{2};}{A; Γ⇒Δ; F_{1}, F_{2}} ⊕_{mR} \frac{A; Γ, E_{1} ⊕ E_{2}⇒Δ; B}{A; Γ, E_{1}⇒Δ and A; Γ , E_{2} ⇒Δ} ⊕_{mL}

\frac{A, E_{1}&E_{2}; Γ⇒Δ; B}{A, E_{1}, E_{2}; Γ⇒Δ; B} &_{aL}  \frac{A; Γ⇒Δ; F_{1} ⊕ F_{2}, B}{A; Γ⇒Δ; F_{1}, F_{2}, B} ⊕_{aR}

\frac{A; Γ_{1}, Γ_{2}⇒Δ_{1}, Δ_{2}, F_{1} ⊗ F_{2}; B}{A_{1}; Γ_{1}⇒Δ_{1}, F_{1}; B_{1} and A_{2}; Γ_{2}⇒Δ_{2}, F_{2}; B_{2}} ⊗_{mR} \frac{A; Γ, E_{1} ⊗ E_{2}⇒Δ; B}{A; Γ, E_{1}, E_{2}⇒Δ; B} ⊗_{mL}

\frac{A; Γ⇒Δ, F_{1}℘F_{2}; B}{A; Γ⇒Δ, F_{1}, F_{2}; B} ℘_{mR} \frac{A; Γ_{1}, Γ_{2}, E_{1}℘E_{2}⇒Δ_{1}, Δ_{2}; B}{A_{1}; Γ_{1}, E_{1}⇒Δ_{1}; B_{1} and A_{2}; Γ_{2}, E_{2}⇒Δ_{2}; B_{2}} ℘_{mL}

\frac{A; Γ⇒Δ; B}{; A, Γ⇒Δ; B} add_{L} A ∈ A \frac{A; Γ⇒Δ; B}{A; Γ⇒Δ, B;} add_{R} B ∈ B

where A_{1} = A and A_{2} = ∅ or inversely A_{1} = ∅ and A_{2} = A, likewise B, B_{1}, B_{2}. Lastly, the contexts A, B, Γ, Δ could be empty. Let us notice that the ⊥ rule is the closure rule. The rules add_{R} and add_{L} define the specific management of the additive contexts, mixed with the application of the rules ⊕_{aR} and &_{aL}.

2.2 An example

To prove the sequent Γ ⊢ Δ, we translate it in our system as ; Γ⇒Δ;. The above rules might be ordered to provide a complete proof search strategy to especially handle more efficiently nondeterministic choices and so to avoid useless searches, by pruning the proof search tree. Some of these points are illustrated through the proof of (A&B) ⊗ C ⊢ (A ⊗ C)&(B ⊗ C).

; (A&B) ⊗ C⇒(A ⊗ C)&(B ⊗ C);  ⊗_{mL}
; (A&B), C⇒(A ⊗ C)&(B ⊗ C);  &_{mL}
A, B; C⇒(A ⊗ C)&(B ⊗ C);  &_{mR}
A, B; C⇒A ⊗ C;  ⊗_{mR} and  A, B; C⇒B ⊗ C;  ⊗_{mR}
\begin{matrix}A, B; ⇒A; & add_{L} & and & ; C⇒C; & ⊥ \\ ; A⇒A; & ⊥ & & ⊥ \\ ⊥ \end{matrix}  \begin{matrix}A, B; ⇒B; & add_{L} & and & ; C⇒C; & ⊥ \\ ; B⇒B; & ⊥ & & ⊥ \\ ⊥ \end{matrix}

We can thus propose strategies for a good pruning of the proof search tree.

2.3 Completeness result

The previous method is complete, in the following sense

Theorem 1 Let us assume that A = {A_{1}, …, A_{m}} and B = {B_{1}, …, B_{n}}, A; Γ⇒Δ; B is a closed tableaux iff A_{1}& … &A_{m}, Γ ⊢ Δ, B_{1} ⊕ … ⊕ B_{n} is derivable in MALL.

Proof (←): It is done by induction on the length of a cut free derivation. The only difficulty arises with the rule

\frac{E_{i}, Γ ⊢ Δ}{E_{1}&E_{2}, Γ ⊢ Δ}

By assumption, ; E_{i}, Γ⇒Δ; is a closed tableau entry. Therefore the tableau

; E_{1}&E_{2}, Γ⇒Δ;
E_{1}, E_{2}; Γ⇒Δ;
; E_{i}, Γ⇒Δ;

is closed. We observe that the case of ⊕ in the right-hand side is symmetrical. (→): we show by induction that if A; Γ⇒Δ; B is a closed tableau then A_{1}& … &A_{m}, Γ ⊢ Δ, B_{1} ⊕…⊕B_{n} holds in MALL. Here the hard case is when a decision is made about waiting choices

\frac{A; Γ⇒Δ; B}{; A_{j}, Γ⇒Δ; B} 1 ≤ j ≤ m

The corresponding proof is then composed of at most m successive &-left rules. In fact, the key point is that A_{j}, Γ ⊢ Δ, B_{i} is derivable from A_{1}& … &A_{m}, Γ ⊢ Δ, B_{1} ⊕ … ⊕ B_{n}. □

3 Concluding remarks

As a corollary of the theorem 1, we can show that the system is complete for the phase semantic. The additive context just depends on two formulae, one on each side. Thus, we could say that the above system has only two steps of non-determinisms. In further work, we will extend this system to express non-deterministic aspects of each formula involved in a proof.

References

[1] H. B. Curry, Foundations of Mathematical Logic, Dover ed., 1976.

[2] M. D’Agostino and M. Mondadori, The taming of the cut. Classical refutations with analytic cut, Journal of Logic and Computation, 4(3):285-319, 1994.

[3] M. D’Agostino and D.M. Gabbay, A generalization of Analytic Deduction via labelled deductive systems. Part I: Basic Substructural Logics, Journal of Automated Reasoning, 13:243-281, 1994.

[4] D. Galmiche and G. Perrier, Automated deduction in multiplicative and additive linear logic, In Symposium on Logical Foundations in Computer Science, Logic at Tver, LNCS 620, 151-162, Tver, Russia, July 1992.

[5] D. Galmiche and G. Perrier, On proof normalization in linear logic, Theoretical Computer Science, 135(1):67-110, 1994.

[6] D. Galmiche and J-Y Marion, Semantics Proof search methods for additive linear logic - a first approach -, 4th International Workshop on Theorem proving with analytic tableaux and related methods, May 1995.

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

[8] M. I. Kanovich, Horn Programming in Linear Logic is NP-Complete, In 7th Logic in Computer Science, IEEE Press, 200-210, 1992.

[9] P. Lincoln, J. Mitchell, A. Scedrov and N. Shankar: Decision Problems for Propositional Linear Logic, Annals Pure Appl. Logic, 56:239-311, 1992.

[10] G. Mints Resolution Calculus for the First Order Linear Logic, Journal of Logic, Language and Information, 2:59-83, 1993.

[11] A. Urquhart, Complexity of proofs in classical propositional logic, In Logic from Computer Science, ed. Y. Moschovakis, Springer-Verlag, 596–608, 1992.