Pith. sign in

REVIEW 3 major objections 5 minor 46 references

Hammering Higher Order Set Theory

T0 review · 3 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read This paper claims that replacing subproofs with automated theorem prover calls can shrink a formal higher-order set theory development to about 46% of its original length, with 82% of subgoals solved automatically.

desk verdict Useful and honest hammering paper: new Megalodon benchmark and big text reduction, but the shorter file is trusted, not kernel-checked. read the letter →

arxiv 2509.08264 v1 pith:BEJXLM2Y submitted 2025-09-10 cs.LO

Chad E. Brown , Cezary Kaliszyk , Martin Suda , Josef Urban This is my paper
classification cs.LO MSC 03B3568V20
keywords automatedtheoremprovinghigher-orderlogicsettheoryhammerproofreconstructionTPTPbenchmarksurrealnumbersMegalodon
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

This paper tries to establish that a large, fully formal mathematical development in higher-order set theory can be drastically shortened by handing many subproofs to automated theorem provers. Starting from a 45,004-line Megalodon formalization of 999 theorems—including 12 of the standard "Freek100" theorems, Conway's surreal numbers, and irrationality of the square root of two—the authors generated 41,738 subgoal problems and found that automated provers could solve 34,172 of them, 82%, within 60 seconds. By keeping only the largest replaceable blocks, the development shrinks to 3,401 prover calls in a 17,435-line file, about 46% of the original text. The approach works so directly because Megalodon's logic is already extensional higher-order logic, so no elaborate encoding is needed to connect it to higher-order automated provers. The paper leaves proof reconstruction—producing checkable proof objects for those prover calls—as future work.

What carries the argument

The load-bearing mechanism is the 'aby' ('automated by') tactic. It takes a current Megalodon subgoal and an explicit list of dependency names, exports them as a TH0 or FOF TPTP problem, and—if any of the connected automated provers solves it—replaces the original subproof with a single call to that prover. The tactic works because the export is a direct translation rather than an encoding: Megalodon's base type is sets and its logic is classical extensional higher-order logic, which is exactly the target logic of the provers. The 'hammer' behavior in the Emacs interface automates premise selection by sending the whole preceding development.

What would settle it

Take any one of the 3,401 final 'aby' calls, ask the prover for a machine-checkable proof object, and expand it into a Megalodon proof term; failure on even one call would show the shortened development is not fully verified, and a systematic check of all 3,401 would settle the 82% replacement claim.

Watch

Extended reading notes

Core claim

The central claim is quantitative: 34,172 of the 41,738 subgoals in a 999-theorem higher-order set theory development are provable by automated theorem provers in 60 seconds, and 3,401 such calls suffice to reproduce the whole development in 46% of its original line count. The authors argue this is possible because the set theory is formalized in Megalodon, whose simply typed, extensional higher-order logic matches the native logic of higher-order automated provers; each subgoal with its dependency list is exported directly to a TH0, or when first-order, FOF TPTP problem. They compare six provers on the resulting benchmark and report the strongest solving 94.8% of the final 3,401 problems. A

Load-bearing premise

The entire reduction relies on trusting that a successful prover run on an exported problem really proves the original subgoal, which in turn requires the export to preserve meaning and the provers to be sound.

Editorial extensions

If this is right

  • A 45,004-line formalization can be compressed to 17,435 lines (159,363 characters) while keeping the same theorem statements, simply by replacing the largest provable subproofs with 3,401 'aby' calls.
  • The 41,738 generated problems form a new benchmark for higher-order automated theorem provers, and the comparative evaluation shows which provers handle set-theoretic subgoals best, with the top prover solving 94.8% of the final problems.
  • Because Megalodon's logic is already the logic of higher-order automated provers, no type encodings or first-order translations are required, making higher-order set theory a particularly easy target for hammer-style automation.
  • The shortened development is not fully proof-checked; a complete version would require proof reconstruction, for example translating automated prover proof objects back into Megalodon terms, which the paper discusses via Dedukti.

