Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908403435044864 |
|---|---|
| author | Wernhard, Christoph Zombori, Zsolt |
| author_facet | Wernhard, Christoph Zombori, Zsolt |
| contents | Viewing formal mathematical proofs as logical terms provides a powerful and elegant basis for analyzing how human experts tend to structure proofs and how proofs can be structured by automated methods. We pursue this approach by (1) combining proof structuring and grammar-based tree compression, where we show how they are inherently related, and (2) exploring ways to combine human and automated proof structuring. Our source of human-structured proofs is Metamath, which, based on condensed detachment, naturally provides a view of proofs as terms. A knowledge base is then just a grammar that compresses a set of gigantic proof trees. We present a formal account of this view, an implemented practical toolkit as well as experimental results. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_12305 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures Wernhard, Christoph Zombori, Zsolt Logic in Computer Science Viewing formal mathematical proofs as logical terms provides a powerful and elegant basis for analyzing how human experts tend to structure proofs and how proofs can be structured by automated methods. We pursue this approach by (1) combining proof structuring and grammar-based tree compression, where we show how they are inherently related, and (2) exploring ways to combine human and automated proof structuring. Our source of human-structured proofs is Metamath, which, based on condensed detachment, naturally provides a view of proofs as terms. A knowledge base is then just a grammar that compresses a set of gigantic proof trees. We present a formal account of this view, an implemented practical toolkit as well as experimental results. |
| title | Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.12305 |