Generating Theorems by Generating Proof Structures

TL;DR

This paper introduces a method for generating theorems from axioms by constructing proof structures, utilizing proof terms, proof structure enumeration, and lemma synthesis to enhance automated theorem generation.

Contribution

It presents a novel approach that combines proof term partitioning, lemma synthesis via DAG compression, and combinator integration for theorem generation without proof goals.

Findings

Successfully generated theorems from a fragment of Metamath.

Demonstrated improvements through lemma synthesis and combinator integration.

Linked proof structure enumeration to automated theorem proving techniques.

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.