The ILLTP Library for Intuitionistic Linear Logic

TL;DR

This paper introduces the ILLTP library for benchmarking automated theorem proving in propositional intuitionistic linear logic, utilizing translations of classical theorems, proof comparisons, and Petri net problems to expand the collection.

Contribution

It presents a new library for intuitionistic linear logic theorem proving, including problem translations, proof analysis, and Petri net problem encoding, filling a gap in non-classical logic benchmarking tools.

Findings

Analyzed four translations of intuitionistic logic into linear logic.

Compared proofs using a linear logic prover with focusing.

Expanded the problem set with Petri net reachability problems.

Abstract

Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in the traditional monograph "Introduction to Metamathematics". We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using a linear logic based prover with focusing. In order to enhance the set of problems in our library, we apply the three provability-preserving translations to the propositional benchmarks in the ILTP Library. Finally, we generate a comprehensive set of reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging our collection of problems.

Tables

Table 1. Table 1: Comparison of translations. Times are measured in miliseconds. Test run on a QEMU Virtual CPU, 2GHz, 64 bits, 6GB of RAM running Ubuntu. Timeout set to 5 minutes.

	Encoding 0/1				Call-by-Name				Call-by-Value
	KLE	LCL	SYJ	SYN	KLE	LCL	SYJ	SYN	KLE	LCL	SYJ	SYN
Num. of Problems	88	2	248	20	88	2	248	20	88	2	248	20
Unsolved (timeouts)	11	2	209	9	12	2	203	9	9	2	209	9
Solved (Theorems)	76	0	39	7	76	0	45	6	76	0	39	7
Non-Theorems	1	0	0	4	0	0	0	5	3	0	0	0
Min Time	17	-	18	16	17	-	17	16	16	-	17	17
Avg Time	798.78	-	34039.10	105.81	250.43	-	20319.98	96.27	494.49	-	33884.36	77.18
Max Time	41548	-	276886	458	4186	-	174778	383	24427	-	265778	321

Equations

$$F::=p\mid 1\mid 0\mid \top \mid \perp \mid F\otimes F\mid F\text{bindnasrepma}F\mid F\text{with}F\mid F\oplus F\mid F-\circ F\mid ?F\mid !F$$

$$\frac{}{p⊢p}\mathsf{init}\frac{}{⊢1}{1}_{\_}R\frac{}{\Gamma ⊢\top }{\top }_{\_}R\frac{\Gamma ⊢}{\Gamma ⊢\perp }{\perp }_{\_}R\frac{\Gamma ⊢\Delta }{\Gamma ,1⊢\Delta }{1}_{\_}L\frac{}{\perp ⊢}{\perp }_{\_}L\frac{}{\Gamma ,0⊢\Delta }{0}_{\_}L$$

$$\frac{\Gamma ⊢F\Gamma ⊢G}{\Gamma ⊢F\text{with}G}{\text{with}}_{\_}R\frac{{\Gamma }_{\_}1⊢F{\Gamma }_{\_}2⊢G}{{\Gamma }_{\_}1,{\Gamma }_{\_}2⊢F\otimes G}{\otimes }_{\_}R\frac{\Gamma ⊢F_{\_}i}{\Gamma ⊢F_{\_}1\oplus F_{\_}2}{\oplus }_{\_}{R}_{\_}i\frac{\Gamma ,F_{\_}i⊢\Delta }{\Gamma ,F_{\_}1\text{with}{F}_{\_}2⊢\Delta }{\text{with}}_{\_}{L}_{\_}i$$

$$\frac{\Gamma ,F,G⊢\Delta }{\Gamma ,F\otimes G⊢\Delta }{\otimes }_{\_}L\frac{\Gamma ,F⊢\Delta \Gamma ,G⊢\Delta }{\Gamma ,F\oplus G⊢\Delta }{\oplus }_{\_}L\frac{\Gamma ,F⊢G}{\Gamma ⊢F-\circ G}{-\circ }_{\_}R\frac{{\Gamma }_{\_}1⊢F{\Gamma }_{\_}2,G⊢\Delta }{{\Gamma }_{\_}1,{\Gamma }_{\_}2,F-\circ G⊢\Delta }{-\circ }_{\_}L$$

$$\frac{!\Gamma ⊢F}{!\Gamma ⊢!F}{!}_{\_}R\frac{\Gamma ,!F,!F⊢\Delta }{\Gamma ,!F⊢\Delta }{\mathsf{cont}}_{\_}L\frac{\Gamma ⊢\Delta }{\Gamma ,!F⊢\Delta }{\mathsf{weak}}_{\_}L\frac{\Gamma ,F⊢\Delta }{\Gamma ,!F⊢\Delta }{\mathsf{der}}_{\_}L$$

$$\Theta :\Gamma ,F\otimes G⟶\Delta \Theta :\Gamma ,F,G⟶\Delta \Theta :\Gamma ⟶F-\circ G\Theta :\Gamma ,F⟶G\Theta :\Gamma ,1⟶\Delta \Theta :\Gamma ⟶\Delta \Theta :\Gamma ⟶\perp \Theta :\Gamma ⟶$$

$$\Theta :\Gamma ⟶\top \Theta :\Gamma ,0⟶\Delta \Theta :\Gamma ,!F⟶\Delta \Theta ,F:\Gamma ⟶\Delta$$

$$\Theta :\Gamma ⟶F\text{with}G\text{lx@proof@logical@and}\Theta :\Gamma ⟶F\Theta :\Gamma ⟶G\Theta :\Gamma ,F\oplus H⟶\Delta \text{lx@proof@logical@and}\Theta :\Gamma ,F⟶\Delta \Theta :\Gamma ,H⟶\Delta$$

