Deriving Theorems in Implicational Linear Logic, Declaratively

TL;DR

This paper presents an efficient algorithm for generating all the theorems of a specific size in the implicational fragment of propositional linear intuitionistic logic, enabling large-scale theorem dataset creation.

Contribution

It introduces a polynomial-effort algorithm for theorem generation based on proof term analysis, improving over previous PSPACE-complete methods.

Findings

Generated over 7.5 billion theorems in a few hours

Developed a Prolog program with O(N) space complexity

Provided datasets for testing and training neural theorem provers

Abstract

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.