English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The problem we want to solve is how to generate all theorems of a given sizein the implicational fragment of propositional intuitionistic linear logic. Westart by filtering for linearity the proof terms associated by our Prolog-basedtheorem prover for Implicational Intuitionistic Logic. This works, but usingfor 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 andtheorems, provided by the Curry-Howard isomorphism, and derive step-by-step anefficient algorithm requiring a low polynomial effort per generated theorem.The resulting Prolog program runs in O(N) space for terms of size N andgenerates in a few hours 7,566,084,686 theorems in the implicational fragmentof Linear Intuitionistic Logic together with their proof terms in normal form.As applications, we generate datasets for correctness and scalability testingof linear logic theorem provers and training data for neural networks workingon theorem proving challenges. The results in the paper, organized as aliterate Prolog program, are fully replicable.  Keywords: combinatorial generation of provable formulas of a given size,intuitionistic and linear logic theorem provers, theorems of the implicationalfragment of propositional linear intuitionistic logic, Curry-Howardisomorphism, efficient generation of linear lambda terms in normal form, Prologprograms for lambda term generation and theorem proving.

Deriving Theorems in Implicational Linear Logic, Declaratively