Pith. sign in

REVIEW 2 major objections 3 minor 41 references

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

T0 review · 2 major / 3 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read A new tool extracts the exact variable instantiations used inside successful Metis proofs and replays the proof from those instantiated facts, speeding up Sledgehammer and making proofs easier to read.

desk verdict A solid, useful systems contribution whose headline numbers are slightly overclaimed because the evaluation lacks a control for the extra preplay time given to Metis. read the letter →

arxiv 2508.20738 v1 pith:TI4FEQND submitted 2025-08-28 cs.LO

Lukas Bartl , Jasmin Blanchette , Tobias Nipkow This is my paper
classification cs.LO
keywords variableinstantiationsparamodulationIsabelle/HOLSledgehammerMetisproofreconstructionautomatedtheoremprovinghigher-orderlogic
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

Metis proves goals in Isabelle/HOL by ordered paramodulation, but its successful proofs carry hidden information: the exact substitution applied to each input lemma. This paper shows how to recover that information by walking the fine-grained proof tree and accumulating the substitutions attached to Subst inference steps, and it states and proves Theorem 1: any Metis proof can be replayed from the instantiated axiom clauses alone, without any Subst steps, using at most as many steps as the original. The paper then builds a tool that translates these inferred instantiations back into Isabelle syntax, instantiates the lemmas, and hands them to Sledgehammer's preplay step. The payoff is practical: more proofs reconstruct successfully (44 extra one-line proofs in the main evaluation), generated metis calls run on average 38% faster, and instantiated facts let methods like auto work on goals where they previously failed, producing shorter proofs a human can follow.

What carries the argument

The central object is the recursive function infer(θ,σ), which walks a Metis proof tree, composing the substitutions attached to Subst inference rules into an accumulator σ and returning, at each Axiom leaf, the pair (clause, σ). Theorem 1 asserts that the instantiated axiom clauses it collects admit a proof with no Subst steps and no more steps than the original, with resolution steps disappearing when instantiation unifies literals. A second mechanism, the read-back translation from Metis terms to Isabelle terms, is what makes the construction usable: it decodes app encodings, eliminates Skolem terms by replacing them with wildcards, expands SKBCI combinators and supercombinators followed

What would settle it

Run the extended Sledgehammer on the 5,000 benchmark goals and count every case where metis succeeds on the original facts, the tool infers instantiations, but the instantiated facts either fail to parse or fail to close the goal within the preplay limit; the paper reports 5 such cases in the smart run and 18 in the true run, so a substantially higher rate would falsify the practical claim. At the theorem level, take any Metis proof, apply the Theorem 1 transformation, and replay the instantiated clauses: a replay that still needs a Subst step or uses more steps would falsify the structural cl

Watch

Extended reading notes

Core claim

At the center of the paper is a structural fact about the Metis proof calculus, whose six rules include an explicit Subst rule. Given a finished proof, the recursive function infer(θ,σ) re-traverses the proof tree; at each Subst step it composes the substitution into an accumulator, and at each Axiom leaf it records the clause together with the accumulated substitution for that occurrence. The paper proves by induction that the set of instantiated axiom clauses Cσ obtained this way admits a proof whose conclusion is still the empty clause, uses no Subst steps, and has no more proof steps than the original, because instantiation can unify literals and thereby remove resolution steps. Around t

Load-bearing premise

The practical payoff rests on the heuristic that every inferred Metis substitution can be read back into Isabelle's own syntax; the paper reports cases where Isabelle could not parse the instantiated terms back, so no instantiated proof could be produced.

Editorial extensions

If this is right

  • Sledgehammer reconstructs one-line proofs for goals that previously timed out: 44 additional ATP proofs in the smart run, roughly 18% of the cases where no one-line proof existed before.
  • Generated proofs run faster: average metis execution dropped from 221 ms to 137 ms between runs, a 38% decrease that applies every time the proof text is re-checked.
  • Instantiated facts shift proof search to simpler methods: after instantiation, a larger fraction of proofs use the default metis encoding (88.3% to 95.4%), and the extra fact ext is needed less often.
  • Users get more readable low-level facts: a fact used multiple times appears with each specific instantiation, so a human can see exactly which lemma instance drove each step.
  • The Theorem 1 transformation guarantees a substitution-free Metis replay for every original proof, so at the clause level the instantiated facts are no harder to prove than the originals.

