LINK: a Proof Environment based on Proof nets

L. Habert^{⋆}, J.-M. Notin, and D. Galmiche

LORIA–Université Henri Poincaré Campus Scientifique, BP 239 Vandœuvre-lès-Nancy, France

1 Introduction

LINK is a proof environment including proof nets-based provers for multiplicative linear logics: mixed linear logic, or recently called non-commutative logic (MNL) [1], commutative linear logic (MLL) and non-commutative (or cyclic) linear logic (MCyLL). Its main characteristic is the provability analysis through automatic proof nets construction. A proof net is a particular graph-theoretic representation of proofs that appears appropriate for proof-search in MLL and MCyLL [4, 5]. It is a powerful alternative to deal with proof search and its problems about non-permutability and resource management [3]. In the context of system verification, such a semantical and graphical representation of proof can be useful from a software engineering point of view. It allows to analyse provability (through proof nets) or non-provability (through proof structures that can be seen as counter-models). The LINK proof engine is based on one specific algorithm dedicated to MLL [8] that has been adapted to deal with non-commutative connectives (MCyLL) and also with both commutative and non-commutative connectives (MNL). This first version of LINK includes provers that can be also seen as implementations of new connection methods for these linear logic fragments [4]. Further work, in addition to standard improvements, will concern the development of this proof technology for other substructural logics and of tools dedicated to the analysis of related semantic structures. LINK illustrates that proof nets-based theorem proving is an appropriate and promising proof-theoretical but also proof-engineering approach of proof search in linear logic fragments.

2 Basic principles of LINK

LINK is a proof environment that includes provers for three multiplicative linear logics, but each of them is based on the same initial principles presented for MLL in [8] and refined in [5]. Let us summarize its underlying concepts and principles. A proof structure for a sequent Γ is composed of its decomposition tree and axiom-links between leaves, labelled with dual atomic formulae X and X^{⊥}. Figure 1 shows a proof structure of a MLL sequent ⊢ (A ⊗ B) & C, A^{⊥}, C^{⊥} ⊗ B^{⊥}. Among proof structures, there are some corresponding to a proof in the sequent

⋆ École Normale Supérieure Ulm, Paris, France, in a training period at LORIA.

Fig. 1. A MLL proof structure

calculus. Such a proof structure is called a proof net and there are criteria characterizing a proof structure that is a proof net. Our approach is based on an inductive definition of proof nets leading to an automatic construction of proof nets from the decomposition tree and thus to an automatic search of appropriate axiom-links. For instance, the inductive definition of MLL proof nets is the following: 1) an axiom (X, X^{⊥}), where X is a atom, is a proof net; 2) let Π_{1} and Π_{2} be disjoint proof nets, with conclusions Γ, A and B, Δ respectively, then the extension of Π_{1} and Π_{2}, from A and B, with a conjunctive link (⊗) between A and B is a proof net Π, with conclusions Γ, A ⊗ B, Δ; 3) let Π_{1} be a proof net with conclusions Γ, A, B, then the extension of Π, from A and B, with a disjunctive link ( & ) is a proof net Π, with conclusions Γ, A & B. Let us summarize the principles of construction for MLL. The algorithm starts with the decomposition tree of the sequent, that is a frame guiding the proof net search. The main idea is to build, step by step but automatically, axiom-links that are elementary proof nets and to link and extend them in order to have new sub-proof nets (further called subnets) and finally a proof net that “covers” the decomposition tree. Coming back to our example, from figure 1, we can first build the axiom-links (A, A^{⊥}) and (B, B^{⊥}) that are two elementary proof nets and connect and extend them with a conjunctive link (⊗). Then, this new proof net and the axiom-link (C, C^{⊥}) can be connected and extended with a conjunctive link (⊗), providing a new proof net. Finally, as A ⊗ B and C are conclusions of the same proof net, we can extend it with a disjunctive link ( & ) and we have a proof net with (A ⊗ B) & C, A^{⊥} and C^{⊥} ⊗ B^{⊥} as conclusions, that covers the initial decomposition tree. A main and necessary principle is to deal with conjunctive links before additive links. More details about the algorithm can be found in [4, 8].

