Pith. sign in

REVIEW 3 major objections 4 minor 52 references

Generating Theorems by Generating Proof Structures

T0 review · 3 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read By enumerating proof structures and mining compressed proof DAGs, a machine can generate useful theorems from axioms alone — shown on 1,374 benchmark theorems, with 734 proofs found and one prover's success rate rising from 74% to 94%.

desk verdict A solid, honest subfield contribution that introduces a useful benchmark and two working lemma-generation ideas; the headline numbers are real but best-case, chosen from a larger run set, so treat the transfer claims with caution. read the letter →

arxiv 2602.15511 v1 pith:Q46RQG7T submitted 2026-02-17 cs.LO

Christoph Wernhard This is my paper · ORCID
classification cs.LO MSC 03B3568T15
keywords theoremgenerationlemmasynthesisprooftermscondenseddetachmentDAGcompressioncombinatorylogicfirst-orderprovingstructureenumeration
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

The paper tries to show that a machine can generate useful mathematical theorems, together with proofs, from a fixed set of axioms and no target theorem. Its approach enumerates proof terms by increasing structural complexity, using condensed detachment (modus ponens with unification), and keeps only those whose most general theorem is defined. A large collection of such proofs is then compressed into a minimal DAG, and the subproofs that save the most space are promoted to candidate lemmas; feeding those lemmas back as additional axioms substantially boosts existing first-order provers. On a benchmark of 1,374 theorems extracted from a well-known formal library, the combined method generates proofs for 734 theorems, including 12 rated hardest by the provers it compared against, and raises the best prover's success rate from 74% to 94% and another's from 7% to 44%. A careful reader should care because this is a concrete, largely parameter-free demonstration that useful lemmas can be discovered from proof structure alone, without human-chosen premises or goal-driven search.

What carries the argument

The central object is the proof term, a tree built by condensed detachment — essentially modus ponens with unification — whose 'most general theorem' (MGT) is the most general formula the proof proves, unique up to variable renaming. The paper partitions all proof terms into inductive level characterizations (by tree size, height, or compacted DAG size) that allow bottom-up, cached enumeration with restrictions such as subsumption. For lemma synthesis it compresses a large set of generated proof terms into its minimal DAG grammar and computes the 'save-value' of each production — the amount of grammar size that production saves across the whole set; productions with high save-value are promo

What would settle it

Run the same lemma-synthesis pipeline on a fresh, equally large formal development — for example, a different axiom system or a separate branch of a proof library that was not used to calibrate the method — and check whether the lemmas it synthesizes still raise prover success rates. Concretely: compute the save-value ranking on a held-out set of proofs, take the top-k lemmas, and compare the precision of that ranking against rankings by formula size or by random selection; if the compressed-DAG lemmas do not outperform the baselines on the held-out set, the compression-value hypothesis is fal

Watch

Extended reading notes

Core claim

The central claim is that theorems can be invented from axioms alone by enumerating proof terms in order of increasing structural complexity — using condensed detachment — and then treating the most 'compressing' subproofs of a large generated proof set as candidate lemmas. The paper demonstrates this on a benchmark of 1,374 propositional-logic theorems drawn from a well-known formal library, generating full proofs for 734 of them, including twelve that three mature first-order provers could not solve within an hour. Adding the synthesized lemmas back as axioms raised the strongest prover's success rate on the benchmark from 74% to 94% and a top-down prover's from 7% to 44%. The paper furthe

Load-bearing premise

The method rests on the hypothesis that a formula is a genuinely useful lemma exactly when it appears as a shared subproof that significantly compresses a large set of generated proofs; this correlation is inferred from experiments on the same benchmark rather than independently proved or tested on out-of-sample axiom systems.

Editorial extensions

If this is right

  • Synthesized lemmas can be appended as axioms to existing first-order provers, raising their success rates on the benchmark from 74% to 94% for the strongest prover and from 7% to 44% for a top-down prover.
  • The method generates full proofs for 734 of the 1,374 benchmark theorems, including 12 that mature provers could not solve within an hour, demonstrating that proof-structure enumeration can discover hard theorems.
  • The generated proofs are often far more compact in DAG size than the original human-written proofs, suggesting the enumeration can surface structurally simpler derivations from the same axioms.
  • The level-based enumeration gives a uniform, configurable framework in which different complexity measures and heuristic restrictions can be plugged in, and which links theorem generation to formulas-as-types and to grammar-based compression.

