论文标题
以暗示的线性逻辑得出定理，声明
Deriving Theorems in Implicational Linear Logic, Declaratively
论文作者
论文摘要
我们要解决的问题是如何在命题直觉线性逻辑的暗示片段中生成给定大小的所有定理。我们首先要过滤线性，以基于序言的定理供体相关联的证明术语，以实现直觉逻辑。这有效，但是对于每个公式A PSPACE算法算法将其限制为非常小的公式。我们在证明项和定理之间的桥梁上来回走几步，由咖喱 - 霍德同构提供，并得出逐步得出有效的算法，需要每个生成的定理的多项式努力。由此产生的Prolog程序在o（n）空间中以尺寸n的术语运行，并在几个小时内生成7,566,084,686个定理，在线性直觉逻辑的暗示片段中以及其正常形式的证明项。作为应用程序，我们生成数据集，以实现线性逻辑定理的正确性和可伸缩性测试，并针对从事定理的神经网络培训数据证明挑战。本文中作为识字序言计划组织的结果是完全可复制的。 关键字：具有给定尺寸，直觉和线性逻辑定理的可证明的公式的组合，是命题线性直觉逻辑的暗示片段的定理，咖喱同构，有效地生成正常形式的线性lambda术语，正常的prolog sprog，prolog in for lambda prove of terlamda prov ofst overem overem overem overem oferem oferem servering。
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.
