Deriving Theorems in Implicational Linear Logic, Declaratively
This work provides a scalable method for generating large datasets to test and train theorem provers and neural networks in linear logic, though it is incremental as it builds on existing Curry-Howard isomorphism and Prolog-based techniques.
The paper tackled the problem of generating all theorems of a given size in implicational linear intuitionistic logic by developing an efficient algorithm that reduces computational effort from PSPACE-complete to low polynomial per theorem, resulting in the generation of 7,566,084,686 theorems and their proof terms in a few hours.
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.