Reading between the lines

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

  • Because the save-value criterion is entirely structural, it may serve as a general proxy for 'mathematical centrality' in any proof corpus, not just this propositional benchmark; testing it on a different large library or on interactive proof assistants would show whether the correlation transfers.
  • The pipeline could be used as a data-augmentation source for learning-based premise selection: generate a large pool of candidate lemmas from axioms alone, then let a learned model filter them by predicted usefulness, rather than relying on human-curated lemma sets.
  • If the same enumeration scales to predicate logic, it would enable machines to propose lemmas in real mathematical domains without human-selected premises, effectively automating part of the invention step in formal mathematics; the paper notes the obvious next target is predicate logic.
  • The compression-value criterion resembles a minimum-description-length principle for proof libraries; one could test whether lemmas that maximize DAG compression coincide with lemmas humans choose to state and reuse across a broader mathematical corpus.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. Starting from condensed detachment over the three classical propositional-logic axioms of set.mm, the paper defines inductive level characterizations of proof terms (tree size, height, PSP) and uses a configurable prover SGCD to enumerate proof-term levels bottom-up. A benchmark POI of 1,374 theorem formulas is extracted from a fragment of set.mm. A baseline enumeration proves 554 theorems. The paper then adds two mechanisms: lemma synthesis by minimal-DAG compression with save-value ordering, and combinator-based proof patterns/schemas. On selected SGCD runs the union of these methods proves 734 POI theorems (12 with rating 1), and the synthesized lemmas substantially raise the number solved by Vampire and leanCoP. The paper supplies extensive run tables, proof listings, and an appendix with per-theorem results.

Significance. The contribution is potentially significant: it gives an explicit proof-structure-based approach to goal-free theorem and lemma generation, with a concrete benchmark, reproducible artifacts, and external first-order prover checks. The described control experiment in Appendix D (save-value vs MGT-size ordering) is a useful step toward isolating the mechanism. If the method transfers beyond the calibration corpus, the paper would be a solid advance in automated lemma synthesis. The main reservation is that the headline numbers are produced by configuration selection on the same benchmark used for evaluation; this limits, for now, the strength of the general claim.

major comments (3)
  1. [§6, Table 8; §7, Tables 10–11] The paper's central empirical claim—that the method generates 734/1374 POI theorems and improves Vampire/leanCoP from 74% to 94% and from 7% to 44%—is an upper envelope over configurations. Section 6 states that 'runs were chosen from a larger test set such that taken together they provide proofs for a large number of POI theorems not in POI-base,' and Section 7 repeats: 'Again, runs were chosen from a larger test set...'. The same selection is also used for the lemma-enhanced prover experiments in Table 9. No size of the larger test set or selection protocol is given, and no held-out subset or separate axiom system is used. As a result, the 734 count and the prover boosts are best-case results, not expected performance of a fixed algorithm. I ask for either (a) an out-of-sample evaluation with a fixed default configuration and no selection after seeing results, or (b) an explicit, quant
  2. [§7, App. G] The combinator inventory is extracted from λ-to-SKI translations of the same set.mm fragment used to form POI, and the candidate combinator sets are selected by frequency in those same proofs. This creates a tuning loop: the proof schemas are chosen because they occur in the corpus, and their success is then measured on theorems from the same corpus. The claim that combinator proof patterns are generally useful therefore lacks an independent test. A concrete fix is to test with combinators chosen from a disjoint corpus or from a principled basis (e.g., all combinators up to a bounded arity/size), and to report sensitivity of Tables 10 and 11 to the combinator inventory.
  3. [§6, 'Computing the Lemmas'] The value hypothesis behind the whole lemma-synthesis workflow—that save-value in a proof DAG measures mathematical usefulness—is an unproven heuristic. Appendix D is a valuable internal control, but it is still on the same POI benchmark and inherits the run-selection issue of Table 8; it shows that save-value beats MGT-size ordering within this corpus, not that the correlation holds more generally. To make the synthesis workflow robust, add a comparison against simple baselines (e.g., random lemmas or lemmas sorted by formula size) with fixed run selection, or an evaluation on a different axiom system. Otherwise the improved prover results may not transfer.