Reading between the lines

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

  • A natural extension, not pursued in the paper, would apply the same substitution-recovery pass to individual steps of detailed Isar proofs, not just to one-line metis calls, making instantiations visible per proof step.
  • The inferred instantiations could be exported as a lightweight proof certificate: the instantiated clauses and substitution-free replay are independent of Metis's search heuristics and could be checked by any fine-grained paramodulation checker.
  • Some SMT solvers can report their instantiations directly, so the same preplay-with-instantiation pipeline could likely be fed without analyzing proof trees at all, a direction the paper mentions only briefly.
  • Because the read-back failures are tied to Isabelle's flexible parsing, adding explicit type annotations to ambiguous inferred instantiations would likely eliminate most of the reported 5 and 18 preplay failures.
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

2 major / 3 minor

Summary. The paper extends Isabelle's Metis proof method and Sledgehammer with a mechanism to infer variable instantiations from successful Metis proofs. The central theoretical result, Theorem 1, states that a successful Metis proof can be transformed into a proof from the instantiated axiom clauses, with no Subst inference steps and no more proof steps. The paper also describes a heuristic translation procedure that maps Metis substitutions to Isabelle terms, and an extension to Sledgehammer's preplay module that uses instantiated facts. The empirical evaluation on 5000 goals from 50 Archive of Formal Proofs entries reports 44 additional one-line reconstructions in smart mode and a 38% reduction in average Metis time, and claims that instantiations improve success rate, speed, and readability.

Significance. If confirmed, the contributions are practically valuable. Theorem 1 is a clean correctness guarantee for the core idea, the implementation is integrated into Isabelle (available starting with Isabelle 2025), and the raw data is publicly provided. The final proofs are checked by Isabelle's inference kernel, so the tool is sound. However, the quantitative claims about success-rate increase and speedup are not yet fully supported: the evaluation lacks a control for the increased preplay time budget, and the speed comparison is based on two unpaired runs. These issues are load-bearing for the abstract's headline claims, so the paper requires revision before the empirical results can be accepted as stated.

major comments (2)
  1. [§5–§6, Table 1] The 44 additional one-line proofs attributed to instantiations are confounded with the increased preplay time budget. In smart mode, the metis call used to infer instantiations is run for five times the preplay time limit (5s), and this call is made only after 1s preplay has failed. Any of the 44 cases in which this 5s metis call succeeds on the original facts would likely also be reconstructed as a one-line proof if Sledgehammer had simply run preplay with a 5s limit and instantiate=false. The paper does not report a control run (instantiate=false with a 5s preplay limit), nor does it report the durations or success rates of the 5s inference calls. The claim that instantiations 'increase Sledgehammer's success rate' is therefore not established. Please provide such a control, or at minimum report how many of the 44 goals are already solved by a 5s metis call on the uninstantiated facts.
  2. [§6, Table 2] The reported 38% Metis speedup is based on comparing average times from two runs that differ in mode (smart vs true) and in the set of invocations (3373 vs 3358 ATP proofs). This is not a paired comparison. The statement that 'about 25% of cases (805 and 44 in Table 1)' are comparable is not a substitute: the intersection of the two runs is not determined by the table, and even for those goals the proof attempts differ in whether instantiations are present. To support the speed claim, please report paired per-goal comparisons (e.g., goals where both an uninstantiated and an instantiated metis proof succeed, comparing the times), or provide a control run with instantiate=false on the same goals. Without paired data, the observed average difference cannot be attributed to instantiations.
minor comments (3)
  1. [§4, Example 5] The composition order of substitutions in the calls to infer is easy to misread. For example, infer(2,{y↦Suc(x)}◦{m↦0,n↦y}) silently uses the composition convention of Definition 2; a short note or a different notation would improve clarity.
  2. [§6, Table 1] After Table 1, the phrase '18.0% of cases where there was no one-line proof before' should explicitly state the denominator (37 Isar + 164 failed + 44 = 245) to avoid ambiguity.
  3. [Abstract and §6] The abstract and conclusion say 'increase Sledgehammer's success rate,' but the evaluation measures one-line proof reconstruction success for ATP-found proofs, not overall Sledgehammer success (e.g., including Isar proofs and other methods). The wording should be adjusted to reflect the actual metric.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: instantiations are read off kernel-checked proofs; evaluation has confounds but no circularity.

full rationale

