Deriving Theorems in Implicational Linear Logic, Declaratively

• URL: http://arxiv.org/abs/2009.10241v1
• Date: Tue, 22 Sep 2020 00:48:45 GMT
• Title: Deriving Theorems in Implicational Linear Logic, Declaratively
• Authors: Paul Tarau (University of North Texas), Valeria de Paiva (Topos Institute)
• Abstract summary: We show how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation. For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  Humans can develop new theorems to explore broader and more complex mathematical results. Current generative language models (LMs) have achieved significant improvement in automatically proving theorems. This paper proposes an Automated Theorem Generation benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems.
  arXiv  Detail & Related papers  (2024-05-05T02:06:37Z)
• LeanReasoner: Boosting Complex Logical Reasoning with Lean [19.486080494198724]
  Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty of such reasoning. We use Lean, a theorem proving framework, to address these challenges. By formalizing logical reasoning problems into theorems within Lean, we can solve them by proving or disproving the corresponding theorems.
  arXiv  Detail & Related papers  (2024-03-20T05:29:06Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
  Automated Theorem Proving deals with the development of computer programs being able to show that some conjectures (queries) are a logical consequence of a set of axioms (facts and rules) Recent approaches have proposed transformer-based architectures for deriving conjectures given axioms expressed in natural language (English) In this work we propose a new architecture, namely the Neural Unifier, which achieves state-of-the-art results in term of generalisation.
  arXiv  Detail & Related papers  (2021-09-17T10:48:39Z)
• Neural Proof Nets [0.8379286663107844]
  We propose a neural variant of proof nets based on Sinkhorn networks, which allows us to translate parsing as the problem of extracting primitive primitive permuting them into alignment. We test our approach on AEThel, where it manages to correctly transcribe raw text sentences into proofs and terms of the linear lambda-calculus with an accuracy of as high as 70%.
  arXiv  Detail & Related papers  (2020-09-26T22:48:47Z)
• Partial Orders, Residuation, and First-Order Linear Logic [0.20305676256390934]
  We will show that adding partial order constraints in such a way as each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators.
  arXiv  Detail & Related papers  (2020-08-14T13:06:21Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic [13.633012068936894]
  We study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings. Our experiments show that the advantages of simpler encoding schemes in terms of runtime are outdone by more complex graph-based embeddings.
  arXiv  Detail & Related papers  (2020-02-02T16:07:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.