A major problem arising in such proof nets construction is the choice of appropriate axiom-links. If we replace, in our example, B and C by A, B^{⊥} and C^{⊥} by A^{⊥}, we need to detect the right axiom-links among all the possible (A, A^{⊥}). Some automatic choices are wrong choices, w.r.t. provability, and thus backtracking is necessary at some points. Our algorithm includes strategies to detect most of the failure cases: for instance, when two premises of a conjunctive link (resp. disjunctive link) are (resp. cannot be) in the same subnet. The impact of the strategies is significant and the backtracking is then strongly reduced. Let us mention that this approach, compared to bottom-up proof search in a sequent calculus, is often very efficient to detect and analyse the non-provability of a sequent.

3 The LINK prover

The LINK prover is written in the OCaml^{1} language. The program and its sources are available at http://www.loria.fr/˜ notin/LINK with information about how to install and use LINK. Thanks to the module system of OCaml, most part of the code is shared between the different provers (for MLL, MCyLL and MNL). Therefore, LINK proposes a single command line interface allowing the user to choose the logic, and to enter the formula to prove. Figure 2 shows a typical session of LINK. If the display mode is available, the proof net in construction is drawn in a graphic window. The user can also choose to have a step by step proof net construction in this window; this mode is very useful to understand the basic principles of the provers, as it shows the main stages like creation of axiom-links or extension of subnets by conjunctive and disjunctive links.

$mnld  We choose to work in MNL, using dependencies.

((a*b)<c)|a^|(c^@b^)  We enter a first formula.

F = ((((a*b)<c)|a^)|(c^@b^))

Disproved in 0.00 seconds The formula is not provable.
((a@b)<c)|a^|(c^@b^)  We enter a second formula.

F = ((((a@b)<c)|a^)|(c^@b^))

Proved in 0.00 seconds  This one is provable.

(* represents ⊗, @ represents ⊙, | represents &and < represents ⊲)

Fig. 2. A session example

LINK is composed of four main modules: Select (for the choice of literals), CC (Connected Components - to handle subnets already built) and PW (Par Waiting - to handle disjunctive links, the premises of which do not belong to the same subnet). The fourth module, Build, is common to all provers and contains the procedures that implement the basic proof nets construction algorithm. The algorithm for MLL is implemented from the basic principles we previously mentioned. Following [5], MCyLL proof nets can be seen as particular MLL proof nets such that there is no crossing between axiom-links. Then, to build a prover for MCyLL, we only have to modify the Select module in order to have a choice of literals in accordance with this restriction. The design of a prover for MNL is more complicated because this logic combines both commutative (⊗, & ) and non-commutative (⊙, ⊲) connectives [1]. The underlying idea is to apply the previous principles with ⊗ and ⊙ as conjunctive links and &and ⊲ as disjunctive links and to capture the actual interactions between connectives during proof search with an appropriate semantic structure (based on labels or dependencies) that is built in parallel with the partial proof nets. Following [7], in which we provide a new definition of MNL proof nets based on dependency

 1 OCaml is available at http://caml.inria.fr/ocaml

relations, a first prover builds, step by step, partial proof nets like in MLL, but also in parallel dependency graphs on which one has to verify some conditions when a non-commutative disjunction (⊲) link must be extended. Therefore, the CC and PW modules have to be adapted to deal with such dependency graphs associated to subnets. In particular, the procedures performing the extension of subnets by disjunctive and conjunctive links (included in the CC module) include the computation of the dependency set associated to the new subnet.

D =

Fig. 3. A step of MNL proof net construction

