Pith. sign in

REVIEW 2 major objections 5 minor 1 cited by

Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures

T0 review · 2 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper establishes that a formal mathematical knowledge base such as Metamath can be viewed — and used — as a grammar that compresses gigantic proof trees, with each theorem production carrying a computable most general formula.

desk verdict A solid grammar-compression view of Metamath proof terms with a real DV-restriction gap that blocks the 'new verifiable lemmas' claim until the export is checked. read the letter →

arxiv 2505.12305 v2 pith:NRIKYHRD submitted 2025-05-18 cs.LO

Christoph Wernhard , Zsolt Zombori This is my paper · ORCID
classification cs.LO MSC 03B3568T15
keywords prooftermsgrammar-basedtreecompressioncondenseddetachmentMetamathmostgeneraltheoremdependencynetworkpower-lawdegreedistributionlemmadiscovery
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Formal proofs, especially in Metamath, can be written as logical terms built from axiom names and parameters. The paper's central proposal is that a mathematical knowledge base is exactly a grammar that compresses a set of gigantic proof trees: each theorem becomes a production, its name a nonterminal, and its hypotheses the production's parameters. To make this precise, the paper defines the CDDC proof calculus with a notion of most general theorem (MGT), lifts it to grammars via the grammar-MGT, and relates the human-stated theorem formula, the grammar composition, and the fully expanded proof by the chain Fi ≥· shallow-mgtK(pi(Vi)) ≥· grammar-mgtB,G(pi(Vi)) ≥· mgtB(valG(pi(Vi))). If the chain holds, a compressed proof grammar can be verified and queried without expanding enormous original trees, and automated compression of expanded proofs can rediscover or suggest human-style lemmas. The paper backs this with an implementation and experiments on a fragment of set.mm containing 27,233 theorems.

What carries the argument

The load-bearing object is the grammar-MGT. Given a proof grammar G and a presupposition base B, the grammar-MGT of a nonterminal pi(Vi) is obtained by computing the MGT of each production's right-hand side in order, treating earlier productions as new presuppositions; this makes the compressed grammar itself a knowledge base with a computable formula for every production. A second object, the proof dependency network PDNet(G), turns the grammar into a directed graph whose edges show which theorems are used as direct premises and whose in-degree distribution is used for the scale-free analysis.

What would settle it

Run the published toolkit on each of the 27,233 theorems in SetCore and check whether every stated theorem formula is an instance of the shallow-MGT of its production; find one theorem whose proof, after stripping syntactic steps, has an undefined grammar-MGT or yields a formula that does not subsume the stated theorem, for instance a proof whose validity requires a disjoint-variable condition that the grammar-MGT would merge. That single counterexample would refute the paper's definition of a knowledge base as a grammar.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that the structure of a mathematical knowledge base is not an external annotation on top of proofs: it is the same object as a grammar-based compression of proof terms. A proof term is a tree whose inner nodes are the two primitive Metamath inferences, condensed detachment and condensed generalization, and whose leaves are axioms; a grammar production p(V1,...,Vn) -> d compresses a family of such trees, and the MGT of d, the unique most general clause proven by the term, recovers the theorem formula. The grammar-MGT computes this compositionally along the production order, and the key relation Fi ≥· shallow-mgtK(pi(Vi)) ≥· grammar-mgtB,G(pi(Vi)) ≥· mgtB(valG(pi(Vi))) ties the human-stated formula, the shallow composition, the grammar composition, and the fully expanded proof together. Empirically, applying grammar compression to fully expanded proofs of a small selection of theorems produced grammars whose formulas overlap with set.mm's human lemma choices in about a third of cases, and the proof dependency networks of human and machine grammars both show power-law degree distributions with matched scaling factors.

Load-bearing premise

The chain that makes a knowledge base into a grammar relies on the assumption that deleting Metamath's syntactic bookkeeping steps, the parts that only check formula well-formedness, leaves a proof term whose most general theorem still matches the original theorem; if those steps carry structure, or if Metamath's disjoint-variable restrictions are missed by the grammar-MGT, the grammar view is not exact.

