Deriving Theorems in Implicational Linear Logic, Declaratively

Paul Tarau, Valeria de Paiva

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 l…