REVIEW 1 cited by
Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 1 Pith paper
-
Generating Theorems by Generating Proof Structures
Proof-structure enumeration, combined with lemma synthesis by DAG compression and combinatory proof patterns, generates proofs for 734 of 1,374 Metamath-derived propositional theorems and improves prover success rates.
Discussion (0). Continue with ORCID to comment.