minor comments (4)
  1. [§8] The sentence 'Its seems useful for a systematic understanding...' contains a typo: 'Its' should be 'It'.
  2. [Table 11] The Schemas column uses notation such as 'dB,B4,C4,S' and 'dC4(C4(C4(C4C)))/1' that is not explained in the table or its caption; the 'd' prefix for direct proof schemas is defined only in the text. Please make the table self-contained or add a pointer.
  3. [§6] The phrase 'Drastic boost-ups' is informal; consider 'large increases' or substituting a quantitative statement of the improvement.
  4. [Fig. 1 and App. E] Figures 1 and E show nearly identical precision plots. One of them could be omitted or reduced to a single representative sequence to save space.

Circularity Check

2 steps flagged · score 4.0 of 10

POI coverage totals and prover boosts are partly in-sample: run configurations and lemma sets were selected on the benchmark, and some solved problems are subsumed by input lemmas; the core proof-term derivation is not circular.

  1. fitted input called prediction [Section 6, 'Lemma-Enhanced Theorem Generation with SGCD' (and Section 7, 'Theorem Generation with SGCD and Proof Schemas')]
    "The runs of Table 8 were chosen from a larger test set such that taken together they provide proofs for a large number of POI theorems not in POI-base. ... Again, runs were chosen from a larger test set such that taken together they prove a large number of POI theorems not in POI-base."

    The headline totals '697' and later '734' are unions over runs whose level characterizations, lemma-prefix lengths, trim values, and combinator sets were selected after inspecting POI results. The quoted sentences explicitly say the runs were chosen to maximize POI coverage. Thus the final count is the value of the target objective on a selected configuration set, not the output of one fixed, pre-specified pipeline. Reporting it as the method's yield is in-sample tuning presented as a result, not a prediction.

  2. fitted input called prediction [Section 6, Table 8 legend and Table 9 setup]
    "Column Inp shows the number of POI theorems which are subsumed by an input lemma. ... The S i columns refer to settings from Table 8: The axioms were enriched by the MGTs of the first NLem proof terms from DLem."

    When a supplied lemma is the MGT of a POI theorem itself (or subsumes it), a first-order prover succeeds by input subsumption rather than by proof search. For example, S3 has Inp=62 while Vampire's S3 total is 1,290 versus 1,023 at base, and S12 has Inp=254. The paper does not report gains net of these subsumed-by-input cases, so part of the 'drastic boost-up' claim for Vampire and leanCoP is forced by construction: the target formula is included among the axioms.

full rationale

Most of the derivation content is not circular. Proof terms are generated from the three axioms via explicit inductive level definitions (Defs. 1, 2, 3, 4), and the claimed POI theorems are accompanied by concrete DAG proof terms whose MGTs are mechanically defined; the POI benchmark is converted from an external corpus, set.mm, and is not just a renaming of the method's output. The self-citations ([42,44,45,46]) supply background constructions, but the paper restates the needed definitions, so there is no load-bearing self-citation chain. The genuinely circular part is the evaluation layer. The paper states that the SGCD runs in Tables 8, 10, and 11 were chosen from larger test sets to maximize POI coverage, so the '734 theorems' and the reported prover improvements are selected maxima, not fixed-pipeline predictions. Additionally, Table 9's prover counts include POI theorems that are subsumed by the supplied lemmas (the Inp column), making some solved problems succeed by construction. This weakens the transferability of the headline improvements, but the generated proof artifacts remain valid and the core enumeration/compression derivation is not circular. Score 4 reflects partial in-sample evaluation circularity rather than a definitional derivation collapse.

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

The central results depend on a configured enumeration engine (level characterization, trim/gen_max, lemma prefixes, combinator choices). The counts of solved theorems are therefore not free of benchmark-specific tuning; the external prover comparisons provide the main independent check.

free parameters (3)
  • SGCD configuration vector ⟨L, Rest, Ord, Trim, Post, MaxLevel⟩ = e.g., BP: ⟨P, dup, f_th, 200k, subs, 64e⟩; BT: ⟨T, dup, f_ht, 20k, subs, 592e⟩; vary in Tables 4-5, 8, 10-11
    The reported 554/734 theorem counts depend on hand-set per-run values for Trim, gen_max, lt_ft, and level characterization; changing these changes the results.
  • Lemma sequences DLem and prefix lengths NLem = LMS 500, LMM 100, LML 4k, LMT 200, A100P 800-12k, etc. (Tables 7-8)
    The enhanced theorem generation is evaluated for specific lemma sets and prefix lengths selected from experiments; the method does not automatically calibrate these.
  • Combinator sets for proof patterns/schemas = Sets such as {I/2, B4, C, C4, S4}, {B, C, S, S4}, {dB,B4,C4,S}, etc. (Tables 10-11); combinator frequencies from Table 1
    Combinators were chosen by analyzing which combinators occur in set.mm proofs (App. G), then tested on POI theorems from the same database.