Reading between the lines

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

  • If proof reconstruction matures, the 3,401 'frontier' problems could serve as a standing test set for proof-object checkers, not just solvers: each solved problem becomes a certification challenge.
  • The compression ratio is likely sensitive to proof style; a development written with heavy tactic automation or many already-small proofs would offer fewer large replaceable blocks, so the 46% figure should be read as specific to this deliberately detailed development.
  • The same direct-translation trick should transfer to other proof systems whose foundational logic is already extensional higher-order logic, potentially avoiding the translation overhead that first-order hammers incur.
  • A live hammer in the editor, demonstrated in the paper, suggests the workflow could shift from post-hoc compression to interactive writing: authors sketch case splits and let automated provers fill routine arithmetic, as in the exponent example.
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 / 5 minor

Summary. The paper presents a hammer-style ATP automation for Megalodon, a higher-order set theory prover. The authors first describe a 45,004-line Megalodon development formalizing 12 Freek100 theorems, including surreal numbers, the fundamental theorem of arithmetic, and irrationality of sqrt(2). They extract 41,738 TH0 subgoal problems (and 29,880 FOF problems where the subgoal is first-order), evaluate six higher-order ATPs with a 60-second timeout, and report that 34,172 (82%) of the subgoals are provable by at least one prover. After filtering for maximal-text-replacement and applying 'some manual modifications,' they obtain 3,401 automated `aby` calls in a 17,435-line file, about 46% of the original size. The paper also describes an Emacs-based full hammer mode and discusses proof reconstruction, including preliminary experiments with Vampire's Dedukti output.

Significance. The benchmark of 41,738/51,243 subgoal problems extracted from a substantial higher-order set theory development is a valuable resource for the ATP and ITP communities, and the systematic comparison of Vampire, Zipperposition, E, Lash, and cvc5 provides useful empirical data. The authors are honest about the limitation that ATP successes are trusted rather than checked. However, the central claim of 'significantly shortening a formal development' is not yet fully justified: the shortened file contains oracle calls whose proofs have not been reconstructed and are not kernel-checked. If the paper is reframed as an experimental evaluation of ATP hammering for a higher-order set theory with proof reconstruction as future work, the contribution stands. As it stands, the headline claim overstates the formal status of the result.

major comments (3)
  1. [Section 4 / Section 3.2] The correctness of the shortened development is load-bearing. The text states: 'when an ATP completes the proof of a subgoal, we trust that there is, indeed, a proof.' No proof-term reconstruction is performed for the 3401 `aby` calls. Since the original development's value is its kernel-checked proof terms, the 17,435-line result is not a formal development in the same sense. Please either (a) reconstruct or independently check the ATP proofs (e.g., replay in Megalodon, verify TH0/FOF proofs in a certified checker), or (b) explicitly present the result as an experimental oracle-backed development whose correctness is pending proof reconstruction, and adjust the title and abstract accordingly.
  2. [Section 3.2] The reduction from 41,738 subgoals to 3,401 ATP calls depends on 'some manual modifications' that are not specified. This prevents reproducibility of the headline 46% figure. Please document these modifications precisely or provide the scripts and diff files so the reduction pipeline is transparent and independently verifiable.
  3. [Section 3.1] The claim of a 'direct' translation to TH0/FOF is asserted but not substantiated. No formal definition of the translation is given, nor is there a correctness argument that a proof of the exported problem yields a proof of the corresponding Megalodon subgoal. Since the benchmark and the trust in ATP results depend on this translation's semantic faithfulness, please provide a precise description of the translation and prove (or at least rigorously argue) that it is conservative or sound with respect to Megalodon's logic.