Figure 3 shows, for the MNL sequent ⊢ (A ⊗ B) ⊲ C, A^{⊥}, C^{⊥} ⊙ B^{⊥}, a partial MNL proof net (in bold) and the associated dependency set D. The algorithm has extended axiom-links by A ⊗ B and then by C^{⊥} ⊙ B^{⊥}. Then, it has to check a condition on the dependency graph, related to the ⊲ connective. When, like here, the condition is not verified then the extension of the ⊲ link is impossible. As there is no other choice for axiom-links, the algorithm cannot perform any backtracking and the construction fails. In such a case of non-provability, the partial proof net (in bold) and the dependency graph in LINK are displayed. Then, such a graph is an essential semantic tool to analyse the provability in MNL. If A ⊗ B is replaced by A ⊙ B then the condition is verified and a final proof net is built. The MLL strategies are extended to MNL and are very efficient to reduce backtracking when many choices are possible for axiom-links construction. LINK also includes two other MNL provers that are based on other semantic structures. One, following [6], with labels that are propagated in partial proof structures (decomposition tree plus axiom-links already built) during the proof net search. Another, following [11], with implementations of a contractibility criterion with a particular graph (a seaweed) and contraction rules applied on the associated structure. Further work will be devoted to refinements on the first MNL prover, focusing on the analysis and manipulation of dependency graphs. The performances of LINK provers have been tested on various examples, of provable and nonprovable formulae and the results are good. They illustrate the efficiency of the based-on proof net theorem proving, mainly in case of non-provability. With our algorithms, we can directly build, in parallel, a sequent proof for Γ, each link extension corresponding to a sequent rule application. Depending on the strategy, we can obtain a sequent proof in various canonical forms (for instance with focusing [2]). Moreover, these provers are implementations of new connection methods for linear logics [4, 10], with automatic generation of connections and parallel construction of sequent proofs.

4 Conclusion and perspectives

LINK is a proof environment based on an original and alternative concept, w.r.t. proof-search, namely proof net. It illustrates the actual interest of this concept, completed with semantic structures, to provide proof search and proof analysis in some linear logic fragments. The main prover of LINK deals with MNL, that appears appropriate to specify particular programming concepts or system properties [9] and for which no automatic prover has been designed before. The LINK provers are efficient, especially for non-provability, and also provide semantic structures that can be analysed in this case. Further developments of this version will include refinements of strategies, parallel construction of the sequent proof and graphical representations of semantic structures like dependency graphs. Tools for the manipulation and the analysis of these structures will be studied, with a software engineering and users point of view. We aim to use the LINK environment and their further extensions (with additives, quantifiers) for the verification and analysis of system properties [9], focusing on the failure analysis from the graph-theoretical proof representation.

References

1. M. Abrusci and P. Ruet. Non-commutative logic I : the multiplicative fragment. Annals of Pure and Applied Logic, 101:29–64, 2000.

2. J.M. Andreoli and R. Maieli. Focusing and proof-nets in linear and noncommutative logic. In Int. Conf. on Logic for Programming and Automated Reasoning, LPAR’99, LNCS 1705, pages 320–333, Tbilisi, Georgia, September 1999.

3. I. Cervesato, J. Hodas, and F. Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1-2):133–163, 2000.

4. D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1-2):231–272, 2000.

5. D. Galmiche and B. Martin. Proof nets construction and automated deduction in non-commutative linear logic - extended abstract. Electronic Notes in Theoretical Computer Science, 17, 1998.

6. D. Galmiche and J.M. Notin. Proof-search and proof nets in mixed linear logic. Electronic Notes in Theoretical Computer Science, 37, 2000.

7. D. Galmiche and J.M. Notin. Calculi with dependency relations for mixed linear logic. In International Workshop on Logic and Complexity in Computer Science, LCCS’2001, pages 81–102, Créteil, France, 2001.

8. D. Galmiche and G. Perrier. A procedure for automatic proof nets construction. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 42–53, St. Petersburg, Russia, July 1992.

9. D. Gray, G. Hamilton, J. Power, and D. Sinclair. Specifying and verifying TCP/IP using Mixed Intuitionistic Linear Logic. Technical report, Dublin City Univ., 2001.

10. C. Kreitz, H. Mantel, J. Otten, and S. Schmitt. Connection-based proof construction in linear logic. In 14th Int. Conference on Automated Deduction, pages 207–221, Townsville, North Queensland, Australia, 1997.

11. V. Mogbil. Quadratic correctness criterion for non commutative logic. In 15th Int. Workshop on Computer Science Logic, CSL 2001, LNCS 2142, pages 69–83, Paris, France, 2001.