Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generating Theorems by Generating Proof Structures

Christoph Wernhard

TL;DR

The paper addresses generating theorems from a fixed axiom set without a specific goal by leveraging condensed detachment and proof-structure enumeration, framed within a formulas-as-types perspective and connected to Metamath. It introduces inductive level characterizations and bottom-up SGCD-based theorem generation, then enhances this with DAG-based lemma synthesis and the incorporation of combinators to compress proof terms. On a Metamath POI benchmark (1,374 theorems), the authors generate proofs for 697 theorems (including 10 with rating 1) and show that lemmas markedly boost automated provers (e.g., Vampire and leanCoP) in solving POI problems. They further extend the approach with combinatory proof schemas, obtaining an additional 116 POI theorems (totaling 734), including 12 highly challenging ones, demonstrating the practical impact of structured proof-term generation for automated reasoning. The work unifies automated proving and theorem generation under a chain of techniques (CD, DAG compression, combinators, and PSP-like schemas), offering a scalable framework for lemma discovery and improved prover performance with potential extensions to richer logics and premise selection.

Abstract

We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, we convert a fragment of the Metamath database set.mm. Our techniques are centered on proof terms and condensed detachment, which ties in with approaches to automated first-order proving by proof structure enumeration, and links to Metamath as well as to formulas-as-types. Our methods for generating theorems are based on partitioning the set of proof terms into inductively characterized levels. We study two ideas for improvement: Lemma synthesis by DAG compression of proof term sets and incorporating combinators into proof term construction.

Generating Theorems by Generating Proof Structures

TL;DR

The paper addresses generating theorems from a fixed axiom set without a specific goal by leveraging condensed detachment and proof-structure enumeration, framed within a formulas-as-types perspective and connected to Metamath. It introduces inductive level characterizations and bottom-up SGCD-based theorem generation, then enhances this with DAG-based lemma synthesis and the incorporation of combinators to compress proof terms. On a Metamath POI benchmark (1,374 theorems), the authors generate proofs for 697 theorems (including 10 with rating 1) and show that lemmas markedly boost automated provers (e.g., Vampire and leanCoP) in solving POI problems. They further extend the approach with combinatory proof schemas, obtaining an additional 116 POI theorems (totaling 734), including 12 highly challenging ones, demonstrating the practical impact of structured proof-term generation for automated reasoning. The work unifies automated proving and theorem generation under a chain of techniques (CD, DAG compression, combinators, and PSP-like schemas), offering a scalable framework for lemma discovery and improved prover performance with potential extensions to richer logics and premise selection.

Abstract

We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, we convert a fragment of the Metamath database set.mm. Our techniques are centered on proof terms and condensed detachment, which ties in with approaches to automated first-order proving by proof structure enumeration, and links to Metamath as well as to formulas-as-types. Our methods for generating theorems are based on partitioning the set of proof terms into inductively characterized levels. We study two ideas for improvement: Lemma synthesis by DAG compression of proof term sets and incorporating combinators into proof term construction.
Paper Structure (36 sections, 18 equations, 3 figures, 17 tables)

This paper contains 36 sections, 18 equations, 3 figures, 17 tables.

Table of Contents

  1. Introduction
  2. Technical Framework: Condensed Detachment
  3. POI: A Benchmark Theorem Set from set.mm
  4. An Approach to Generating Proof Structures
  5. POI-Base: An Easy-to-Generate Subset of POI
  6. Lemma Synthesis via Proof Term Compression
  7. Computing the Lemmas.
  8. Lemma-Enhanced Theorem Generation with SGCD.
  9. Lemma-Enhanced First-Order Theorem Proving.
  10. Precision Aspects.
  11. Theorem Generation with Combinatory Proof Schemas
  12. Proof Patterns with Combinatory Definitions.
  13. The PSP Level for Proof Schemas.
  14. Theorem Generation with SGCD and Proof Schemas.
  15. Conclusion
  16. ...and 21 more sections

Figures (3)

  • Figure 1: Percentage of prefix members that prove a POI theorem for sequences of proof terms obtained by lemma synthesis as specified in Table , ordered by different criteria.
  • Figure 2: Percentage of prefix members that prove a POI theorem for sequences of proof terms obtained by lemma synthesis as specified in Table , ordered by different criteria.
  • Figure 3: Increase of POI problems solved by Vampire in 3,600 s, 600 s and 60 s through supplying the lemma set from $\mathit{S}_3$.