Generating Theorems by Generating Proof Structures
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912909720813568 |
|---|---|
| author | Wernhard, Christoph |
| author_facet | Wernhard, Christoph |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_15511 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Generating Theorems by Generating Proof Structures Wernhard, Christoph Logic in Computer Science 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. |
| title | Generating Theorems by Generating Proof Structures |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.15511 |