  The problem we want to solve is how to generate all theorems of a given size
in the implicational fragment of propositional intuitionistic linear logic. We
start by filtering for linearity the proof terms associated by our Prolog-based
theorem prover for Implicational Intuitionistic Logic. This works, but using
for each formula a PSPACE-complete algorithm limits it to very small formulas.
We take a few walks back and forth over the bridge between proof terms and
theorems, provided by the Curry-Howard isomorphism, and derive step-by-step an
efficient algorithm requiring a low polynomial effort per generated theorem.
The resulting Prolog program runs in O(N) space for terms of size N and
generates in a few hours 7,566,084,686 theorems in the implicational fragment
of Linear Intuitionistic Logic together with their proof terms in normal form.
As applications, we generate datasets for correctness and scalability testing
of linear logic theorem provers and training data for neural networks working
on theorem proving challenges. The results in the paper, organized as a
literate Prolog program, are fully replicable.
  Keywords: combinatorial generation of provable formulas of a given size,
intuitionistic and linear logic theorem provers, theorems of the implicational
fragment of propositional linear intuitionistic logic, Curry-Howard
isomorphism, efficient generation of linear lambda terms in normal form, Prolog
programs for lambda term generation and theorem proving.