Editorial extensions

If this is right

  • A compressed proof grammar can be verified and queried without expanding its gigantic proof trees, because the grammar-MGT yields a checkable formula for each production.
  • Grammar compression of fully expanded proofs can rediscover a substantial fraction of human-chosen lemma statements, as in the reported ~34 percent overlap, so it offers a mechanical way to propose lemmas to a proof library.
  • The save-value of a production gives a quantitative measure of how much reuse a lemma contributes, which could guide which new lemmas are worth adding to a knowledge base.
  • Proof dependency networks of human-structured and machine-compressed proofs have power-law in-degree distributions with correlated scaling factors, indicating that both forms of structuring follow similar reuse patterns.
  • Subsumption-based and same-value reductions can identify redundant theorems in a library, suggesting cleanups that preserve the set of provable statements.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • This view suggests that any proof system admitting a term-like representation of derivations could be reorganized by the same grammar-compression machinery, not only Metamath, if a faithful translation into proof terms exists.
  • The scale-free structure of proof dependency networks implies that a small set of heavily reused lemmas dominates proof search; a premise selector could rank lemmas by grammar in-degree rather than by formula similarity.
  • If the grammar-MGT chain is stable under small additions to the theorem set, incremental grammar compression could serve as a continuous refactoring tool for a growing proof library.
  • The observed 7 percent total size reduction when compressing human-structured grammars suggests that human proof libraries contain systematic, mechanically detectable redundancy that could be trimmed without changing any theorem statement.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper develops a formal framework in which Metamath-style proofs are viewed as terms in a generalized condensed detachment calculus (CDDC) and a mathematical knowledge base is viewed as a grammar that compresses a forest of proof trees. It defines proof grammars, shallow and grammar-based most general theorems (MGTs), and a KB structure, and claims the chain Fi ≥· shallow-mgtK(pi) ≥· grammar-mgtB,G(pi) ≥· mgtB(valG(pi)). It applies this view to a fragment of set.mm, reports structural statistics (sizes, save-values, nonlinearity, variable occurrences), describes a TreeRePair-based compression pipeline with nonlinear and MGT-based reductions, compares human and machine structurings on a subset, and proposes compressed lemmas for eighteen topics of SetCore. The implemented toolkit is publicly available and the experiments are anchored to a fixed set.mm commit.

Significance. If the formal bridge to Metamath can be closed, the paper offers a genuinely useful unifying perspective: named lemmas in a proof assistant can be read as productions of a grammar, and automated tree compression can be used to discover new, potentially reusable lemmas. The formal CDDC machinery is self-contained, the top-level theorem formulas are protected during compression, and the empirical work is grounded in an external, public corpus rather than ad-hoc examples. The paper also gives a refreshingly qualified treatment of its scale-free observation, acknowledging the ongoing debate. The main value is conditional on two gaps: the missing treatment of Metamath's disjoint-variable restrictions in the formal calculus, and the absence of proofs for the central MGT chain.

major comments (2)
  1. [Sect. 2, Table 1; Sect. 7] The formal CDDC calculus does not model Metamath's disjoint-variable restrictions, and this gap is load-bearing for the paper's Metamath claims. In particular, the presupposition G :: ∀(x,y) ← y in Table 1 is presented as the counterpart of ax-gen, but ax-gen in set.mm is valid only when the distinguished variable is disjoint from the wff variable. Without such a side condition, the MGT of G(V1) is ∀(x,u1) ← u1, which admits the invalid first-order instance ∀x P(x) ← P(x). Since the grammar-MGT in Definition 7 and the chain in Definition 8 are computed in this DV-free calculus, those statements are about CDDC rather than about Metamath's actual proof system. Section 7 describes an export procedure that 'infers a suitable syntactic part to be supplemented to a given proof, on the basis of declarations, subject to Metamath's inheritance mechanism of disjoint variable restrictions,' but no correctness proof or metamath.exe verification of the generated lemmas (e.g., lemma905 in Sect. 6) is reported. The authors should either extend CDDC with explicit DV side conditions and prove that the MGTs coincide with the intended Metamath semantics, or verify all exported lemma formulas with the official Metamath verifier and report the results.
  2. [Sect. 2, Prop. 4; Defs. 7–8] The central formal chain is asserted rather than proved. Proposition 4, which governs the behavior of MGTs under substitution for linear and nonlinear proof terms, is stated without proof, and the inequalities Fi ≥· shallow-mgtK(pi(Vi)) ≥· grammar-mgtB,G(pi(Vi)) ≥· mgtB(valG(pi(Vi))) in Definition 8 are simply asserted. The nonlinear case is not a routine consequence: the paper itself notes that grammar-MGTs may be strict instances of expanded MGTs or even undefined. The second inequality (shallow-MGT versus grammar-MGT) is also not immediate, since the two constructions use different presupposition bases. A proof of each inequality, or a precise citation for each, is needed before the KB-as-grammar claim can be regarded as formally established.