minor comments (5)
  1. [Section 2.3] In the surreal numbers representation paragraph, 'It is also to see' should be 'It is also easy to see.'
  2. [Section 3.2] The sentence 'We also called a recent first order version of Vampire was called on the FOF problems' contains a grammar error; it should be 'We also called a recent first-order version of Vampire on the FOF problems.'
  3. [Section 4.1] The Dedukti experiment notes that 'some of the steps to produce clausal form are left unjustified at the moment.' Please state explicitly which steps these are and whether they are the clausification steps; this is relevant to the trust question and to the usefulness of the Dedukti output for reconstruction.
  4. [Tables 1 and 2] The tables would be easier to interpret if the union of provers were also reported (e.g., number/percentage of problems solved by at least one prover), alongside the per-prover columns.
  5. [References] Reference [14] is listed as 'Available online.' without a venue or year; if this is a preprint, please include the arXiv identifier or update the reference.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the ATP-size-reduction and prover-comparison claims are direct measurements on independently generated problem files; the only trust assumption (ATP soundness/export faithfulness) is a correctness risk, not circularity.

full rationale

The paper's central quantitative claims — 34,172 of 41,738 subgoals solvable, and a shortened 17,435-line/159,363-character development (~46%) — are obtained by exporting each Megalodon subgoal to TPTP (Section 3.1: 'we can directly translate the given dependencies and current subgoal into the TH0 TPTP format'), running automated theorem provers, and filtering for maximal text replacement (Section 3.2: 'After filtering for the problems that allow the largest texts to be replaced ... we were left with 3401 calls to an ATP and a development with 17435 lines and 159363 characters'). The subgoals are generated from the original proof scripts before any ATP result is used, so the solvability numbers and size reduction are measurements, not re-statements of inputs. No fitted parameter is renamed as a prediction. The paper's self-citations (e.g., Megalodon [15], Lash [12], higher-order Vampire [4]) are routine system references and are not load-bearing: the empirical comparison would stand even if those systems were replaced by independent implementations. The genuine limitation is the paper's own acknowledgment in Section 4: 'when an ATP completes the proof of a subgoal, we trust that there is, indeed, a proof,' and Section 4.1: 'some of the steps to produce clausal form are left unjustified at the moment.' These are trust/omission caveats about soundness and proof reconstruction; they affect whether the shortened text is a verified formal proof, but they do not amount to a circular derivation. The paper makes no claim that the ATP outputs are derived from the conclusion, and no equation or definition reduces the target result to its input. Honest non-finding: no significant circularity.

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

The paper's central claim is empirical; its load-bearing premises are the semantic faithfulness of the export to TH0, the soundness and trust of external ATPs, and the standard Megalodon set theory axioms. None of these are proved inside the paper, and the ATP trust is explicitly acknowledged in Section 4.

assumptions (3)
  • domain assumption The Megalodon-to-TH0 translation is semantically faithful, so TH0 proofs transfer back to Megalodon.
    Section 3.1 asserts direct translation; no verification is provided.
  • domain assumption The automated theorem provers used are sound for classical extensional higher-order logic.
    Section 4 states the authors trust ATP results rather than reconstructing proof terms.
  • domain assumption The underlying Tarski-Grothendieck set theory axioms of Megalodon are consistent and adequate for the formalization.
    Section 2.1 lists primitives and axioms from [15]; the paper relies on them without re-proving.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Hammering Higher Order Set Theory." pith.science (2026). https://pith.science/paper/BEJXLM2Y

@misc{pith2026250908264,
  author       = {Pith},
  title        = {Pith review of: Hammering Higher Order Set Theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BEJXLM2Y}},
  note         = {Machine review of arXiv:2509.08264}
}
read the original abstract

We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of two. Higher order automated theorem provers are particularly useful here, since the underlying framework of higher order set theory coincides with the classical extensional higher order logic of (most) higher order automated theorem provers, so no significant translation or encoding is required. Additionally, many subgoals are first order and so first order automated provers often suffice. We compare the performance of different provers on the subgoals generated from the development. We also discuss possibilities for proof reconstruction, i.e., obtaining formal proof terms when an automated theorem prover claims to have proven the subgoal.

Figures

Figures reproduced from arXiv: 2509.08264 by the authors.