$$\Theta :{\Gamma }_{\_}1,{\Gamma }_{\_}2{-}_{\_}F\otimes G\to \text{lx@proof@logical@and}\Theta :{\Gamma }_{\_}1{-}_{\_}F\to \Theta :{\Gamma }_{\_}2{-}_{\_}G\to \Theta :{\Gamma }_{\_}1,{\Gamma }_{\_}2\stackrel{F-\circ G}{\to }\Delta \text{lx@proof@logical@and}\Theta :{\Gamma }_{\_}1{-}_{\_}F\to \Theta :{\Gamma }_{\_}2\stackrel{G}{\to }\Delta \Theta :\Gamma {-}_{\_}{F}_{\_}1\oplus F_{\_}2\to \Theta :\Gamma {-}_{\_}{F}_{\_}i\to$$

$$\Theta :\Gamma \stackrel{F_{\_}1\text{with}{F}_{\_}2}{\to }C\Theta :\Gamma \stackrel{F_{\_}i}{\to }\Delta \Theta :\cdot {-}_{\_}1\to \Theta :\cdot \stackrel{\perp }{\to }\Theta :\cdot {-}_{\_}!F\to \Theta :\cdot ⟶F$$

$$\Theta :\Gamma {-}_{\_}p\to$$

$$\Theta ,N_{\_}a:\Gamma ⟶\Delta \Theta ,N_{\_}a:\Gamma \stackrel{N_{\_}a}{\to }\Delta \Theta :\Gamma ,N⟶\Delta \Theta :\Gamma \stackrel{N}{\to }\Delta \Theta :\Gamma ⟶P\Theta :\Gamma {-}_{\_}P\to$$

$$\Theta :\Gamma \stackrel{P}{\to }\Delta \Theta :\Gamma ,P⟶\Delta \Theta :\Gamma {-}_{\_}N\to \Theta :\Gamma ⟶N$$

$$\begin{array}[]{rclcrclcrcl}(p)^{m}&=&p&&(A\to B)^{m}&=&A^{m}\mathbin{-\circ}B^{m}&&(A\wedge B)^{m}&=&A^{m}\otimes B^{m}\\ (t)^{m}&=&1&&(A\vee B)^{m}&=&A^{m}\bindnasrepma B^{m}&&(f)^{m}&=&\perp\end{array}$$

$$\begin{array}[]{rclcrclcrcl}(p)^{g}&=&p&&(A\to B)^{g}&=&\mathop{!}A^{g}\mathbin{-\circ}B^{g}&&(A\wedge B)^{g}&=&A^{g}\with B^{g}\\ (t)^{g}&=&\top&&(A\vee B)^{g}&=&\mathop{!}A^{g}\oplus\mathop{!}B^{g}&&(f)^{g}&=&0\end{array}$$

$$\begin{array}[]{rclcrclcrcl}(p)^{p}&=&\mathop{!}p&&(A\to B)^{p}&=&\mathop{!}(A^{p}\mathbin{-\circ}B^{p})&&(A\wedge B)^{p}&=&A^{p}\otimes B^{p}\\ (t)^{p}&=&1&&(A\vee B)^{p}&=&A^{p}\oplus B^{p}&&(f)^{p}&=&0\end{array}$$

$$\begin{array}[]{rclcrclcrcl}(p)^{0}&=&p&&(A\to B)^{0}&=&\mathop{!}A^{1}\mathbin{-\circ}\mathop{!}B^{0}&&(A\wedge B)^{0}&=&\mathop{!}A^{0}\with\mathop{!}B^{0}\\ (t)^{0}&=&\top&&(A\vee B)^{0}&=&\mathop{!}A^{0}\oplus\mathop{!}B^{0}&&(f)^{0}&=&0\\ \\ (p)^{1}&=&p&&(A\to B)^{1}&=&\mathop{!}(\mathop{!}A^{0}\mathbin{-\circ}B^{1})&&(A\wedge B)^{1}&=&\mathop{!}(A^{1}\with B^{1})\\ (t)^{1}&=&1&&(A\vee B)^{1}&=&\mathop{!}A^{1}\oplus\mathop{!}B^{1}&&(f)^{1}&=&0\end{array}$$

$$\begin{array}[]{lll l lll l lll}(s)^{pt}&=&\texttt{s}&&(\{\})^{pt}&=&1\\ (\{s\}\uplus M)^{pt}&=&(s)^{pt}\otimes(M)^{pt}&&(r:M\rhd M^{\prime})&=&!((M)^{pt}\mathbin{-\circ}(M^{\prime})^{pt})\end{array}$$

Full text

1 Introduction

Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. For intuitionistic logic, several small collections of formulas have been published and used for testing ATP systems. Raths, Otten and Kreitz [25] consolidated and extended these small sets to provide the ILTP Library111http://iltp.de/ for first-order and propositional intuitionistic logic. For modal systems there are at least two libraries of theorems [32, 24].