minor comments (5)
  1. [App. B, introductory sentence] The sentence 'Lemmas that are subsumed by existing theorems are now shown' appears to be a typo; it should presumably read 'not shown'.
  2. [Table 3, O14] The columns 'Set' and 'MS' are defined only in Observation O14; defining them in the table caption would make the table self-contained.
  3. [Sect. 5, O15–O16] The claims of power-law behavior and 'strongly correlated' scaling factors would be much stronger if the paper reported the fitted exponent values, the chosen fitting range, goodness-of-fit measures, the correlation coefficient, and the number of PDNet pairs used; without these, the correlation statement is not quantitatively supported.
  4. [Table 4] The row for Elementary Geometry silently lacks compression results; the reader has to find in the text that the computation did not terminate in seven days. A footnote in the table would be clearer.
  5. [Fig. 1] The axes are said to be logarithmic but are not labeled, and it is unclear whether the fitted tail range is chosen identically for all three panels; stating this explicitly would improve the reproducibility of the visual fit.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the grammar-compression framework is defined self-containedly and checked against the external set.mm corpus.

full rationale

The paper's formal development is self-contained. Definition 2 fixes the MGT from a presupposition base; Definition 7 defines the grammar-MGT inductively over the acyclic production sequence; Definition 8 then adds the KB constraint F_i ≥ shallow-mgt_K(p_i(V_i)). The displayed chain F_i ≥· shallow-mgt_K(p_i(V_i)) ≥· grammar-mgt_B,G(p_i(V_i)) ≥· mgt_B(val_G(p_i(V_i))) is not an assumption smuggled in as a conclusion: it is a subsumption statement that follows from the KB constraint together with Proposition 4 and the monotonicity of MGT with respect to strengthening the presupposition base. Nothing in this chain is defined in terms of the quantity it is said to predict. The only fitted quantity in the paper is the power-law scaling factor of PDNet in-degree distributions, which is an empirical descriptor of the observed graphs, not an input to the grammar-compression claim or to the lemma-generation pipeline. The author self-citations (e.g., [44], [46]) are used for implementation lineage, background on condensed detachment, and side remarks about resolution simulation; none of them carries the central argument. The omission of Metamath's disjoint-variable restrictions in the CDDC bridge is a fidelity or export-correctness concern, not a circularity, since the paper does not define the target result in terms of that bridge. Because the central derivation is independent of any fitted value or self-citational chain, the correct circularity score is 0.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The central framework rests on standard unification and the assumption that CDDC adequately represents Metamath. The only fitted quantity is the power-law exponent used for the network observation. The paper's tool and the set.mm corpus are external benchmarks, so the ledger is light.

free parameters (2)
  • Power-law scaling factor alpha of PDNet in-degree distributions = Fit via MLE; individual values shown in Fig. 2, not reported in text
    The paper fits alpha to each proof dependency network's in-degree tail to support the scale-free observation (Sect. 5, O15-O16). This is an empirical fit, not a parameter of the compression framework.
  • Tractability cutoffs (1 minute for MiniSet, 100 seconds for PDNet pairs) = Hand-selected cutoffs
    These thresholds determine the experimental subsets (17 theorems; 3,287 human/machine pairs) and therefore bound the generality of the reported compression ratios and correlations (Sect. 5).