assumptions (5)
  • domain assumption Condensed detachment (Det) and axioms 1,2,3 constitute a sound and complete proof system for classical propositional logic.
    Background used throughout; from Section 2/Table 1. Standard, but it grounds the benchmark's relevance.
  • domain assumption Metamath theorem statements can be converted from definite clauses to implication form with linear proof translation.
    Section 3 relies on this to define POI; the proof sketch in App. A uses λ-to-SKI compilation and replacement of K/S by axioms 1/2, but no machine-checked certificate is given.
  • standard math A proof term has at most one most general theorem (MGT) up to renaming.
    Used implicitly in Sections 2 and 4 to define MGT and level cutoffs; follows from unification, not proved in the paper.
  • ad hoc to paper DAG-compression save-value is a meaningful heuristic for lemma usefulness.
    Sect. 6 states this as a hypothesis; supported by the ablation in App. D but not proven.
  • ad hoc to paper The combinator inventory extracted from λ-to-SKI translations of set.mm proofs transfers to useful proof schemas for the same axiom system.
    App. G uses this to choose candidate combinators; it is experimental and has no independent justification.
invented entities (2)
  • Proof pattern p/k with associated combinator c
    purpose: Compress proof-term enumeration by treating combinator applications as parameterized patterns (Def. 3/4).
    No theoretical guarantee outside the paper; utility is shown by SGCD runs C1-C15 in Table 10.
  • Direct proof schema c/k
    purpose: Alternate way to incorporate combinators as explicit D-schemas (Def. 4); used in runs C16-C22.
    Results in Table 11; no external evidence beyond the reported experiments.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Generating Theorems by Generating Proof Structures." pith.science (2026). https://pith.science/paper/Q46RQG7T

@misc{pith2026260215511,
  author       = {Pith},
  title        = {Pith review of: Generating Theorems by Generating Proof Structures},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Q46RQG7T}},
  note         = {Machine review of arXiv:2602.15511}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2602.15511 by the authors.

Figure 1
Figure 1. Percentage of prefix members that prove a POI theorem for sequences of proof terms obtained by lemma synthesis as specified in [PITH_FULL_IMAGE:figures/full_fig_p012_1.png] view at source ↗
Figure 2
Figure 2. below extends [PITH_FULL_IMAGE:figures/full_fig_p024_2.png] view at source ↗
Figure 3
Figure 3. below supplements [PITH_FULL_IMAGE:figures/full_fig_p025_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 18 canonical work pages

  1. [1]

    Addison-Wesley (1986)

    Aho, A.V., Sethi, R., Ullman, J.D.: Compilers – Principles, Techniques, and Tools. Addison-Wesley (1986)

    1986

  2. [2]

    CoRR abs/2504.04942(2025).https://doi.org/10.48550/ARXIV.2504.04942

    Alhessi, Y., Einarsdóttir, S.H., Granberry, G., First, E., Johansson, M., Lerner, S., Smallbone, N.: Lemmanaid: Neuro-symbolic lemma conjecturing. CoRR abs/2504.04942(2025).https://doi.org/10.48550/ARXIV.2504.04942

    arXiv doi:10.48550/arxiv.2504.04942 2025

  3. [3]

    In: Douglas, M.R., Hales, T.C., Kaliszyk, C., Schulz, S., Urban, J

    Axelrod, G., Dubhashi, D., Johansson, M., Silvi, A., Smallbone, N., , Stucki, S.: Learning to generate abstractions for an equational solver. In: Douglas, M.R., Hales, T.C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) AITP 2025 (Informal Book of Abstracts) (2025), online:https://aitp-conference.org/2025/abstract/AITP_ 2025_paper_18.pdf, accessed Feb 03, 2026

    2025

  4. [4]

    Vieweg (1987), first edition 1982

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

    1987

  5. [5]

    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

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

  6. [6]

    In: Capretta, V., Krebbers, R., Wiedijk, F

    Blaauwbroek, L., Cerna, D.M., Gauthier, T., Jakubuv, J., Kaliszyk, C., Suda, M., Urban, J.: Learning guided automated reasoning: A brief survey. In: Capretta, V., Krebbers, R., Wiedijk, F. (eds.) Logics and Type Systems in Theory and Prac- tice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birth- day. LNCS, vol. 14560, pp. 54–83. Spring...

    2024

  7. [7]

    In: Naumowicz, A., Thiemann, R

    Carneiro, M., Brown, C.E., Urban, J.: Automated theorem proving for Metamath. 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

  8. [8]

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

    1958