The central claim is a proof-transformation theorem, Theorem 1: "A Metis proof θ can be transformed into a new Metis proof derived from the instantiated axiom clauses... The new Metis proof does not involve the Subst inference rule and uses at most as many proof steps as θ." This is proved by induction and is not assumed as an input. The instantiations are not fitted parameters chosen to force a desired result; they are literally read off an existing successful Metis proof by the recursive `infer` function (Definition 3). The subsequent success of the instantiated facts is independently verified by Isabelle's inference kernel, so the conclusion is not baked in by construction. No load-bearing self-citation is present: citations to the authors' prior work ([6], [31], [32]) supply background on Sledgehammer, preplay, and Metis reconstruction, but do not by themselves justify the instantiation mechanism or forbid alternatives. The evaluation section does disclose limitations that are genuine correctness risks rather than circularity: "the metis call used to infer the instantiations is given more time than the proof methods during preplay. More precisely, it is executed for five times the preplay time limit (i.e., 5s by default)" (Section 5), which can confound the attribution of gains to instantiations rather than to extra proof search; and "Isabelle's extremely flexible syntax allows ambiguities and does not guarantee that all terms can be parsed back" (Section 6), explaining the 5 and 18 preplay failures. The two runs are also not fully paired because of nondeterminism. These are important interpretation concerns, but they do not make the derivation circular: the mathematical core is self-contained and kernel-checked. Score 2 reflects only minor self-citation and the self-involving evaluation setup; no specific circular reduction was found.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new mathematical entities. The 'wildcard' symbol '_' is a display placeholder, not an entity. The central claim rests on domain assumptions about the soundness of the Metis calculus and the faithfulness of the translation layer, plus a benchmark representativeness assumption for the empirical evaluation.

free parameters (1)
  • metis instantiation time multiplier = 5
    Section 5: the metis call used to infer instantiations is given five times the preplay time limit (5s by default). This hand-chosen value affects how often instantiations are found and the measured tradeoff between Sledgehammer time and proof speed.
assumptions (4)
  • domain assumption The Metis proof system is sound with respect to Isabelle's logic.
    Section 2 describes Metis as the reconstruction prover; the extracted instantiations are used to build new proofs that must be accepted by Isabelle's kernel, so soundness of Metis's inference rules is assumed.
  • domain assumption The translation from polymorphic higher-order logic to untyped first-order logic, and its inverse, is faithful enough for proof reconstruction.
    Section 4 relies on decoding the encodings (symbols, app, type encodings) introduced by the translation. This is inherited from existing metis reconstruction code and is not re-proved.
  • domain assumption Metis's clausifier preserves variable names, so inferred Metis substitutions can be mapped back to Isabelle free variables.
    Section 4 states that the clausifier preserves variable names, in contrast to other ATPs mentioned in Section 8. This is essential for the translation procedure to work.
  • ad hoc to paper The 50 Archive of Formal Proofs entries and randomly selected 100 goals per entry are representative of typical Sledgehammer usage.
    Section 6 uses this benchmark set, selected from a prior paper (Desharnais et al. [16]). The representativeness is not established, and the selection is not seeded.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL." pith.science (2026). https://pith.science/paper/TI4FEQND

@misc{pith2026250820738,
  author       = {Pith},
  title        = {Pith review of: Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TI4FEQND}},
  note         = {Machine review of arXiv:2508.20738}
}
read the original abstract

Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas are found by Sledgehammer, a tool that integrates external automatic provers. We present a new tool that analyzes successful Metis proofs to derive variable instantiations. These increase Sledgehammer's success rate, improve the speed of Sledgehammer-generated proofs, and help users understand why a goal follows from the lemmas.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

41 extracted references · 26 canonical work pages

  1. [1]

    CoRRabs/2311.07185 (2023)

    Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Dedukti: a logical framework based on theλΠ-calculus modulo theory. CoRRabs/2311.07185 (2023). https: //doi.org/10.48550/ARXIV.2311.07185 18 L. Bartl et al

    arXiv doi:10.48550/arxiv.2311.07185 2023

  2. [2]

    In: Stickel, M.E

    Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE-10. LNCS, vol. 449, pp. 427–441. Springer (1990). https://doi.org/10.1007/3-540-52885-7_105

    work page doi:10.1007/3-540-52885-7_105 1990

  3. [3]

    In: Fisman, D., Rosu, G

    Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022, Part I. LNCS, vol. 13243, pp. 415–442. Springer (2022). h...

    work page doi:10.1007/978-3-030-99524- 2022

  4. [4]

    In: Benzmüller, C., Heule, M.J.H., Schmidt, R.A

    Bhayat, A., Suda, M.: A higher-order Vampire (short paper). In: Benzmüller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024, Part I. LNCS, vol. 14739, pp. 75–85. Springer (2024). https://doi.org/10.1007/978-3-031-63498-7_5

    work page doi:10.1007/978-3-031-63498-7_5 2024

  5. [5]

    Blanchette, J.: Hammering away: A user’s guide to Sledgehammer for Isabelle/ HOL (2025), https://isabelle.in.tum.de/website-Isabelle2025/dist/Isabelle2025/ doc/sledgehammer.pdf

    work page 2025

  6. [6]

    Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi- intelligible Isar proofs from machine-generated proofs. J. Autom. Reason.56(2), 155–200 (2016). https://doi.org/10.1007/S10817-015-9335-3

    doi:10.1007/s10817-015-9335-3 2016

  7. [7]

    Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Meth. Comput. Sci.12(4) (2016). https://doi.org/10. 2168/LMCS-12(4:13)2016

    work page 2016

  8. [8]

    Blanchette, J.C., Greenaway, D., Kaliszyk, C., Kühlwein, D., Urban, J.: A learning- based fact selector for Isabelle/HOL. J. Autom. Reason.57(3), 219–244 (2016). https://doi.org/10.1007/s10817-016-9362-8

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