assumptions (3)
  • standard math Standard unification and substitution properties, including most general unifiers, are available.
    Used throughout the CDDC rules and MGT definitions (Sect. 2).
  • domain assumption Metamath proofs can be represented in CDDC as definite clauses with presuppositions, with the two primitive rules corresponding to ax-mp and ax-gen.
    This is the paper's central modeling assumption, introduced in the Introduction and Sect. 2; it is not proved by a bijection.
  • domain assumption The tail of the PDNet in-degree distribution follows a power law, following Clauset et al.
    Used for observations O15-O16; the paper fits to the tail and does not test alternative distributions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures." pith.science (2026). https://pith.science/paper/NRIKYHRD

@misc{pith2026250512305,
  author       = {Pith},
  title        = {Pith review of: Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NRIKYHRD}},
  note         = {Machine review of arXiv:2505.12305}
}
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.

Figures

Figures reproduced from arXiv: 2505.12305 by the authors.

Figure 1
Figure 1. Complementary cumulative distribution of the empirical in-degree, along with that of the fitted scale-free graph. Both axes are of logarithmic scale. The fitted curves are shifted to align with the tail of the distribution. Left: SetCore Center: MiniSet Right: MiniTrp [PITH_FULL_IMAGE:figures/full_fig_p012_1.png] view at source ↗
Figure 2
Figure 2. PDNets of proof grammars as found in Metamath (Human) and of those gener￾ated via automated compression from the fully expanded proof tree (Machine): Left: Histogram of power law distribution scaling factors, fitted to each PDNet separately. Right: Scatter plot showing the correlation among scaling factors of both PDNets. differences depending on whether they were created by humans or by machine. Recall that in a PD… view at source ↗
Figure 3
Figure 3. supports observation O15 in Sect. 5 with additional visualizations of the in-degree distribution of PDNets. Here they are considered for grammars obtained for single theorems of set.mm. They contain the theorem’s proof rep￾resented as a production, supplemented by productions representing the proofs of the theorems that are directly or indirectly referenced in it [PITH_FULL_IMAGE:figures/full_fig_p019_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Generating Theorems by Generating Proof Structures

    cs.LO 2026-02 conditional novelty 6.0 of 10

    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.

Reference graph

Works this paper leans on

50 extracted references · 37 canonical work pages · cited by 1 Pith paper

  1. [1]

    Reviews of Modern Physics 74(1), 47–97 (Jan 2002)

    Albert, R., Barabási, A.L.: Statistical mechanics of complex networks. Reviews of Modern Physics 74(1), 47–97 (Jan 2002). https://doi.org/10.1103/RevModPhys. 74.47

    doi:10.1103/revmodphys 2002

  2. [2]

    https://doi.org/10.1093/jigpal/jzac082

    Benzmüller, C., Fuenmayor, D., Steen, A., Sutcliffe, G.: Who finds the short proof? Logic Journal of the IGPL (2023). https://doi.org/10.1093/jigpal/jzac082

    work page doi:10.1093/jigpal/jzac082 2023

  3. [3]

    Vieweg (1987), first edition 1982

    Bibel, W.: Automated Theorem Proving. Vieweg (1987), first edition 1982

    work page 1987

  4. [4]

    In: Kahle, R., Rathjen, M

    Bibel, W., Otten, J.: From Schütte’s formal systems to modern automated deduc- tion. In: Kahle, R., Rathjen, M. (eds.) The Legacy of Kurt Schütte, chap. 13, pp. 215–249. Springer (2020). https://doi.org/10.1007/978-3-030-49424-7_13

    doi:10.1007/978-3-030-49424-7_13 2020

  5. [5]

    Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016). https://doi.org/10.6092/ISSN. 1972-5787/4593

    doi:10.6092/issn 2016

  6. [6]

    Boolos, G.: A curious inference. J. Philos. Logic16, 1–12 (1987). https://doi.org/ 10.1007/BF00250612

    work page doi:10.1007/bf00250612 1987

  7. [7]

    Nature Communications 10(1), 1017(Mar2019).https://doi.org/10.1038/s41467-019-08746-5,https://doi

    Broido, A.D., Clauset, A.: Scale-free networks are rare. Nature Communications 10(1), 1017(Mar2019).https://doi.org/10.1038/s41467-019-08746-5,https://doi. org/10.1038/s41467-019-08746-5

    doi:10.1038/s41467-019-08746-5

  8. [8]

    Conversion of HOL Light proofs into Metamath

    Carneiro, M.: Conversion of HOL Light proofs into Metamath. CoRR abs/1412.8091 (2014), https://arxiv.org/abs/1412.8091

    work page Pith review arXiv 2014