Show all 52 references
  1. [9]

    Seki-Report SR-94-05, Uni- versitä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 Gener- ated by a Distributed Completion Based Proof System. Seki-Report SR-94-05, Uni- versität Kaiserslautern (1994),http://wwwlehre.dhbw-stuttgart.de/~sschulz/ PAPERS/DS94-SR-94-05.ps.gz, revised Sep...

    1994

  2. [10]

    Vieweg, Braunschweig (1992).https://doi.org/10.1007/978-3-322-84222-0

    Eder, E.: Relative Complexities of First Order Calculi. Vieweg, Braunschweig (1992).https://doi.org/10.1007/978-3-322-84222-0

    1992 doi

  3. [11]

    In: Börger, E., Kleine Büning, H., Richter, M.M

    Eder, E.: A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL ’88. LNCS, vol. 385, pp. 80–98. Springer (1989). https://doi.org/10.1007/BFb0026296

    1989 doi

  4. [12]

    Genitrini, A., Gittenberger, B., Kauers, M., Wallner, M.: Asymptotic enumeration of compacted binary trees of bounded right height. J. Comb. Theory, Ser. A172, 105177 (2020).https://doi.org/10.1016/j.jcta.2019.105177 Generating Theorems by Generating Proof Structures 17

    2020

  5. [13]

    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

  6. [14]

    Cambridge University Press (1997)

    Hindley, J.R.: Basic Simple Type Theory. Cambridge University Press (1997). https://doi.org/10.1017/CBO9780511608865

    1997 doi

  7. [15]

    Journal of Symbolic Logic55(1), 90–105 (1990).https://doi.org/10.2307/ 2274956

    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

  8. [16]

    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

  9. [17]

    In: Gallagher, J.P., Sulzmann, M

    Kiselyov, O.:λto SKI, semantically. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS (LNTCS), vol. 10818, pp. 33–50 (2018).https://doi.org/ 10.1007/978-3-319-90686-7_3

    2018 doi

  10. [18]

    In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013

    Kovács, L., Voronkov, A.: First-order theorem proving andV ampire. In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. pp. 1–35. Springer (2013)

    2013

  11. [19]

    Structure, Complexity, Implementa- tion

    Letz, R.: Tableau and Connection Calculi. Structure, Complexity, Implementa- tion. Habilitationsschrift, TU München (1999),https://web.archive.org/web/ 20230604101128/https://www2.tcs.ifi.lmu.de/~letz/habil.ps, accessed Feb 12, 2026

    1999

  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

    2013 doi

  14. [22]

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

    2005

  15. [23]

    lulu.com, second edn

    Megill, N., Wheeler, D.A.: Metamath: A Computer Language for Mathemat- ical Proofs. lulu.com, second edn. (2019), onlinehttps://us.metamath.org/ downloads/metamath.pdf

    2019

  16. [24]

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

    2025

  17. [25]

    Notre Dame J

    Megill, N.D.: A finitely axiomatized formalization of predicate calculus with equal- ity. Notre Dame J. of Formal Logic36(3), 435–453 (1995).https://doi.org/10. 1305/ndjfl/1040149359

    1995

  18. [26]

    OEIS Foundation Inc.: The On-Line Encyclopedia of Integer Sequences (2026), http://oeis.org

    2026

  19. [27]

    Otten,J.:Restrictingbacktrackinginconnectioncalculi.AICommunications23(2- 3), 159–182 (2010).https://doi.org/10.3233/AIC-2010-0464

    2010 doi

  20. [28]

    Prentice Hall (1987),https://simon.peytonjones.org/slpj-book-1987/

    Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice Hall (1987),https://simon.peytonjones.org/slpj-book-1987/

    1987

  21. [29]

    In: Lusk, E., Overbeek, R

    Pfenning, F.: Single axioms in the implicational propositional calculus. In: Lusk, E., Overbeek, R. (eds.) CADE-9. LNCS (LNAI), vol. 310, pp. 710–713. Springer (1988).https://doi.org/10.1007/BFb0012869

    1988 doi

  22. [30]

    Australasian Journal of Philosophy34(3), 182–192 (1956).https://doi.org/10.1080/ 00048405685200181

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

    1956

  23. [31]

    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 18 Christoph Wernhard

    2023 doi

  24. [32]

    In: Douglas, M.R., Hales, T.C., Kaliszyk, C., Schulz, S., Urban, J

    Rawson, M., Zombori, Z., Doré, M., Wernhard, C.: Project proposal: Forward reasoning in hindsight. In: Douglas, M.R., Hales, T.C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) AITP 2024 (Informal Book of Abstracts) (2024), online:https:// aitp-conference.org/2024/abstract/AITP_2...

    2024

  25. [33]

    Rezus, A.: Witness Theory – Notes onλ-calculus and Logic, Studies in Logic, vol. 84. College Publications, London (2020)

    2020

  26. [34]

    Projektarbeit in informatik, Fachbereich Informatik, Universität Kaiserslautern (1993),http: //wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Sch93-project.ps.gz, (Ger- man 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, (Ger- man Language)

    1993

  27. [35]

    In: Fontaine, P

    Schulz, S., Cruanes, S., Vukmirović, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 27. pp. 495–507. No. 11716 in LNAI, Springer (2019).https:// doi.org/10.1007/978-3-030-29436-6_29

    2019 doi

  28. [36]

    In: CADE-12

    Schumann, J.M.P.: DELTA — A bottom-up preprocessor for top-down theorem provers. In: CADE-12. LNCS (LNAI), vol. 814, pp. 774–777. Springer (1994). https://doi.org/10.1007/3-540-58156-1_58

    1994 doi

  29. [37]

    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

  30. [38]

    From CNF to TH0, TPTP v6.4.0

    Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reasoning59(4), 483–502 (2017).https://doi. org/10.1007/S10817-009-9143-8

    2017 doi

  31. [39]

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

    2001 doi

  32. [40]

    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

  33. [41]

    Wernhard, C.: CD Tools, online:http://cs.christophwernhard.com/cdtools/, accessed Feb 10, 2025

    2025

  34. [42]

    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

  35. [43]

    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

    2023

  36. [44]

    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

  37. [45]

    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

  38. [46]

    CoRR abs/2505.12305(2025).https://doi.org/10.48550/arXiv.2505.12305

    Wernhard, C., Zombori, Z.: Mathematical knowledge bases as grammar- compressed proof terms: Exploring Metamath proof structures. CoRR abs/2505.12305(2025).https://doi.org/10.48550/arXiv.2505.12305

    2025 doi arXiv

  39. [47]

    Wernhard, C., Zombori, Z.: Are proof structures machine-learnable? (2026), in preparation

    2026

  40. [48]

    Wielemaker, J.: Annotation post to predicateterm_factorized/3, May 07 2014, online:http://140.211.15.118/pldoc/doc_for?object=terms%3Aterm_ factorized/3, accessed Nov 21, 2020 Generating Theorems by Generating Proof Structures 19

    2014

  41. [49]

    Theory and Practice of Logic Programming12(1-2), 67–96 (2012).https://doi.org/10.1017/ S1471068411000494

    Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. Theory and Practice of Logic Programming12(1-2), 67–96 (2012).https://doi.org/10.1017/ S1471068411000494

    2012

  42. [50]

    Computers Math

    Wos, L.: The resonance strategy. Computers Math. Applic.29(2), 133–178 (1995). https://doi.org/10.1016/0898-1221(94)00220-F

    1995 doi

  43. [51]

    top-level

    Wos, L.: Conquering the Meredith single axiom. J. Autom. Reasoning27(2), 175– 199 (2001).https://doi.org/10.1023/A:1010691726881 Appendices A Supplementary Material for Section 3: Conversion to Implication Form 19 B Supplementary Material for Section 4: Cardinalities of Levels...

    2001 doi

  44. [2015]

    9168, pp

    LNCS, vol. 9168, pp. 46–57. Springer (2015).https://doi.org/10.1007/ 978-3-319-21500-6_3

    2015

Pith tools

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