In this paper, we provide a library for benchmarking Girard’s linear logic [12]. Linear logic is a substructural logic that is a refinement of classical and intuitionistic logic, combining the dualities of the former with many of the constructive properties of the latter. Ideas from linear logic have been influential in fields such as programming languages, game semantics, quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction. In particular, linear logic has had an important role as a logical framework for specifying and reasoning about logical and computational systems (the list is long; some examples are [7, 20, 9, 23]). As a consequence, several provers have been built for linear logic for different purposes (listing some: Sympli 222https://github.com/chaudhuri/sympli, llprover333http://bach.istc.kobe-u.ac.jp/llprover/, LL prover444https://github.com/wujuihsuan2016/LLprover, linTAP555http://www.leancop.de/lintap/, LL prover explorer666https://github.com/andykitchen/linear-logic, Lolli777http://www.lix.polytechnique.fr/~dale/lolli/, Alcove888http://cic.puj.edu.co/~caolarte/alcove2/). However, so far, there has been no discussion about the efficiency or adequacy of these provers. In this work we present a comprehensive collection of propositional tests. Moreover, with the aim of comparing proofs obtained from different translations of intuitionistic problems, we use a prototypical prover, based on focusing, to run some experiments.

When designing a benchmark, one has to carefully decide on a set of formulas that is meaningful in, at least, three ways: (1) the formulas should be able to distinguish several different characteristics of the logical systems and provers; (2) the set should contain important theorems and paradigmatic formulas (non necessarily provable); and (3) the set should be large enough, so to serve as a comparison for different provers and systems. We first concentrate on (1) and (2), comparing translations of a (small) set of intuitionistic formulas into linear logic. This will enable the discussion of other possible approaches to follow. We will then deal with (3), by introducing a library with more than 4.000 problems, including different translations of intuitionistic formulas as well as translations of reachability problems in Petri nets as linear logic sequents.

Starting with (1), it turns out that propositional linear logic ($\mathsf{LL}$) has many aspects that need to be considered. For example, one could adopt its classical ($\mathsf{CLL}$) or intuitionistic ($\mathsf{ILL}$) versions. Hence one important task would be to determine the difference in provability between them, and this is already far from trivial. While it is possible to differentiate the syntax of formulas and the presentation of the inference rules by the standard restriction on the right context to having at most one formula in $\mathsf{ILL}$999We note that in the literature there are two versions of $\mathsf{ILL}$, having at most or exactly one formula in the right context. This is similar to the problem of considering intuitionistic/minimal logics. Since in this work we will use a multiplicative fragment of $\mathsf{ILL}$, we adopted the version of $\mathsf{ILL}$ having $\bot$ in the grammar., $\mathsf{FILL}$ [3] is a multiple-conclusion system with the same connectives and rules as $\mathsf{CLL}$, but restricting the form of the application of such rules. Restricting ourselves to formulas with the same syntax in classical and intuitionistic versions of $\mathsf{LL}$, the first interesting question would be which formulas are provable in $\mathsf{CLL}$ but not in $\mathsf{ILL}$. This is the same issue e.g. when building a benchmark for intuitionistic logic versus the existing ones for classical logic. But the linear case is far more complicated, since the lack of the structural rules of weakening and contraction in both $\mathsf{ILL}$ and $\mathsf{CLL}$ makes these systems “closer” to each other than in the case of classical and intuitionistic logics. Indeed, only very recently [14] the first conservativity results presented in [27] were generalized.

Another important aspect to be taken into consideration is focusing [2]. It turns out that both $\mathsf{ILL}$ and $\mathsf{CLL}$ admit complete focused proof systems, and provers can be built using proof search strategies based on this discipline, which reduces the proof search space. This has an immediate effect on the proposal of formulas composing a possible benchmark library, since the amount of exponentials in a formula can make a significant difference on the performance of provers.

Concerning (2), there is no consensus in the community on a set of “principal” theorems that should be used as a test for $\mathsf{LL}$-based theorem provers. In this work, we will start the discussion by considering the translation of a fragment of Kleene s basic list of intuitionistic logic ($\mathsf{IL}$). The first challenge is to understand how these intuitionistic theorems should be interpreted in $\mathsf{LL}$. A first answer would be: use one of the well known translations of $\mathsf{IL}$ into $\mathsf{LL}$. This naive approach has, at least, two problems. First, it is not adequate to elect one translation, since different translations have very different computational behaviors, as it will be clear in Section 2.2. Second, some translations would not give the best interpretation of linear logic formulas. As a simple example, $A\to A$ should most probably be translated as $A\mathbin{-\circ}A$, without exponentials since this is equivalent, as a theorem, to the identity. But any sound translation from $\mathsf{IL}$ to $\mathsf{LL}$ adds exponentials to implicational formulas. Hence none of them would preserve the axiom’s interpretation.

To achieve desiderata (3), we start by applying four different translations from $\mathsf{IL}$ to $\mathsf{LL}$ using Kleene’s collection of $\mathsf{IL}$ theorems. One of the translations is not validity perserving, resulting in 22 non-provable formulas. We propose provable versions (not following any systematic translation) for those. This gives a initial set of 271 sequents for our library. Next, we apply to all the propositional formulas of the ILTP library the three provability preserving translations considered in this work. This whole set will not only provide some interesting insights on different behaviors of $\mathsf{LL}$ formulas coming from different translations in the literature, but also present a significant set of 1.086 formulas for benchmarking linear logic based provers. Finally, to enlarge the number of problems in our library, we have generated automatically several reachability problems from the large collection of Petri nets101010We thank Frank Pfenning, who suggested the use of Petri nets during the TLLA/Linearity 2018 meeting., available in the Petri Nets Repository111111https://pnrepository.lip6.fr/. Then, by using the standard translation of Petri nets as $\mathsf{ILL}$ formulas [18, 5], we add to our benchmark 3.137 formulas of different levels of difficulty. All these 4.494 formulas will constitute our ILLTP library for intuitionistic linear logic, available at:

https://github.com/meta-logic/lltp.

Outline. The rest of the paper is organized as follows. Section 2 presents $\mathsf{LL}$, focusing, translations and decorations; Section 3 explains the different parts that make ILLTP, and some experiment results; Section 4 concludes the paper and presents some future research directions.

2 Linear Logic

Although we assume that the reader is familiar with linear logic, we review some of its basic proof theory (see [31] for more details).

Linear logic is a substructural logic proposed by Girard [12] as a refinement of classical and intuitionistic logic. Formulas for propositional linear logic ($\mathsf{LL}$) are built from the following grammar

[TABLE]

where atomic formulas $p$ or their negations $p^{\perp}=p\mathbin{-\circ}\bot$ are called literals. The logical connectives for $\mathsf{LL}$ can be divided into the following groups: the multiplicative version of conjunction, true, disjunction, and false, which are written as $\otimes$, $1$, $\bindnasrepma$, $\perp$, respectively; and the additive version of these connectives, which are written as $\with$, $\top$, $\oplus$, [math], respectively; and the exponentials $\mathop{!}$ and $\mathord{?}$.

In this work we will concentrate on intuitionistic linear logic ($\mathsf{ILL}$) [12], having sequents of the form $\Gamma\vdash\Delta$ where $\Delta$ has at most one formula and $\Gamma$ is a multiset of formulas built from the grammar above, except for the connective $\bindnasrepma$ and the exponential $\mathord{?}$. The rules of $\mathsf{ILL}$ are depicted in Figure 1.

2.1 Focusing

Andreoli introduced in [2] a notion of normal form for cut-free derivations in linear logic. The connectives of $\mathsf{LL}$ can be divided into two classes: negative ($\bindnasrepma$, $\perp$, $\with$, $\top$, and $\mathord{?}$) and positive ($\otimes$, $1$, $\oplus$, [math], and $\mathop{!}$). Note that the dual of a negative connective is positive and vice-versa. In general, the right introduction rules for negative connectives are invertible, meaning that the conclusion of any of these introduction rules is equivalent to its premises. The right introduction rules for the positive connectives are not necessarily invertible, and may require a choice or a context restriction on the application of rules. The notions of negative and positive polarities are extended to formulas in the natural way by considering the outermost connective, e.g., $A\oplus B$ is positive while $A\with B$ is negative. Any bias can be assigned to atomic $\mathsf{LL}$ formulas.

A focused proof is organized around two “phases” of proof construction: the negative phase for introducing negative connectives on the succedent or positive ones in the antecedent, and the positive phase for the positive connectives on the succedent or negative ones in the antecedent. In the focusing discipline, formulas are decomposed eagerly in the negative phase, until only positive formulas on the succedent or negative on the antecedent are left. Then one of them is non-deterministically chosen to be focused on.

The focused system $\mathsf{ILLF}$ for intuitionistic linear logic is presented in Figure 2. There are three kinds of arrows in this proof system and a pair of contexts to the left of the arrows:

• •

$\Theta$ is a set of antecedent formulas whose main connective is a bang, being hence the unbounded (classical) context;

• •

$\Gamma$ is a multiset of linear formulas, behaving as the bounded (linear) context;

• •

sequents of the form $\Theta:\Gamma-_{\_}{F}\!\!\to$ or $\Theta:\Gamma\xrightarrow{F}\Delta$ belong to the positive phase and introduce the logical connective of the “focused” formula $F$: building proofs of such sequents may require non-invertible proof steps to be taken;

• •

sequents of the form $\Theta:\Gamma\longrightarrow\Delta$ belong to the negative phase and decompose the multisets $\Gamma,\Delta$ in such a way that only inference rules over negative formulas on the right or positive ones on the left are applied.

The structural rules $D_{\_}{L1},D_{\_}{L2}$ and $D_{\_}R$ make the transition between negative and positive phases. The positive phase begins by choosing a non-atomic fomula $N_{\_}a$ from the classical context or a negative left formula $N$ (resp. a positive right formula $P$) on which to focus using $D_{\_}{L1},D_{\_}{L2}$ (resp. $D_{\_}R$). Atoms in $\mathsf{ILLF}$ always have a positive bias121212Although $\mathsf{ILL}$ can allow any polarity assignment for atomic formulas, we will present here the system that was actually implemented.. Positive rules are applied to $N,N_{\_}a/P$ until either $1$ or an atom is encountered in the right, or $\bot$ is on the left (and, in such cases, the proof must end by applying the respective axiom), or the promotion rule ($\mathop{!}$) is applied, or yet a positive left (respect. negative right) subformula is encountered, when the proof switches to the negative phase by applying $R_{\_}L$ (resp. $R_{\_}R$).

An observation is in order: the system presented in Figure 2 induces a weak focusing, in the sense that, a priori, the positive phase could start even with the presence, in one of the contexts, of formulas amenable to negative rule applications. However, our rewrite-based implementation (see Section 3.3) forces the strong focusing approach: rules in the negative phase are exhaustively applied until a normal form is found, i.e., in all the resulting subgoals, there are no positive formulas in the linear context, nor a negative formula in the succedent.

Finally, we observe that, although focusing is a complete strategy that decreases considerably the search space, it is not enough for avoiding loops on proof search. Let us give two simple examples. A focused proof of the sequent $\cdot:\mathop{!}A,\mathop{!}(\mathop{!}A\mathbin{-\circ}B)\longrightarrow 0$ starts by storing $A,\mathop{!}A\mathbin{-\circ}B$ in the classical context and then it focuses on $\mathop{!}A\mathbin{-\circ}B$ continuously, adding various copies of $B$ in the linear context. Since the sequents produced in this process are all different, no loop detection will work for this case. One way of avoiding this kind of behavior would be by restricting the number of focusing steps over the same formula in the classical context. This is a sound, but not complete, strategy. Another way to deal with this problem would be to introduce a heuristics in order to stop the computation or to modify the sequents, depending on the shape of formulas in the context. In this particular example, it is enough to observe that sequents of the form $\Theta,A,A\mathbin{-\circ}B:\Gamma\longrightarrow C$ can be re-written as $\Theta,A,B,A\mathbin{-\circ}B:\Gamma\longrightarrow C$, and continue by analyzing the formula $B$.

Another pathological behavior may arise with a sequent of the shape $\Theta,P_{\_}1\with P_{\_}2:\Gamma\longrightarrow C$ where $P_{\_}i$ is a positive formula. In this case, if we decide to focus on the formula $P_{\_}1\with P_{\_}2$, we are forced to choose one of the $P_{\_}i$ and then, the positive phase ends by adding yet another copy of $P_{\_}i$ into the linear context. In this particular case, we may use the well known equivalence $!(F\with G)\equiv!F\otimes!G$ and rewrite the above sequent into a simpler one: $\Theta,P_{\_}1,P_{\_}2:\Gamma\longrightarrow C$. If $P_{\_}1$ and $P_{\_}2$ are atomic formulas, this simplification is quite useful since those atoms will remain in the classical context (remember that it is not possible to focus on them) and they will never be added to the linear context.

In a broader sense, the analysis of proof theoretic properties of $\mathsf{LL}$ must guide the design of more advanced/efficient proof search procedures. For instance, invertibility and permutability of rules lead to systems that reduce the non-determinism [11, 2] as already mentioned. Moreover, the resource management problem has been tackled by delaying, as much as possible, the decision on how to split the linear context [6, 17]. On the other hand, systems for forward reasoning have been also explored in the context of $\mathsf{LL}$ (see e.g., [21, 29, 30, 8]), usually showing a better performance that those based on backward reasoning [29, 8]. Since our goal with this work is to present an initial library for $\mathsf{LL}$ and not to test particular theorem provers or automated reasoning techniques, we will not focus our attention on these issues. We just note that no silver-bullet will work in all the cases since, as it is well known, propositional linear logic is undecidable [16].

2.2 Translations and Decorations

A naive approach for building a set of test formulas for $\mathsf{LL}$ based provers would be to use one of the well known translations of intuitionistic (or classical) formulas into $\mathsf{LL}$. Since there are several ways of translating a formula from $\mathsf{IL}$ to $\mathsf{LL}$, we asked ourselves which one would be the best option, if any. Each translation characterizes a different linear view of intuitionistic formulas and it is interesting and relevant to establish a comparison between them. We analyze four: a multiplicative translation, the original Girard’s translation, Girard’s positive translation and Miller and Liang’s $0/1$ translation.

The multiplicative translation trivially substitutes the intuitionistic connectives by their multiplicative linear version

[TABLE]

Translation of sequents is given by $(\Gamma\vdash A)^{m}=\Gamma^{m}\vdash A^{m}$. Observe that this translation does not preserve provability: for instance, diagonals $A\otimes A\to A$ exist in $\mathsf{IL}$, but not in $\mathsf{LL}$.

Girard’s translation [12], also known as call-by-name translation, is the most well known translation of $\mathsf{IL}$ into $\mathsf{LL}$, defined as

[TABLE]

Sequents are translated as $(\Gamma\vdash A)^{g}=\mathop{!}\Gamma^{g}\vdash A^{g}$. Girard’s translation preserves provability but is not a decoration in the sense of [10], namely, a proof of $A$ in $\mathsf{IL}$ is transformed into a proof of $A^{g}$ in $\mathsf{LL}$ which is not isomorphic to the original one.

Girard proposed in the same paper [12] another translation, known as call-by-value translation. Henceforth, we will call this translation positive, since $\mathsf{IL}$ formulas become positive $\mathsf{LL}$ formulas.

[TABLE]

Sequents are translated as $(\Gamma\vdash A)^{p}=\Gamma^{p}\vdash A^{p}$. It is easy to see that the positive translation is a decoration: proofs of $A^{p}$ in $\mathsf{LL}$ are isomorphic to proofs of $A$ in $\mathsf{IL}$ (see [10] for details).

Another interesting translation is the $0/1$ translation [15], which distinguishes the polarity of formulas in a sequent.

[TABLE]

The translation of sequents is given by $(\Gamma\vdash A)^{0/1}=\mathop{!}\Gamma^{0}\vdash A^{1}$. Using this translation, focused proofs in $\mathsf{ILLF}$ are in bijective correspondence with proofs in $\mathsf{IL}$. In a loose sense, this can be considered a decoration if the isomorphism is interpreted “modulo focusing”. In the focusing context, this is referred to as adequacy on the level of derivations [22].

Basically these four translations differ on their use of bangs and polarization of atoms. The multiplicative translation introduces no bangs; Girard’s translation forces backchaining proofs; the positive translation sets the global preference to be forward-chaining and atoms have positive polarity; the $0/1$ translation is asymmetric, and it does not impose restrictions on atoms. Of course, less bangs implies shorter proofs. For instance, consider the $\mathsf{IL}$ sequent $A\to B,B\to C\vdash A\to C$ and the corresponding proofs using the four translations in Figure 3.

3 The ILLTP Library

The ILLTP library is composed of problems from three sources: Kleene’s “Introduction to Metamathematics”, ILTP (a library of problems for intuitionistic theorem provers), and Petri nets from the Model Checking Contest 131313https://pnrepository.lip6.fr/mcc/. We use a syntax similar to TPTP [28]141414http://www.tptp.org, where axioms (formulas on the left side of the sequent) and conjectures (the formula on the right side of the sequent) are specified as fof(name, axiom, F) and fof(name, conjecture, F) respectively. The name chosen is not important. The denominations axiom and conjecture are fixed. F is a linear logic formula built from the connectives: *, &, +, |, -o, !, ?, corresponding to $\otimes$, $\binampersand$, $\oplus$, $\bindnasrepma$, $\multimap$, $!$, $?$, respectively151515 Although our library is used here for $\mathsf{ILL}$, the format of our files and translations support $\mathsf{LL}$ formulas as well, so that our library can be extended to the classical case as well..

3.1 Kleene’s problems

Kleene s traditional book “Introduction to Metamathematics” [13] has a collection of interesting intuitionistic theorems. They are rather straightforward, thus they would not be especially useful for testing the efficiency of a prover. Instead, they can be regarded as a minimal set of intuitionistic theorems that a sound prover should be able to derive. As such, they can be valuable to uncover bugs and unsoundness. Our first goal is to set up a similar set for $\mathsf{LL}$.

The main challenge is to understand how these intuitionistic theorems should be interpreted in $\mathsf{LL}$. Deciding whether to translate intuitionistic disjunction as the multiplicative disjunction $\bindnasrepma$ of linear logic or the additive disjunction $\oplus$ changes the target system under consideration, thus we prefer to not consider the intuitionistic disjunction to begin with. Hence we will start by considering what we call the rudimentary fragment of $\mathsf{IL}$, which is very well-behaved: semantically this fragment corresponds to cartesian closed categories. Figure 4 shows the 61 theorems considered.

Applying each translation defined in Section 2.2 to these 61 sequents gives rise to 244 different $\mathsf{ILL}$ sequents. As already noted, provability is not preserved in the multiplicative translation. The reason for that, other than the obvious absence of structural rules in the left context, is that the multiplicative false $\bot$ is relevant, so while $0\vdash B$ for any $B$, $A\otimes(A\mathbin{-\circ}\bot)\not\vdash B$ in $\mathsf{LL}$. The other three translations fix this by systematically adding bangs and additive connectives.

The multiplicative translation of all sequents in Kleene’s list is in Appendix A, including the 22 ones that are not provable (indicated by $\not\vdash$). In Figure 5 we present an alternative translation for them, using a small number of bangs and/or additives.

3.2 ILTP problems

The problems from the ILTP library for intuitionistic theorem provers [25] were parsed and translated into linear logic using the three provability preserving translations presented in Section 2.2. Due to the number and size of problems, it is unpractical to apply the multiplicative translation and find the unprovable sequents to propose an alternative translation as it was done with the previous set of problems.

The original library contains 274 problems (including theorems and non-theorems), separated into three categories: LCL (logical calculi), SYJ and SYN (syntactic problems that have no obvious interpretation in intuitionistic and classical logic, respectively). Their translation resulted in 822 linear logic problems. Moreover, we also considered the remaining Kleene’s theorems in  [13] (i.e., those out of the rudimentary fragment) resulting in a total of 1.086 problems in this collection.

3.3 Comparing translations

We specified $\mathsf{IL}$ and different fragments of linear logic in rewriting logic ($\mathsf{RW}$, see e.g. [19]) and implemented in Maude161616http://maude.cs.uiuc.edu a very basic prover for $\mathsf{IL}$ as well as for $\mathsf{ILLF}$ and $\mathsf{LLF}$. The use of $\mathsf{RW}$ leads to a clear separation between deterministic inference rules that can be eagerly applied (as those in the negative phase) and non-deterministic inference rules where backtracking may be needed (as those in the positive phase). Moreover, the minimal distance between the represented logic ($\mathsf{IL}$, $\mathsf{ILLF}$ and $\mathsf{LLF}$) and its specification in $\mathsf{RW}$ allowed us to quickly implement a good prototypical tool useful for our tests. Although more efficient provers can be built by e.g., including sophisticated heuristics and specialized data structures, our prototypical implementations were enough to compare the different translations.

Using these provers, we generated LaTeX proofs for the intuitionistic problems from Kleene and ILTP, plus for all $\mathsf{ILL}$ translations of the sequents, when provable. These results can be found in the PDFs at

https://github.com/carlosolarte/Linear-Logic-Prover-in-Maude

in the directory output.

The proofs are grouped by intuitionistic problem, so one can compare the shape and size of the original intuitionistic proofs and their linear versions resulted from each translation. A summary of the results is presented in Table 1.

3.4 Petri nets problems

Petri nets (see e.g. [26]) are a model for distributed systems that generalize automata and hence also transition systems. Local states in the net are called places (denoted graphically as a circle) and the global state is a multiset of local states called a marking. A certain number $n$ of copies of a local state $s$ in a marking $M$ is denoted as $n$ tokens (graphically bullets) inside the circle $s$. Transitions produce and consume tokens, representing transformations in the local states.

Abstractly, we can see a Petri net as a multiset rewrite system and thus, there is a natural connection with the multiplicative fragment of linear logic [4]. More precisely, a transition system over the set of places $S$ is a set of rewrite rules of the form $r:\bullet t\rhd t\bullet$ where $\bullet t$ and $t\bullet$ are multisets on $S$, usually called preset and postset. As expected, the rule $r$ is enabled in a marking (global state) $M$ if $\bullet t$ is a multisubset of $M$. Then, $M$ reduces to $M^{\prime}$, notation $M\rhd M^{\prime}$, where $M^{\prime}=M\setminus\bullet t\uplus t\bullet$. Let $\rhd^{*}$ be the reflexive and transitive closure of $\rhd$. We say that $M^{\prime}$ is reachable from $M$ if $M\rhd^{*}M^{\prime}$.

Let $s\in S$ be a place and $M,M^{\prime}$ be a multisets on $S$. Then, we can encode places, markings and rules as follows [4]:

[TABLE]

where s is an atomic proposition. Given a set of transitions $\mathcal{R}$, the reachability problem whether $M\rhd^{*}M^{\prime}$ can be encoded as the $\mathsf{ILL}$ sequent $\bigotimes\limits_{\_}{r\in\mathcal{R}}(r)^{pt}\vdash(M)^{pt}\mathbin{-\circ}(M^{\prime})^{pt}$.

The Petri Nets Repository171717https://pnrepository.lip6.fr/ contains a large collection of Petri nets in PNML (Petri Net Markup Language181818http://pnml.lip6.fr/) syntax, an XML with tags for places and transitions (or “arcs”), and a way to represent the initial marking. We wrote scripts that translate PNML into a simple Maude program that can perform transitions in the net, transforming the markings. This program was used to generate final markings of the Petri nets after 1, 5, 10, 20, 50 and 100 transitions. Each final marking, together with the Petri net specification, is a reachability problem in linear logic, which was written in the ILLTP format (described at the beginning of Section 3) using the translation above. It is worth noticing that some nets are cyclic (deadlock free transition systems), hence it is possible that the marking after $n$ transition can be also obtained after $m<n$ transitions. This procedure allowed us to generate 3.137 new problems.

4 Conclusion

In this work we proposed an initial set of problems as a library for benchmarking linear logic based provers. Starting with the $(\to,\land)$-fragment of Kleene’s theorems, we generated 244 different $\mathsf{ILL}$ sequents using 4 automatic translations: multiplicative, call-by-name, call-by-value and 0/1. The first translation is the only one that does not preserve provability. For each of those 22 $\mathsf{ILL}$ sequents that are not provable via the multiplicative translation, we proposed an alternative provable sequent with a small set of additives and bangs added. This makes these particular sequents amenable to the use of all the power of focusing theorem provers. In fact, the excess of bangs in formulas tends to neutralize the efficacy of focusing, due to the positive/negative behavior of the exponentials. Thus our initial proposal for a suitable benchmark for $\mathsf{ILL}$ has 271 formulas, testing aspects like provability and focusing.

It is worth noticing that (1) we include $\bot$ in the grammar of $\mathsf{ILL}$; (2) all the sequents of our collection can also serve as tests in $\mathsf{CLL}$. The decision in (1) was motivated by the fact that the resulting sequents fall into the multiplicative fragment of $\mathsf{ILL}$. However, observe that one could clearly exchange $\bot$ for [math] in the multiplicative translation (that would not be multiplicative anymore) and still obtain a significant set of 23 formulas not provable via this new translation.

We then moved in the direction of increasing the amount of formulas in our library, still using the translation approach. For that, we took all the 274 formulas from the ILTP Library and applied the three sound translations from $\mathsf{IL}$ to $\mathsf{LL}$ considered in this work. At this point, our library had already 1.093 formulas to be tested. For an initial experiment with this first proposed set of sequents, we implemented a focused-based prover for $\mathsf{ILL}$. This allowed us to compare well known $\mathsf{LL}$ translations for $\mathsf{IL}$ formulas, not only considering the time needed for proving a sequent: our results give a comprehensive collection of proofs where it is possible to visualize the different shapes (and sizes) of such proofs.

Finally, following Frank Pfenning’s suggestion, we have generated automatically several reachability problems from the large collection of Petri nets. This not only moves us out of intuitionistic logic examples, but it also considers a serious amount of problems that are actually used for testing Petri nets model checkers.

It should be noted that these are only the first steps on the direction of benchmarking linear logic. For future work, we intend to test different provers already available online and to propose a large collection of formulas dedicated to classical linear logic $\mathsf{CLL}$.

Appendix A Multiplicative translation of Kleene’s list

$\vdash A\mathbin{-\circ}A$ (identity) 2. 2.

$A\mathbin{-\circ}B,B\mathbin{-\circ}C\vdash A\mathbin{-\circ}C$ (transitivity of implication) 3. 3.

$A\mathbin{-\circ}(B\mathbin{-\circ}C)\vdash B\mathbin{-\circ}(A\mathbin{-\circ}C)$ (exchange of premises) 4. 4.

$A\mathbin{-\circ}(B\mathbin{-\circ}C)\vdash A\otimes B\mathbin{-\circ}C$ (uncurrying) 5. 5.

$A\otimes B\mathbin{-\circ}C\vdash A\mathbin{-\circ}(B\mathbin{-\circ}C)$ (currying) 6. 6.

$A\mathbin{-\circ}B\vdash(B\mathbin{-\circ}C)\mathbin{-\circ}(A\mathbin{-\circ}C)$ (precomposing maps) 7. 7.

$A\mathbin{-\circ}B\vdash(C\mathbin{-\circ}A)\mathbin{-\circ}(C\mathbin{-\circ}B)$ (post-composing maps) 8. 8.

$A\mathbin{-\circ}B\vdash A\otimes C\mathbin{-\circ}B\otimes C$ (tensor is a bifunctor) 9. 9.

$A\mathbin{-\circ}B\vdash C\otimes A\mathbin{-\circ}C\otimes B$ (tensor is a bifunctor) 10. 10.

$A^{\bot}\not\vdash A\mathbin{-\circ}B$ 11. 11.

$A\not\vdash A^{\bot}\mathbin{-\circ}B$ 12. 12.

$B\not\vdash A\mathbin{-\circ}B$ but (projection is non-linear) 13. 13.

$A\mathbin{-\circ}B\vdash B^{\bot}\mathbin{-\circ}A^{\bot}$ (linear negation is contravariant) 14. 14.

$A\mathbin{-\circ}B^{\perp}\vdash B^{\perp}\mathbin{-\circ}A^{\perp}$ 15. 15.

$A\mathbin{-\circ}B,B\mathbin{-\circ}A\vdash A\multimapboth B$ 16. 16.

$A\multimapboth B\not\vdash A\mathbin{-\circ}B$ (cannot throw away $B\mathbin{-\circ}A$) 17. 17.

$A\multimapboth B\not\vdash B\mathbin{-\circ}A$ (cannot throw away $A\mathbin{-\circ}B$) 18. 18.

$A\multimapboth B,A\not\vdash B$ 19. 19.

$A\multimapboth B,B\not\vdash A$ 20. 20.

$\vdash A\multimapboth A$ 21. 21.

$A\multimapboth B\vdash B\multimapboth A$ 22. 22.

$A\multimapboth B,B\multimapboth C\vdash A\multimapboth C$ 23. 23.

$A\mathbin{-\circ}(B\mathbin{-\circ}C),A^{{\bot}{\bot}},B^{{\bot}{\bot}}\vdash C^{{\bot}{\bot}}$ 24. 24.

$(A\mathbin{-\circ}B)^{{\bot}{\bot}}\vdash A^{{\bot}{\bot}}\mathbin{-\circ}B^{{\bot}{\bot}}$ (double negation is a functor) 25. 25.

$(A\mathbin{-\circ}B)^{{\bot}{\bot}},(B\mathbin{-\circ}C)^{{\bot}{\bot}}\vdash(A\mathbin{-\circ}C)^{{\bot}{\bot}}$ 26. 26.

$\not\vdash(A\otimes B)^{{\bot}{\bot}}\multimapboth A^{{\bot}{\bot}}\otimes B^{{\bot}{\bot}}$ 27. 27.

$\not\vdash(A\multimapboth B)^{{\bot}{\bot}}\multimapboth(A\mathbin{-\circ}B)^{{\bot}{\bot}}\otimes(B\mathbin{-\circ}A)^{{\bot}{\bot}}$ 28. 28.

$A\multimapboth B\vdash(A\mathbin{-\circ}C)\multimapboth(B\mathbin{-\circ}C)$ 29. 29.

$A\multimapboth B\vdash(C\mathbin{-\circ}A)\multimapboth(C\mathbin{-\circ}B)$ 30. 30.

$A\multimapboth B\vdash(A\otimes C)\multimapboth(B\otimes C)$ 31. 31.

$A\multimapboth B\vdash(C\otimes A)\multimapboth(C\otimes B)$ 32. 32.

$A\multimapboth B\vdash A^{\bot}\multimapboth B^{\bot}$ 33. 33.

$\vdash((A\otimes B)\otimes C)\multimapboth(A\otimes(B\otimes C))$. 34. 34.

$\vdash A\otimes B\multimapboth B\otimes A$ 35. 35.

$\not\vdash A\otimes A\multimapboth A$ ($\otimes$ is not idempotent) 36. 36.

$A\not\vdash(A\mathbin{-\circ}B)\multimapboth B$ 37. 37.

$B\not\vdash(A\mathbin{-\circ}B)\multimapboth B$ 38. 38.

$A^{\perp}\not\vdash(A\mathbin{-\circ}B)\multimapboth A^{\perp}$ 39. 39.

$B^{\perp}\not\vdash(A\mathbin{-\circ}B)\multimapboth A^{\perp}$ 40. 40.

$B\not\vdash(A\otimes B)\multimapboth A$ 41. 41.

$B^{\perp}\not\vdash((\mathop{!}A\otimes B)\mathbin{-\circ}B)\otimes(B\mathbin{-\circ}(A\otimes B))$ 42. 42.

$\vdash A\mathbin{-\circ}A^{\perp\perp}$ 43. 43.

$\vdash A^{\perp\perp\perp}\multimapboth A^{\perp}$ 44. 44.

$\vdash(A\otimes A^{\perp})^{\perp}$ 45. 45.

$\not\vdash(A\multimapboth A^{\perp})^{\perp}$ 46. 46.

$\not\vdash(((A\mathbin{-\circ}0)\mathbin{-\circ}0)\mathbin{-\circ}A)^{\perp\perp}$ 47. 47.

$\not\vdash A\otimes(B\otimes B^{\perp})\multimapboth(B\otimes B^{\perp})$ 48. 48.

$\vdash(A\mathbin{-\circ}B)\mathbin{-\circ}(A\otimes B^{\perp})^{\perp}$ 49. 49.

$\vdash(A\mathbin{-\circ}B^{\perp})\multimapboth(A\otimes B)^{\perp}$ 50. 50.

$\vdash(A\otimes B)^{\perp}\multimapboth(A^{\perp\perp}\mathbin{-\circ}B^{\perp})$ 51. 51.

$B^{\perp\perp}\mathbin{-\circ}B\vdash(A^{\perp\perp}\mathbin{-\circ}B)\multimapboth(A\mathbin{-\circ}B)$ 52. 52.

$B^{\perp\perp}\mathbin{-\circ}B\vdash(A\mathbin{-\circ}B)\multimapboth(A\otimes B^{\perp})^{\perp}$ 53. 53.

$\vdash(A^{\perp\perp}\mathbin{-\circ}B)\mathbin{-\circ}(A\otimes B^{\perp})^{\perp}$ 54. 54.

$\vdash A\otimes B\mathbin{-\circ}(A\mathbin{-\circ}B^{\perp})^{\perp}$ 55. 55.

$\vdash A\otimes B^{\perp}\mathbin{-\circ}(A\mathbin{-\circ}B)^{\perp}$ 56. 56.

$\vdash(A^{\perp\perp}\otimes B)\mathbin{-\circ}(A\mathbin{-\circ}B^{\perp})^{\perp}$ 57. 57.

$\not\vdash(A^{\perp\perp}\otimes B^{\perp})\multimapboth(A\mathbin{-\circ}B)^{\perp}$ 58. 58.

$\not\vdash(A\mathbin{-\circ}B)^{\perp}\multimapboth(A\otimes B^{\perp})^{\perp\perp}$ 59. 59.

$\not\vdash(A\mathbin{-\circ}B)^{\perp\perp}\multimapboth(A\otimes B^{\perp})^{\perp}$ 60. 60.

$\vdash(A\otimes B^{\perp})^{\perp}\multimapboth(A\mathbin{-\circ}B^{\perp\perp})$ 61. 61.

$\vdash(A\mathbin{-\circ}B^{\perp\perp})\multimapboth(A^{\perp\perp}\mathbin{-\circ}B^{\perp\perp})$