Show all 50 references
  1. [9]

    In: Benzmüller, C., Miller, B

    Carneiro, M.: Metamath zero: Designing a theorem prover prover. In: Benzmüller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 71–88. Springer (2020)

    2020

  2. [10]

    In: Naumowicz, A., Thiemann, R

    Carneiro, M., Brown, C.E., Urban, J.: Automated theorem proving for Meta- math. In: Naumowicz, A., Thiemann, R. (eds.) ITP 2023. LIPIcs, vol. 268, pp. 9:1–9:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023). https: //doi.org/10.4230/LIPIcs.ITP.2023.9

    2023 doi

  3. [11]

    SIAM Review51(4), 661–703 (2009)

    Clauset, A., Shalizi, C.R., Newman, M.E.J.: Power-law distributions in empirical data. SIAM Review51(4), 661–703 (2009). https://doi.org/10.1137/070710111

    2009 doi

  4. [12]

    Curry, H., Feys, R.: Combinatory Logic, vol. I. North-Holland (1958)

    1958

  5. [13]

    In: Bonacina, M.P., Furbach, U

    Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the Mizar mathematical library. In: Bonacina, M.P., Furbach, U. (eds.) FTP’97. pp. 58–62. RISC-Linz Report Series No. 97–50, Joh. Kepler Univ., Linz (1997), https://www.logic.at/ftp97/papers/dahn.pdf

    1997

  6. [14]

    Seki-Report SR-94-05, Universität Kaiserslautern (1994), http://wwwlehre.dhbw-stuttgart.de/~sschulz/ PAPERS/DS94-SR-94-05.ps.gz, revised September 1997

    Denzinger, J., Schulz, S.: Analysis and Representation of Equational Proofs Gen- erated by a Distributed Completion Based Proof System. Seki-Report SR-94-05, Universität Kaiserslautern (1994), http://wwwlehre.dhbw-stuttgart.de/~sschulz/ PAPERS/DS94-SR-94-05.ps.gz, revised Sept...

    1994

  7. [15]

    Eder, E.: Properties of substitutions and unification. J. Symb. Comput.1(1), 31–46 (1985). https://doi.org/10.1016/S0747-7171(85)80027-4

    1985 doi

  8. [16]

    In: Dediu, A.H., Martín-Vide, C

    Hetzl, S.: Applying tree languages in proof theory. In: Dediu, A.H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 301–312 (2012). https://doi.org/10. 1007/978-3-642-28332-1_26

    2012

  9. [17]

    Journal of Symbolic Logic55(1), 90–105 (1990)

    Hindley, J.R., Meredith, D.: Principal type-schemes and condensed detachment. Journal of Symbolic Logic55(1), 90–105 (1990). https://doi.org/10.2307/2274956

    1990 doi

  10. [18]

    Kaliszyk,C.,Urban,J.:Learning-assistedtheoremprovingwithmillionsoflemmas. J. Symb. Comput.69, 109–128 (2015). https://doi.org/10.1016/J.JSC.2014.09.032

    2015 doi

  11. [19]

    Larsson, N.J., Moffat, A.: Off-line dictionary-based compression. Proc. IEEE 88(11), 1722–1732 (2000). https://doi.org/10.1109/5.892708

    2000 doi

  12. [20]

    In: Potapov, I

    Lohrey, M.: Grammar-based tree compression. In: Potapov, I. (ed.) DLT

  13. [21]

    Lohrey, M., Maneth, S., Mennicke, R.: XML tree structure compression using Re- Pair. Inf. Syst.38(8), 1150–1167 (2013). https://doi.org/10.1016/j.is.2013.06.006, system available from https://github.com/dc0d32/TreeRePair, accessed Jun 30, 2022

    2013 doi

  14. [22]

    JACM15(2), 236–251 (1968)

    Loveland, D.W.: Mechanical theorem proving by model elimination. JACM15(2), 236–251 (1968)

    1968

  15. [23]

    North Holland (1970), edited by L

    Łukasiewicz, J.: Selected Works. North Holland (1970), edited by L. Borkowski

    1970

  16. [24]

    Comptes rendus des séances de la Soc

    Łukasiewicz, J., Tarski, A.: Untersuchungen über den Aussagenkalkül. Comptes rendus des séances de la Soc. d. Sciences et d. Lettres de Varsovie 23 (1930), English translation in [23], pp. 131–152

    1930

  17. [25]

    McCune, W.: Prover9 and Mace4 (2005–2010), http://www.cs.unm.edu/~mccune/ prover9

    2005

  18. [26]

    In: Kapur, D

    McCune, W., Wos, L.: Experiments in automated deduction with condensed de- tachment. In: Kapur, D. (ed.) CADE-11. LNCS (LNAI), vol. 607, pp. 209–223. Springer (1992). https://doi.org/10.1007/3-540-55602-8_167

    1992 doi

  19. [27]

    lulu.com, second edn

    Megill, N., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs. lulu.com, second edn. (2019), online https://us.metamath.org/downloads/ metamath.pdf

    2019

  20. [28]

    Megill, N.D.: Home Page – Metamath, online: https://us.metamath.org/, accessed Jan 10, 2025

    2025

  21. [29]

    Megill, N.D.: Proof Explorer – Home Page – Metamath: A Theorem Sampler, online: https://us.metamath.org/mpeuni/mmset.html#theorems, accessed Jan 10, 2025

    2025

  22. [30]

    Megill, N.D.: A finitely axiomatized formalization of predicate calculus with equal- ity.NotreDameJ.ofFormalLogic 36(3),435–453(1995).https://doi.org/10.1305/ ndjfl/1040149359

    1995

  23. [31]

    Oxford Univ

    Newman, M.: Networks. Oxford Univ. Press, second edn. (2018)

    2018

  24. [32]

    Theoria26, 102–139 (1960)

    Prawitz, D.: An improved proof procedure. Theoria26, 102–139 (1960)

    1960

  25. [33]

    Machine In- telligence 4, 59–71 (1969), reprinted with author preface in J

    Prawitz, D.: Advances and problems in mechanical proof procedures. Machine In- telligence 4, 59–71 (1969), reprinted with author preface in J. Siekmann, G. Wright (eds.): Automation of Reasoning, vol 2: Classical Papers on Computational Logic 1967–1970, Springer, 1983, pp. 283–297

    1969

  26. [34]

    Australasian Journal of Philosophy 34(3), 182–192 (1956)

    Prior, A.N.: Logicians at play; or Syll, Simp and Hilbert. Australasian Journal of Philosophy 34(3), 182–192 (1956). https://doi.org/10.1080/00048405685200181

    1956 doi

  27. [35]

    Clarendon Press, Oxford, 2nd edn

    Prior, A.N.: Formal Logic. Clarendon Press, Oxford, 2nd edn. (1962). https://doi. org/10.1093/acprof:oso/9780198241560.001.0001

    1962

  28. [36]

    In: Ramanayake, R., Urban, J

    Rawson, M., Wernhard, C., Zombori, Z., Bibel, W.: Lemmas: Generation, selection, application. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNAI, vol. 14278, pp. 153–174 (2023). https://doi.org/10.1007/978-3-031-43513-3_9

    2023 doi

  29. [37]

    Projektarbeit in informatik, Fachbereich Informatik, Universität Kaiserslautern (1993), http: //wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Sch93-project.ps.gz, (German Language)

    Schulz, S.: Analyse und Transformation von Gleichheitsbeweisen. Projektarbeit in informatik, Fachbereich Informatik, Universität Kaiserslautern (1993), http: //wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Sch93-project.ps.gz, (German Language)

    1993

  30. [38]

    Schönfinkel, M.: Über die Bausteine der mathematischen Logik. Math. Ann.92(3– 4), 305–316 (1924). https://doi.org/10.1007/BF01448013

    1924 doi

  31. [39]

    Stickel, M.E.: A Prolog technology theorem prover: implementation by an extended Prolog compiler. J. Autom. Reasoning4(4), 353–380 (1988). https://doi.org/10. 1007/BF00297245

    1988

  32. [40]

    Ulrich, D.: A legacy recalled and a tradition continued. J. Autom. Reasoning27(2), 97–122 (2001). https://doi.org/10.1023/A:1010683508225 18 C. Wernhard, and Z. Zombori

    2001 doi

  33. [41]

    Vyskocil, J., Stanovský, D., Urban, J.: Automated proof compression by invention ofnewdefinitions.In:Clarke,E.M.,Voronkov,A.(eds.)LPAR-16.LNCS,vol.6355, pp. 447–462. Springer (2010). https://doi.org/10.1007/978-3-642-17511-4_25

    2010 doi

  34. [42]

    In: Fontaine, P., Schulz, S., Urban, J

    Wernhard, C.: The PIE system for proving, interpolating and eliminating. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proc., vol. 1635, pp. 125–138. CEUR-WS.org (2016), http://ceur-ws.org/Vol-1635/ paper-11.pdf

    2016

  35. [43]

    In: Hofstedt, P., et al

    Wernhard, C.: Facets of the PIE environment for proving, interpolating and elim- inating on the basis of first-order logic. In: Hofstedt, P., et al. (eds.) DECLARE

  36. [44]

    In: Konev, B., Schon, C., Steen, A

    Wernhard, C.: Generating compressed combinatory proof structures — an ap- proach to automated first-order theorem proving. In: Konev, B., Schon, C., Steen, A. (eds.) PAAR 2022. CEUR Workshop Proc., vol. 3201. CEUR-WS.org (2022), https://arxiv.org/abs/2209.12592

    2022 arXiv

  37. [45]

    In: Otten, J., Bibel, W

    Wernhard, C.: Structure-generating first-order theorem proving. In: Otten, J., Bibel, W. (eds.) AReCCa 2023. CEUR Workshop Proc., vol. 3613, pp. 64–83. CEUR-WS.org (2024), https://ceur-ws.org/Vol-3613/AReCCa2023_paper5.pdf

    2024

  38. [46]

    In: Platzer, A., Sutcliffe, G

    Wernhard, C., Bibel, W.: Learning from Łukasiewicz and Meredith: Investi- gations into proof structures. In: Platzer, A., Sutcliffe, G. (eds.) CADE 28. LNCS (LNAI), vol. 12699, pp. 58–75. Springer (2021). https://doi.org/10.1007/ 978-3-030-79876-5_4

    2021

  39. [47]

    Wernhard, C., Bibel, W.: Investigations into proof structures. J. Autom. Reasoning 68(24) (2024). https://doi.org/10.1007/s10817-024-09711-8

    2024 doi

  40. [48]

    bottom-up

    Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory and Practice of Logic Programming 12(1-2), 67–96 (2012). https://doi.org/10.1017/ S1471068411000494 Mathematical Knowledge Bases as Grammar-Compressed Proof Terms 19 A Additional Plots of Degree Distribu...

    2012

  41. [2015]

    9168, pp

    LNCS, vol. 9168, pp. 46–57. Springer (2015). https://doi.org/10.1007/ 978-3-319-21500-6_3 Mathematical Knowledge Bases as Grammar-Compressed Proof Terms 17

    2015

  42. [2019]

    12057, pp

    LNCS (LNAI), vol. 12057, pp. 160–177 (2020). https://doi.org/10.1007/ 978-3-030-46714-2_11

    2020

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.