REVIEW 3 major objections 3 minor 9 references
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
T0 review · 3 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read A generic tool turns TSTP prover traces into complete Dedukti proofs, increasing the number of certified TPTP problems to 3285.
desk verdict A genuinely useful proof-reconstruction pipeline with strong results, but the reported proof counts need a Dedukti type-check run and the forall handling in assembly is underspecified. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing object is the extraction function $P$, which maps a TSTP source to the set of leaf formulas that an inference step depends on, deliberately ignoring the inference rule name so that the method works for any prover. Each trace step becomes a separate TPTP FOF problem of the form $F_0 \Rightarrow \dots \Rightarrow F_k \Rightarrow F$, with free variables quantified. The composition works because in Dedukti's encoding the type of a proof of $A \Rightarrow B$ reduces to a function type from proofs of $A$ to proofs of $B$, so the proof terms returned for the subproblems can be applied one by one along the trace's proof tree. The restriction to CNF guarantees that every step is a purely logical consequence; Skolemisation and definitional steps are explicitly left out.
What would settle it
Feed EKSTRAKTO a TSTP file that contains a Skolemisation step, which the paper lists as unsupported future work, and observe that the extracted subproblem is not a first-order theorem and reconstruction fails. More sharply, produce any CNF trace whose recorded inference is not a pure first-order consequence of its leaves; if EKSTRAKTO still extracts a provable obligation or reconstructs a proof, the paper's implicit universality claim would be refuted, whereas a failure would confirm the CNF-only boundary.
Extended reading notes
Core claim
The central claim is that proof reconstruction can be made generic: instead of translating the original prover's inference rules, EKSTRAKTO treats each trace step as a black-box logical obligation. For a step with conclusion $F$ and leaf premises $F_0,\dots,F_k$, it forms the closed first-order formula $F_0 \Rightarrow \dots \Rightarrow F_k \Rightarrow F$ and asks a Dedukti-capable prover to prove it. In the experiments on the 4582 TSTP traces that E prover produced for the 7922 CNF problems of TPTP v7.2.0, this method yields 2189 complete Dedukti proofs with ZenonModulo, 2793 with ArchSAT, and 3285 using both, compared with 1026 for ZenonModulo alone and 500 for ArchSAT alone.
Load-bearing premise
Every inference step recorded in a CNF TSTP trace is a logical consequence in pure first-order logic of the leaf formulas it cites, so the extracted implication is always a theorem.
Editorial extensions
If this is right
- Every first-order prover that emits TSTP traces for CNF problems becomes a potential source of Dedukti-proof certificates, with no need to reimplement its calculus.
- The reconstructed proofs inherit Dedukti's portability: they can be translated to Coq, HOL, Lean, Matita, and PVS.
- The TPTP library gains 3285 known Dedukti proofs for CNF problems, more than tripling the 1026 obtainable with ZenonModulo alone.
- The certification rate is limited by the Dedukti-capable provers' ability to re-prove individual steps, so improvements to ZenonModulo or ArchSAT translate directly into more certified traces.
- The method applies only to CNF traces; extending it to handle Skolemisation would bring FOF traces into scope.
Reading between the lines
- The same extraction recipe could be applied to any trace format that records parent steps, not just TSTP, making it a general strategy for converting incomplete prover output into checked certificates.
- Because the generated subproblems are much smaller than the original problem, the main bottleneck is the Dedukti provers' calculus mismatch rather than logical hardness; a prover closer to superposition would likely push the yield well above 72 percent.
- A failed extraction on a successful trace would pinpoint a step that is not a pure first-order consequence, effectively letting the tool double as a validator of the trace itself.
- The per-step obligations could serve as a benchmark suite for Dedukti-capable provers, since each is a theorem whose difficulty is calibrated by a real prover trace.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. This extended abstract presents EKSTRAKTO, a tool that takes a TSTP proof trace produced by an automated theorem prover on a CNF TPTP problem, extracts for each inference step a closed FOF formula whose premises imply the step's conclusion, and calls an external Dedukti-capable prover (ZenonModulo or ArchSAT) to obtain a proof term for each subproblem. The tool then assembles these proof terms into a single Dedukti file by applying each subproof to the proofs of its premises. Experiments with E prover on 7,922 CNF problems yield 4,582 traces and 362,556 extracted subproblems; the union of ZenonModulo and ArchSAT solves 97% of the subproblems and 71–72% of the complete traces, giving 2,189, 2,793, and 3,285 reconstructed Dedukti proofs depending on the external prover used.
Significance. If the assembled files really are accepted by Dedukti, the result is significant: it gives a prover-calculus-independent route from E's TSTP traces to proof objects usable by multiple proof assistants, and it roughly triples the number of TPTP CNF problems for which Dedukti proofs are available compared with ZenonModulo alone. The paper's strengths are its concrete artifact, its large-scale experiment over the TPTP library, and its simple, clearly explained extraction scheme. The main weakness is that the empirical claim is measured by counting solved subproblems and not by checking the final assembled Dedukti files; without that check the central claim is not fully established.
major comments (3)
- [§5 (Tables 1 and 2)] The experiments count how many extracted TPTP subproblems are solved and how many TSTP files have all their subproblems solved, but they never report running Dedukti on the 2,189, 2,793, or 3,285 assembled files. Since the paper's central claim is that EKSTRAKTO 'reconstructs complete proofs in Dedukti', a generated file that fails Dedukti's type checker is not a proof. Please add a type-checking step and report the number of assembled files accepted by Dedukti, or explicitly state that the files were checked and by which version.
- [§4.2] The proof-reconstruction explanation uses only the rewrite rule for Proof (˙⇒ a b), while the generated subproblems are FOF formulas in which universal quantifiers occur inside the antecedent (see c_5.p). The paper does not state the Dedukti rule for Proof (˙∀ a f), nor does it show that the hypotheses in the final file are proofs of the universally quantified clauses rather than of the open CNF formulas. Please give the full set of rewrite rules for Proof over ˙∀ (and ˙∃ if relevant) and a typing derivation for one composition, e.g. c_5.delta hyp_c_0 hyp_c_1, so that the well-typedness of the assembly is checkable.
- [§2 and §6] The extraction of §4.1 assumes that every inference step in a CNF TSTP trace is a logical consequence of its leaves in pure first-order logic. The paper restricts to CNF and lists Skolemisation as future work, but it does not check or report whether E's traces contain other non-logical steps, such as definition introduction or splitting. Such steps would make the extracted FOF subproblem unprovable and would violate the claimed genericity with respect to the original prover's calculus. Please state how traces with such steps are detected and report their frequency, or qualify the genericity claim accordingly.
minor comments (3)
- [§5, Table 2] The prose says that the union succeeds on 72% of TSTP files, while Table 2 says 71%; since 3,285/4,582 ≈ 71.7%, the text should be 72% and the table should be corrected accordingly.
- [§4.1, c_5.p] In the displayed file c_5.p, the predicate 's' is used where the TSTP example defines 'subset'; this appears to be a typo that should be fixed to avoid confusion.
- [§1] The prover named 'ZipperPosition' should be 'Zipperposition'.
Circularity Check
No circular reasoning: EKSTRAKTO's reconstruction claims are empirically measured against the external TPTP library, not derived from its own assumptions.
full rationale
The paper's central claim is an empirical capability claim: from E prover TSTP traces on 7,922 TPTP CNF problems, EKSTRAKTO extracts 362,556 implication subproblems, calls ZenonModulo/ArchSAT on each, and counts how many TSTP files have all subproblems proved (2189/2793/3285). The success counts are measured outcomes, not consequences of the definitions. The extraction function P in Section 4.1 is purely syntactic (leaf premises of a trace), and the generated FOF subproblem is the implication from those premises to the conclusion; whether the external provers can prove it is an independent empirical fact. No parameter is fitted to the final counts, and no target result is assumed in defining the tool. The main self-references are citations to the Dedukti framework and to the encoding of first-order logic in Dedukti; these are context about the external proof checker, not premises that force the reported numbers. The paper's own limitation statements (CNF only, Skolemisation left for future work, and the lack of explicit forall-instantiation/type-checking detail in Section 4.2) are correctness risks rather than circularity: a type error in the assembled proof would make the claim false, not true by construction.
Assumptions & free parameters
assumptions (3)
- domain assumption Every inference step in the processed TSTP CNF traces is a first-order logical consequence of its leaf premises.
- domain assumption The Dedukti encoding from Section 3 supports the proof assembly in Section 4.2, including the handling of universal quantifiers when applying closed sub-proofs to open hypotheses.
- domain assumption ZenonModulo and ArchSAT produce correct Dedukti proof terms for the generated subproblems.
Cite this review
Pith. "Pith review of EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)." pith.science (2026). https://pith.science/paper/QE6AVOAJ
@misc{pith2026190809479,
author = {Pith},
title = {Pith review of: EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)},
year = {2026},
howpublished = {\url{https://pith.science/paper/QE6AVOAJ}},
note = {Machine review of arXiv:1908.09479}
}
read the original abstract
Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many details to build a complete proof. Hence these traces are hard to check and reuse in proof assistants. Dedukti is a proof checker whose proofs can be translated to various proof assistants: Coq, HOL, Lean, Matita, PVS. We implemented a tool that extracts TPTP subproblems from a TSTP file and reconstructs complete proofs in Dedukti using automated provers able to generate Dedukti proofs like ZenonModulo or ArchSAT. This tool is generic: it assumes nothing about the proof calculus of the prover producing the trace, and it can use different provers to produce the Dedukti proof. We applied our tool on traces produced by automated theorem provers on the CNF problems of the TPTP library and we were able to reconstruct a proof for a large proportion of them, significantly increasing the number of Dedukti proofs that could be obtained for those problems.
Reference graph
Works this paper leans on
-
[1]
Available at http://www.lsv.fr/~dowek/Publi/expressing.pdf
Ali Assaf, Guillaume Burel, Rapha ¨el Cauderlier, Gilles Dowek, Catherine Dubois, Fr ´ed´eric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard: Dedukti: a Logical Framework based on the λ Π-Calculus Modulo Theory. Available at http://www.lsv.fr/~dowek/Publi/expressing.pdf
-
[2]
Richard Bonichon, David Delahaye & Damien Doligez (2007): Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings , pp. 151–165, doi:10.1007/978-3-540-75560-9 13
-
[3]
Available at https://hal.archives-ouvertes.fr/hal-02083232
Guillaume Bury, Simon Cruanes & David Delahaye (2018): SMT Solving Modulo Tableau and Rewriting Theories. Available at https://hal.archives-ouvertes.fr/hal-02083232
work page 2018
-
[4]
Simon Cruanes (2015): Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond . Theses, ´Ecole polytechnique. Available at https://hal.archives-ouvertes.fr/tel-01223502
work page 2015
-
[6]
Available at http://www.lsv.fr/~dowek/Publi/skolem.pdf
Gilles Dowek & Benjamin Werner: A constructive proof of Skolem theorem for constructive logic . Available at http://www.lsv.fr/~dowek/Publi/skolem.pdf
-
[7]
In Ken McMillan, Aart Middeldorp & Andrei V oronkov, editors: Proc
Stephan Schulz (2013): System Description: E 1.8 . In Ken McMillan, Aart Middeldorp & Andrei V oronkov, editors: Proc. of the 19th LPAR, Stellenbosch, LNCS 8312, Springer, doi:10.1007/978-3-642-45221-5 49
-
[8]
Sutcliffe (2017): The TPTP Problem Library and Associated Infrastructure
G. Sutcliffe (2017): The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), pp. 483–502, doi:10.1007/s10817-017-9407-7
-
[9]
Geoff Sutcliffe (2018): The 9th IJCAR Automated Theorem Proving System Competition - CASC-J9 . AI Commun. 31(6), pp. 495–507, doi:10.3233/AIC-180773
Show all 9 references
-
[10]
Franc ¸ois Thir´e (2018): Sharing a Library between Proof Assistants: Reaching out to the HOL Family . In Fr ´ed´eric Blanqui & Giselle Reis, editors: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018,...
2018 doi
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.