Show all 41 references
  1. [9]

    In: Kerber, M

    Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the Archive of Formal Proofs. In: Kerber, M. (ed.) CICM 2015. LNCS, vol. 9150, pp. 1–15. Springer (2015). https://doi.org/10.1007/978-3-319-20615-8_1

    2015 doi

  2. [10]

    In: Beringer, L., Felty, A

    Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle: Superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 345–360. Springer (2012). https://doi.org/10.1007/978-3-642-32347-8_24

    2012 doi

  3. [11]

    In: Kobayashi, N., Worrell, J

    Blot, V., Dowek, G., Traversié, T., Winterhalter, T.: From rewrite rules to axioms in the λΠ-calculus modulo theory. In: Kobayashi, N., Worrell, J. (eds.) FoSSaCS 2024, Part II. LNCS, vol. 14575, pp. 3–23. Springer (2024). https://doi.org/10.1007/978- 3-031-57231-9_1

    2024 doi

  4. [12]

    In: Giesl, J., Hähnle, R

    Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 107–121. Springer (2010). https: //doi.org/10.1007/978-3-642-14203-1_9

    2010 doi

  5. [13]

    In: Schmidt, R.A

    Bouton, T., Oliveira, D.C.B.D., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151–156. Springer (2009). https://doi.org/10.1007/978-3-642-02959-2_12

    2009 doi

  6. [14]

    Chihani, Z., Miller, D., Renaud, F.: A semantic framework for proof evidence. J. Autom. Reason.59(3), 287–330 (2017). https://doi.org/10.1007/S10817-016-9380-6

    2017 doi

  7. [15]

    Archive of Formal Proofs (2021), https://isa-afp.org/entries/IsaGeoCoq.html

    Coghetto, R.: Tarski’s Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid. Archive of Formal Proofs (2021), https://isa-afp.org/entries/IsaGeoCoq.html

    2021

  8. [16]

    In: Andronick, J., de Moura, L

    Desharnais, M., Vukmirović, P., Blanchette, J., Wenzel, M.: Seventeen provers under the hammer. In: Andronick, J., de Moura, L. (eds.) ITP 2022. p. 8:1–8:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022). https://doi.org/10. 4230/LIPIcs.ITP.2022.8 Exploiting Instant...

    2022

  9. [17]

    In: Olivetti, N., Tiwari, A

    Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 293–301. Springer (2016). https://doi.org/10.1007/978-3-319-40229- 1_20

    2016 doi

  10. [18]

    In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J

    Gordon, M.J.C.: Introduction to the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) TPHOLs 1991. pp. 2–3. IEEE Computer Society (1991), https://ieeexplore.ieee.org/document/596265

    1991

  11. [19]

    In: LFP ’82

    Hughes, R.J.M.: Super-combinators: A new implementation method for applicative languages. In: LFP ’82. p. 1–10. ACM Press (1982). https://doi.org/10.1145/ 800068.802129

    1982

  12. [20]

    In: Archer, M., Vito, B.D., Muñoz, C

    Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics. p. 56–68. No. NASA/CP-2003-212448 in NASA Technical Reports (Sep 2003), https://www.gili...

    2003

  13. [21]

    In: Klusáček, D., Corbalán, J., Rodrigo, G.P

    Jette, M.A., Wickberg, T.: Architecture of the Slurm workload manager. In: Klusáček, D., Corbalán, J., Rodrigo, G.P. (eds.) JSSPP 2023. p. 3–23. Springer (2023). https://doi.org/10.1007/978-3-031-43943-8_1

    2023 doi

  14. [22]

    Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason.40(1), 35–60 (Sep 2007). https://doi.org/10.1007/s10817-007- 9085-y

    2007 doi

  15. [23]

    Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. App. Log.7(1), 41–57 (2009). https://doi.org/10.1016/J. JAL.2007.07.004

    2009 doi

  16. [24]

    In: Momigliano, A., Pientka, B., Pollack, R

    Miller, D.: Foundational proof certificates: Making proof universal and permanent. In: Momigliano, A., Pientka, B., Pollack, R. (eds.) LFMTP 2013. pp. 1–2. ACM (2013), https://doi.org/10.1145/2503887.2503894

    2013

  17. [25]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    2008 doi

  18. [26]

    Nipkow, T.: Equational reasoning in Isabelle. Sci. Comput. Prog.12(2), 123–149 (Jul 1989). https://doi.org/10.1016/0167-6423(89)90038-5

    1989 doi

  19. [27]

    LNCS, Springer (2002)

    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher- Order Logic. LNCS, Springer (2002). https://doi.org/10.1007/3-540-45949-9

    2002 doi

  20. [28]

    Nipkow, T., Prehofer, C.: Type reconstruction for type classes. J. Funct. Prog. 5(2), 201–224 (Apr 1995). https://doi.org/10.1017/S0956796800001325

    1995 doi

  21. [29]

    LNCS, Springer (1994)

    Paulson, L.C.: Isabelle: A generic theorem prover. LNCS, Springer (1994). https: //doi.org/10.1007/BFb0030541

    1994 doi

  22. [30]

    Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J. Univ. Comput. Sci. 5(3), 73–87 (1999). https://doi.org/10.3217/jucs-005-03-0073

    1999 doi

  23. [31]

    In: Sutcliffe, G., Schulz, S., Ternovska, E

    Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010. EPiC Series in Computing, vol. 2, p. 1–11. EasyChair (2012). https:/...

    2010 doi

  24. [32]

    In: Schneider, K., Brandt, J

    Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. p. 232–245. Springer (2007). https://doi.org/10.1007/978-3-540-74591-4_18

    2007 doi

  25. [33]

    Prieto-Cubides, J., Sicard-Ramírez, A.: Proof-reconstruction in type theory for propositional logic, https://raw.githubusercontent.com/jonaprieto/athena/master/ pubs/paper/paper.pdf

  26. [34]

    Roßkopf, S., Nipkow, T.: A formalization and proof checker for Isabelle’s metalogic. J. Autom. Reason.67(1), 1 (2023). https://doi.org/10.1007/s10817-022-09648-w 20 L. Bartl et al

    2023 doi

  27. [35]

    In: Galmiche, D., Schulz, S., Sebastiani, R

    Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 108–116. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_8

    2018 doi

  28. [36]

    AI Commun.25(1), 49–63 (2012)

    Sutcliffe, G.: The CADE-23 automated theorem proving system competition— CASC-23. AI Commun.25(1), 49–63 (2012). https://doi.org/10.3233/AIC-2012- 0512

    2012 doi

  29. [37]

    Turner, D.A.: A new implementation technique for applicative languages. Softw. Pract. Exper. 9(1), 31–49 (1979). https://doi.org/10.1002/spe.4380090105

    1979 doi

  30. [38]

    In: Platzer, A., Sutcliffe, G

    Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, vol. 12699, pp. 415–432. Springer (2021). https://doi.org/10. 1007/S10817-021-09613-Z

    2021

  31. [39]

    In: Sankaranarayanan, S., Sharygina, N

    Vukmirović, P., Blanchette, J., Schulz, S.: Extending a high-performance prover to higher-order logic. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, Part II. LNCS, vol. 13994, pp. 111–129. Springer (2023). https://doi.org/10.1007/ 978-3-031-30820-8_10

    2023

  32. [40]

    In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Théry, L

    Wenzel, M.: Isar—A generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Théry, L. (eds.) TPHOLs ’99. LNCS, vol. 1690, pp. 167–184. Springer (1999). https: //doi.org/10.1007/3-540-48256-3_12

    1999 doi

  33. [41]

    Wenzel, M.: Isabelle/Isar — A Versatile Environment for Human-Readable Formal Proof Documents. Ph.D. thesis, Institut für Informatik, Technische Universität München (2002), http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel. pdf

    2002

Pith tools

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