Figure 1
Figure 1. Original Megalodon Proof. create a TH0 file which includes the whole previous development. Then it calls Vampire with a schedule constructed for the Sledgehammer division of the CASC competition.12 If successful, the names of the used axioms are translated back to the Megalodon syntax and the aby call using them is automatically inserted into the current buffer. The operation is shown in Figures 1, 2, and 3. 12 The … view at source ↗
Figure 2
Figure 2. Aby call invoked inside the proof. To test this “full hammer” performance, we generated corresponding ATP problems each time a tactic was used in the original development. This resulted in 51243 TH0 problems.13 Note that this is larger than the 41738 premise se￾lected problem files. This difference arises from several factors, which we do not discuss in detail here. We called Vampire with the two portfolios for 60s.… view at source ↗
Figure 3
Figure 3. Successful aby call with the axiom names inserted. behaving like the Naproche system [19]. That is, when an ATP completes the proof of a subgoal, we trust that there is, indeed, a proof. Ultimately it would be more satisfying to do proof reconstruction so that we still obtain complete proof terms even when some subgoals are completed by ATPs. A common technique [33] is to use an ATP to prune the dependencies and the… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

46 extracted references · 35 canonical work pages

  1. [1]

    Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lach- nitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors,Tools and ...

    2022

  2. [2]

    Superpositionforlambda-freehigher-orderlogic.Log

    Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. Superpositionforlambda-freehigher-orderlogic.Log. Methods Comput. Sci.,17(2),

    work page

  3. [3]

    THF0 - the core of the TPTP language for higher-order logic

    Christoph Benzmüller, Florian Rabe, and Geoff Sutcliffe. THF0 - the core of the TPTP language for higher-order logic. InIJCAR 2008, volume 5195 ofLNCS, pages 491–506. Springer, 2008

    work page 2008

  4. [4]

    A higher-order vampire (short paper)

    Ahmed Bhayat and Martin Suda. A higher-order vampire (short paper). In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors,Au- tomated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 ofLecture Notes in Com- puter Science, pages 75–85. Springer, 2024.doi:10.1...

    doi:10.1007/978-3-031-63498-7 2024

  5. [5]

    PhD thesis, Fakultät für Informatik, Technische Universität München, 2012

    Jasmin Christian Blanchette.Automatic Proofs and Refutations for Higher-Order Logic. PhD thesis, Fakultät für Informatik, Technische Universität München, 2012

    work page 2012

  6. [6]

    Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extend- ing Sledgehammer with SMT solvers. In Nikolaj Bjørner and Viorica Sofronie- Stokkermans, editors,CADE, volume 6803 ofLNCS, pages 116–130. Springer, 2011

    work page 2011

  7. [7]

    Encoding monomorphic and polymorphic types.Log

    Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Small- bone. Encoding monomorphic and polymorphic types.Log. Methods Comput. Sci., 12(4), 2016.doi:10.2168/LMCS-12(4:13)2016

    work page doi:10.2168/lmcs-12(4:13)2016 2016

  8. [8]

    A learning-based fact selector for Isabelle/HOL

    Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016. URL:http://dx.doi.org/10.1007/ s10817-016-9362-8,doi:10.1007/s10817-016-9362-8

    work page doi:10.1007/s10817-016-9362-8 2016

