{"id":"a4f9c56b-6645-4aff-ad87-dccf3002d4b5","arxiv_id":"1908.09479","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"EKSTRAKTO reconstructs complete Dedukti proofs from E prover's TSTP traces by decomposing each trace into first-order subproblems and re-proving them with Dedukti-capable provers.","lead":"This paper presents EKSTRAKTO, a tool that takes proof traces from automated theorem provers and rebuilds them as complete, checkable proofs in the Dedukti logical framework. It increases the number of TPTP benchmark problems with Dedukti proofs from about a thousand to over three thousand.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Reconstruction produces Dedukti proof terms whose forall-instantiation and type-correctness are not demonstrated; running Dedukti on the 3,285 outputs would settle whether the central claim holds.","rationale":"The reader's verdict is CONDITIONAL, and I agree that full acceptance is not warranted. I focused on the proof-assembly step rather than on the logical-consequence assumption because the CNF restriction plus the future-work paragraph explicitly acknowledge Skolemisation and definitions, while the assembly step is claimed to work whenever all subproblems are proved. The gap is that Section 4.1 generates closed FOF subproblems by adding forall quantifiers over free variables, so each subproof term has a type whose outermost connective is Proof(forall ...). Section 4.2 invokes the rewrite rule for Proof(=>) to make this type convertible to a function, but the zen.lp excerpt in Section 3 only unfolds top-level implication; it cannot remove the forall connective. In the lambda-Pi-calculus modulo this encoding, a proof of a universally quantified formula is an opaque term unless additional forall-elimination constants or rewrite rules are supplied, and none are described. Therefore the sentence 'We just need to apply each proof term... by following the proof tree' skips the hardest part: instantiating the quantified variables with the substitution implicit in the TSTP inference. The empirical section reports only subproblem success; it never states that the assembled .lp files were run through Dedukti. Without that check, the counts of 2,189, 2,793, and 3,285 Dedukti proofs are not yet established. This does not prove the construction is wrong: an implementation could add the missing forall-elimination constants and then dkcheck all files, which is exactly the proposed test. I also note that the paper is honest about the scope of the extraction step in Section 6, so the main unresolved question is the typedness of the final reconstructed objects, not the intent of the authors.","tokens_in":7076,"tokens_out":7987,"duration_ms":88790,"concrete_test":"Run Dedukti's type checker on each of the 3,285 reconstructed proof files from the ZenonModulo union ArchSAT experiment (and on the 2,189 and 2,793 files from the other columns of Table 2) and report the number that type-check. Additionally, inspect the generated terms for a step like c_6 in Section 4.1: verify whether the subproof term is applied to hypotheses after an explicit forall-elimination or instantiation of the quantified variables. If no such instantiation exists, the term is ill-typed and the claimed counts overstate the number of Dedukti proofs; if all files type-check, the central claim is supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The strongest claim is that EKSTRAKTO 'reconstructs complete proofs in Dedukti', with 3,285 proofs in the union experiment. The load-bearing step is the composition in Section 4.2, and it is not shown to be well-typed. The extracted subproblems are closed FOF formulas with explicit universal quantifiers over the free variables of the CNF clauses (Section 4.1). Their Dedukti proof terms therefore have a type of the form Proof(forall x1...xn. A1 => ... => Ak => C). The only conversion rule displayed in Section 3 is 'Proof (=> a b) -> Proof a => Proof b'; there is no corresponding rule for 'Proof (forall a f)' and no described forall-elimination constant. Thus the application of a subproof term to the hypotheses is not definitionally justified: the outer forall must first be instantiated at the terms used in the TSTP inference, and the paper does not explain how this instantiation is performed. Moreover, the experiments count TSTP files for which every extracted subproblem was proved, but do not report running Dedukti's type checker on the 3,285 assembled files. A file whose final term is ill-typed is not a Dedukti proof. This is the weakest point because it directly affects the central claim, while the restriction to CNF and the future-work statement about Skolemisation in Section 6 are explicit limitations of the extraction step, not of the assembly step.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":7341,"tokens_out":9723,"duration_ms":100701,"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":[{"comment":"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.","section":"§5 (Tables 1 and 2)"},{"comment":"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.","section":"§4.2"},{"comment":"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.","section":"§2 and §6"}],"minor_comments":[{"comment":"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.","section":"§5, Table 2"},{"comment":"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.","section":"§4.1, c_5.p"},{"comment":"The prover named 'ZipperPosition' should be 'Zipperposition'.","section":"§1"}],"recommendation":"major_revision","confidential_remarks":"The missing Dedukti type-checking experiment is easy to fix and would directly address the central claim. If the authors can confirm that the assembled files were checked, or add that experiment, I would be willing to support acceptance of a revised version. The paper is appropriate for a workshop on proof exchange, and the reported numbers are promising."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a look if you work on proof exchange. EKSTRAKTO takes a TSTP trace, extracts each inference as a closed TPTP subproblem, re-proves those with ZenonModulo or ArchSAT, and assembles the results into a Dedukti file. The main contribution is that it gets there without trusting the original prover's inference names, so it is generic across provers. The empirical jump from 1,026 to 3,285 CNF problems with Dedukti proofs is real and useful; 72% of E prover's traces are covered by the union.\n\nWhat I like: the idea is simple and the implementation is open source. The paper is honest about the limits — Skolemisation and typed formulas are left to future work, and the authors note that ZenonModulo/ArchSAT fail on some easy steps for calculus reasons. That is the right framing for an extended abstract.\n\nThe soft spot is the assembly step, and it is load-bearing. The subproblems are closed formulas, with universal quantifiers over the free variables. So a sub-proof term has a type that begins with `Proof(forall x1...xn ....)` and, as written, Section 4.2 just displays the implication part and says the term can be applied to the premises. There is no conversion rule shown for `Proof (forall a f)` and no description of how the quantifiers are instantiated with the terms used in the original inference. If Dedukti's encoding in [1] has a rule like `Proof (forall a f) -> Π x:term a, Proof (f x)`, the paper should say so and explain the instantiation. Without it, the composition is not definitionally justified. On top of that, the experiments count files that were assembled, not files that Dedukti actually checked. Running Dedukti on the 3,285 outputs and reporting how many check would settle the central claim. That check is quick to do and should be standard before calling them proofs.\n\nThe citation pattern seems fine: the references are the relevant Dedukti/ZenonModulo/ArchSAT lineage, and the TPTP/TSTP standard. No signs of circularity.\n\nIf I were the editor at PxTP, I would send this to a referee. The core idea is sound and the missing items are addressable: add the forall-elimination rule or a reference to it, and add one line with the type-checker results. With those, the paper would be a solid contribution for the proof-exchange community.","headline":"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.","tokens_in":7913,"tokens_out":5865,"would_cite":true,"duration_ms":60554,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68T15"],"pacs":[],"model":"deepseek-v4-flash","headline":"A generic tool turns TSTP prover traces into complete Dedukti proofs, increasing the number of certified TPTP problems to 3285.","keywords":["proof reconstruction","Dedukti","TSTP","TPTP","proof checking","automated theorem proving","proof traces","lambda-Pi-calculus modulo rewriting"],"falsifier":"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.","tokens_in":6891,"feed_emoji":"🧾","tokens_out":5206,"duration_ms":48719,"temperature":0.7,"pith_summary":"EKSTRAKTO claims that a TSTP proof trace from any first-order prover can be turned into a complete Dedukti proof without understanding the prover's inference rules. The idea is to cut each trace into its individual inference steps, extract the leaf formulas that each step cites, and re-prove the resulting implication with a prover that emits Dedukti proofs, specifically ZenonModulo or ArchSAT. Because the extracted implications are pure first-order consequences of CNF formulas, a successful re-proof of every step composes into a full certificate. The paper reports that this raises the number of TPTP CNF problems with Dedukti proofs from 1026 with ZenonModulo alone to 3285 when both ZenonModulo and ArchSAT are used on E prover traces.","feed_headline":"3,285 TPTP problems now have Dedukti proofs","feed_subtitle":"A generic extractor re-proves each inference step of E prover TSTP traces with ZenonModulo or ArchSAT.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines Dedukti and the lambda-Pi-calculus modulo rewriting encoding of first-order formulas and proofs that the reconstructed proofs target.","marker":"[1]"},{"why":"Describes ZenonModulo, one of the two provers used to discharge the extracted subproblems with Dedukti proof output.","marker":"[5]"},{"why":"Describes ArchSAT, the other Dedukti-capable prover used for the same subproblem discharge.","marker":"[3]"},{"why":"Introduces E prover, the source of the TSTP traces used in the experiments.","marker":"[7]"},{"why":"Defines the TPTP problem library and TSTP trace format that the tool reads and processes.","marker":"[8]"},{"why":"Supports the motivation by showing Dedukti proofs can be translated to other proof assistants.","marker":"[10]"}],"fun_headline_variants":["Generic proof reconstruction: 3,285 TPTP problems in Dedukti","EKSTRAKTO: 3,285 Dedukti proofs from E prover traces","Black-box steps yield 3,285 Dedukti proofs","3,285 TPTP problems proven in Dedukti via generic extractor","Ekstrakto reconstructs Dedukti proofs for 3,285 TPTP problems"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Generic proof reconstruction: 3,285 TPTP problems in Dedukti","EKSTRAKTO: 3,285 Dedukti proofs from E prover traces","Black-box steps yield 3,285 Dedukti proofs","3,285 TPTP problems proven in Dedukti via generic extractor","Ekstrakto reconstructs Dedukti proofs for 3,285 TPTP problems"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000626,"raw_usage":{"total_tokens":2886,"prompt_tokens":925,"completion_tokens":1961,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":541,"completion_tokens_details":{"reasoning_tokens":1856}},"tokens_in":541,"tokens_out":1961,"duration_ms":12746,"temperature":1.0,"reasoning_tokens":1856,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:11:21.227057+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Available at http://www.lsv.fr/~dowek/Publi/expressing.pdf","cited_arxiv_id":null,"evidence_quote":"Defines Dedukti and the lambda-Pi-calculus modulo rewriting encoding of first-order formulas and proofs that the reconstructed proofs target."},{"cited_title":"Available at https://hal.archives-ouvertes.fr/hal-02083232","cited_arxiv_id":null,"evidence_quote":"Describes ArchSAT, the other Dedukti-capable prover used for the same subproblem discharge."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supports the motivation by showing Dedukti proofs can be translated to other proof assistants."}],"review_version":1}