Show all 46 references
  1. [9]

    Paulson, and Josef Urban

    Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED.J. Formalized Reasoning, 9(1):101–148,

  2. [10]

    Chad E. Brown. Reconsidering Pairs and Functions as Sets.Journal of Automated Reasoning, 55(3):199–210, Oct 2015

    2015

  3. [11]

    Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, and Josef Urban

    Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, and Josef Urban. GRUNGE: A grand unified ATP challenge. In Pascal Fontaine, edi- tor,Automated Deduction - CADE 27 - 27th International Conference on Auto- mated Deduction, Natal, Brazil, August 27-30, 2019, P...

    2019 doi

  4. [12]

    Brown and Cezary Kaliszyk

    Chad E. Brown and Cezary Kaliszyk. Lash 1.0 (system description). In Jas- min Blanchette, Laura Kovács, and Dirk Pattinson, editors,Automated Reasoning 16 C. Brown, C. Kaliszyk, M. Suda, J. Urban - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 20...

    2022 doi

  5. [13]

    Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban

    Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proof- gold: Blockchain for formal methods. In Zaynah Dargaye and Clara Schnei- dewind, editors,4th International Workshop on Formal Methods for Blockchains, FMBC@CAV 2022, August 11, 2022, Haifa, Israel, volu...

    2022 doi

  6. [14]

    Brown, Cezary Kaliszyk, and Josef Urban

    Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Payment channels with proofs. Available online., 2025. URL:http://grid01.ciirc.cvut.cz/~mptp/FMBC_2025_ paper_6.pdf

    2025

  7. [15]

    Brown and Karol Pąk

    Chad E. Brown and Karol Pąk. A tale of two set theories. In Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors,Intelli- gent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings...

    2019

  8. [16]

    Brown and Josef Urban

    Chad E. Brown and Josef Urban. Extracting higher-order goals from the mizar mathematical library. In Michael Kohlhase, Moa Johansson, Bruce R. Miller, Leonardo de Moura, and Frank Wm. Tompa, editors,Intelligent Computer Mathe- matics - 9th International Conference, CICM 2016, ...

    2016

  9. [17]

    Brown, and Josef Urban

    Mario Carneiro, Chad E. Brown, and Josef Urban. Automated theorem proving for Metamath. In Adam Naumowicz and René Thiemann, editors,14th Interna- tional Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 ofLIPIcs, pag...

    2023 doi

  10. [18]

    Conway.On numbers and games, Second Edition

    John H. Conway.On numbers and games, Second Edition. A K Peters, 2001

    2001

  11. [19]

    The Naproche system: Proof-checking mathematical texts in controlled natural language

    Marcos Cramer. The Naproche system: Proof-checking mathematical texts in controlled natural language. In Hermann Cölfen, Ulrich Schmitz, and Bernhard Schröder, editors,Sprache und Datenverarbeitung, volume 38, pages 9–33. Univer- sitätsverlag Rhein-Ruhr, Duisburg, 2014

    2014

  12. [20]

    Hammer for Coq: Automation for depen- dent type theory.J

    Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for depen- dent type theory.J. Autom. Reasoning, 61(1-4):423–453, 2018.doi:10.1007/ s10817-018-9458-4

    2018

  13. [21]

    Interpretation of a Mizar-like logic in first-order logic

    Ingo Dahn. Interpretation of a Mizar-like logic in first-order logic. In Ricardo Caferra and Gernot Salzer, editors,FTP (LNCS Selection), volume 1761 ofLNCS, pages 137–151. Springer, 1998

    1998

  14. [22]

    TheDeduktilogical framework.https://deducteam.github.io

  15. [23]

    Seventeen provers under the hammer

    Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, and Makarius Wenzel. Seventeen provers under the hammer. In June Andronick and Leonardo de Moura, editors,13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 23...

    2022 doi

  16. [24]

    Premise selection and external provers for HOL4

    Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. InCertified Programs and Proofs (CPP’15), LNCS. Springer, 2015. http://dx.doi.org/10.1145/2676724.2693173. URL:http://dx.doi.org/10. 1145/2676724.2693173,doi:10.1145/2676724.2693173. Hammer...

    2015

  17. [25]

    Michael Gordon. Set theory, higher order logic or both? In Joakim von Wright, Jim Grundy, and John Harrison, editors,Theorem Proving in Higher Order Logics, TPHOLs’96, volume 1125 ofLNCS, pages 191–201. Springer, 1996.doi:10.1007/ BFb0105405

    1996

  18. [26]

    Integrating Gandalf and HOL

    Joe Hurd. Integrating Gandalf and HOL. In Yves Bertot, Gilles Dowek, An- dré Hirschowitz, C. Paulin, and Laurent Théry, editors,TPHOLs, volume 1690 of LNCS, pages 311–322. Springer, 1999

    1999

  19. [27]

    An LCF-style interface between HOL and first-order logic

    Joe Hurd. An LCF-style interface between HOL and first-order logic. In Andrei Voronkov, editor,CADE, volume 2392 ofLNCS, pages 134–138. Springer, 2002

    2002

  20. [28]

    First-order proof tactics in higher-order logic theorem provers

    Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz, editors,Design and Application of Strate- gies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003- 212448 in NASA Technical Reports, pages 56...

    2003

  21. [29]

    Learning-assisted automated reasoning with Flyspeck.J

    Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck.J. Autom. Reasoning, 53(2):173–213, 2014.doi:10.1007/ s10817-014-9303-3

    2014

  22. [30]

    Learning-assisted automated reasoning with Flyspeck.J

    Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck.J. Autom. Reasoning, 53(2):173–213, 2014. URL:http://dx.doi.org/ 10.1007/s10817-014-9303-3,doi:10.1007/s10817-014-9303-3

    2014 doi

  23. [31]

    Case study: Verified vampire proofs in the lambdapi-calculus modulo, 2025

    Anja Petković Komel, Michael Rawson, and Martin Suda. Case study: Verified vampire proofs in the lambdapi-calculus modulo, 2025. URL:https://arxiv. org/abs/2503.15541,arXiv:2503.15541

    2025

  24. [32]

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

    2005

  25. [33]

    Jia Meng and Lawrence C. Paulson. Lightweight relevance filtering for machine- generated resolution problems.Journal of Applied Logic, 7(1):41–57, 2009. Special Issue: Empirically Successful Computerized Reasoning. URL:https: //www.sciencedirect.com/science/article/pii/S157086...

    2009

  26. [34]

    N. D. Goodman and J. Myhill. Choice Implies Excluded Middle.Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 24:461, 1978

    1978

  27. [35]

    Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers

    Karol Pak and Cezary Kaliszyk. Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors,15th International Conference on Interac- tive Theorem Proving, ITP 2024, September 9-14, 2024,...

    2024 doi

  28. [36]

    Lawrence C. Paulson. Set theory for verification: I. from foundations to functions. Journal of Automated Reasoning, 11:353–389, 1993

    1993

  29. [37]

    Lawrence C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Renate A. Schmidt, Stephan Schulz, and Boris Konev, editors,Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAA...

    2010 doi

  30. [38]

    Dover, 2006

    Dag Prawitz.Natural deduction: a proof-theoretical study. Dover, 2006

    2006

  31. [39]

    Axiomofchoiceandcomplementation.Proceedings of the American Mathematical Society, 51:176–178, 1975

    R.Diaconescu. Axiomofchoiceandcomplementation.Proceedings of the American Mathematical Society, 51:176–178, 1975. 18 C. Brown, C. Kaliszyk, M. Suda, J. Urban

    1975

  32. [40]

    Cambridge University Press, 1903

    Bertrand Russell.The Principles of Mathematics. Cambridge University Press, 1903

    1903

  33. [41]

    J. Urban. Translating Mizar for First Order Theorem Provers. In A. Asperti, B. Buchberger, and J.H. Davenport, editors,Proceedings of the 2nd International Conference on Mathematical Knowledge Management, number 2594 in LNCS, pages 203–215. Springer, 2003

    2003

  34. [42]

    MPTP – Motivation, Implementation, First Experiments.J

    Josef Urban. MPTP – Motivation, Implementation, First Experiments.J. Autom. Reasoning, 33(3-4):319–339, 2004.doi:10.1007/s10817-004-6245-1

    2004 doi

  35. [43]

    Extending a high- performance prover to higher-order logic

    Petar Vukmirović, Jasmin Blanchette, and Stephan Schulz. Extending a high- performance prover to higher-order logic. In Sriram Sankaranarayanan and Natasha Sharygina, editors,Tools and Algorithms for the Construction and Anal- ysis of Systems - 29th International Conference, T...

    2023

  36. [114]

    Springer, 2016.doi:10.1007/978-3-319-42547-4\_8

    2016 doi

  37. [2016]

    URL:http://dx.doi.org/10.6092/issn.1972-5787/4593,doi:10.6092/ issn.1972-5787/4593

    1972 doi

  38. [2021]

    URL:https://lmcs.episciences.org/7349

Pith tools

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