{"id":"63576013-d35d-4647-9f14-303e553543fd","arxiv_id":"2507.11349","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper specifies SC-TPTP, a TPTP-compatible derivation format for sequent calculus proofs, with tools for checking proofs, unfolding high-level steps, and exporting them to Coq.","lead":"SC-TPTP is a proposed file format for recording proofs made by sequent-based theorem provers, built as an extension of the existing TPTP standard. It is meant to let interactive proof assistants such as Lisa call automated provers like Goéland and then import, check, and even translate the resulting proofs into Coq.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Coq export is not shown to be a faithful translation: §4.1 gives only per-rule lemmas, the Drinker theorem is stated as `~~F` not `F`, and no mapping from arbitrary SC-TPTP sequents/proofs to Coq propositions is specified. Until this is fixed, the export-to-Coq contribution is unverified.","rationale":"The reader's weakest assumption targets the soundness of the Coq export, and the full text supports that concern. The paper gives only a few illustrative lemmas, and the one complete Coq proof shown proves a double-negated statement rather than the original conjecture. No compositional translation is specified for the general case, including cuts, weakening, and multi-formula succedents, and the dependence on classical principles is not declared. This is load-bearing because one of the four headline contributions is exporting SC-TPTP proofs to Coq; if the exported theorem is not the original statement, the interoperability pipeline from Goéland through SC-TPTP to Coq is not delivered even though the SC-TPTP format itself may be sound and precisely checkable. The concern is concrete and testable, but it does not invalidate the format-level claims: the rule tables are standard, the implementation is public, the Goéland/Lisa integration is a real proof of concept, and the congruence-unfolding algorithm is a substantive contribution. The appropriate verdict remains CONDITIONAL: the paper should be accepted only after the Coq translation is either fixed to end in the original formula or accompanied by an explicit, verified statement of what it proves.","tokens_in":15825,"tokens_out":25934,"duration_ms":313949,"concrete_test":"Run the published library's Coq exporter on the Drinker SC-TPTP proof from Example 3.2 and on one additional proof that uses `rightOr` and `cut`; compile the results with `coqc` and inspect the final theorem statements. The test passes only if, after importing exactly the lemmas in SC-TPTP.v (plus a declared classical axiom if used), the final Coq theorem is the original conjecture (for Drinker: `exists X, d X -> forall Y, d Y`), not its double negation. If the generated statement is `~~F` or requires an undocumented axiom, the §4.1 mapping is not faithful.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Load-bearing concern (Section 4.1, Examples 4.2/4.5): the paper claims a 'one-to-one mapping' between SC-TPTP rules and Coq lemmas, but no translation function is defined on arbitrary sequents and proofs. The displayed lemmas are not the direct sequent rules: rightOr is encoded as `~(~P /\\ ~Q) -> P \\/ Q`, and left rules require separate `_s` inversion lemmas with 'holes' that are not specified compositionally. More concretely, Example 4.5's `Theorem drinker` is `~(~(exists X, d X -> forall Y, d Y))`; the original SC-TPTP conjecture is the positive formula (Example 3.2). Coq's logic does not identify `~~F` with `F` without an explicit classical axiom, and the paper does not state what classical axioms (`NNPP`, `classic`) the exported files depend on, nor how cuts or multi-formula succedents are represented. If the exporter silently proves double-negated or otherwise rearranged statements, the 'export them into Coq files' contribution fails even though the SC-TPTP format itself may be sound. A soundness statement for the translation is entirely absent: no theorem, no Coq-checked correspondence, no class of sequents covered.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes SC-TPTP, an extension of the TPTP derivation format intended for sequent-based first-order logic proofs. It defines two levels of derivation steps: 30 level-1 rules (structural, left/right introduction, left-negation, and equality rules) and three level-2 steps (NNF, congruence, and simultaneous substitution), with sequents interpreted as sets of formulas. The paper also describes a Scala library that parses, prints, checks, unfolds congruence steps, and exports proofs to Coq, together with an integration in which the Lisa proof assistant queries the Goéland ATP and imports SC-TPTP proofs. The central claims are that the format is precise, mechanically checkable, and interoperable, and that the provided tools realize these properties.","tokens_in":16099,"tokens_out":8368,"duration_ms":101568,"significance":"The proposal addresses a real interoperability need and has the virtue of building on the widely used TPTP syntax. The set-based semantics and explicit per-rule parameters simplify checking, and the public implementation, the proof-producing e-graph, and the working Lisa--Goéland integration are concrete artifacts that give the paper practical weight. If the soundness gaps identified below are resolved, SC-TPTP could become a useful common format for exchanging first-order sequent proofs. The level-1 rule set is standard, but the paper currently lacks the formal translation and soundness theorems needed to substantiate the Coq-export contribution and to guarantee that the format itself is sound as specified.","major_comments":[{"comment":"The Coq export is not defined as a translation on arbitrary SC-TPTP sequents and proofs. The displayed `Theorem drinker` proves `~(~(exists X, d X -> forall Y, d Y))`, while the original SC-TPTP conjecture in Example 3.2 is the positive formula `(? [X] : d(X) => (! [Y] : d(Y)))`. The paper does not state that exported proofs concern double-negated statements, does not list the classical axioms (e.g., `NNPP`, `classic`) on which the generated Coq scripts depend, and does not explain how multi-formula succedents, `cut`, or the `_s` inversion lemmas are composed into a full proof translation. Without a soundness statement relating SC-TPTP provability to Coq provability under the described translation, the contribution \"export them into Coq files\" is unverified.","section":"Section 4.1, Examples 4.1-4.5"},{"comment":"The `leftEx` and `leftNotAll` rules omit the eigenvariable (freshness) side condition. In standard LK, the rule `Γ, A(y) ⊢ Δ ⇒ Γ, ∃x.A(x) ⊢ Δ` is sound only when `y` does not occur free in `Γ, Δ`; the same freshness condition is required for `leftNotAll`. The surrounding text in Section 3.2 mentions a freshness check only for `rightAll` (step s3), so a checker implementing the tables literally would accept unsound derivations. This is a soundness gap in the proposed format itself and must be fixed in the rule definitions and in the checker.","section":"Section 3.2, Tables 2 and 4"},{"comment":"The e-graph-based unfolding of `congruence` steps is described only informally. No theorem states that the `explain` method always terminates, that the returned equality path is acyclic, or that its recursive expansion produces a valid sequence of level-1 `leftSubst`/`rightSubst` steps preserving the original sequent. Since eliminating level-2 steps in favor of low-level steps is a stated contribution, the unfolding procedure needs a precise correctness invariant and a proof that the constructed level-1 proof is well-formed.","section":"Section 4.2"}],"minor_comments":[{"comment":"The parameter descriptions for `leftNotEx` and `leftNotAll` say the index points to the formula \"on the right\" of the conclusion; both rules are left-introduction rules, so this should read \"on the left\".","section":"Table 4"},{"comment":"Example 3.2 uses the rule name `leftNotForall`, while Table 4 names the same rule `leftNotAll`. The names should be harmonized and the example should parse against the published rule set.","section":"Example 3.2 vs. Table 4"},{"comment":"The `leftSubst` derivation example appears to refer to `s1` as its own premise and contains a malformed parameter list (an extra closing parenthesis after `$fot(Z))`). It should refer to the axiom `a1` and use correct SC-TPTP syntax.","section":"Section 3.2, leftSubst example"},{"comment":"The statement that the 30 rules are \"complete for first order logic with equality\" is asserted without proof or citation; since the paper is primarily about a format rather than a new calculus, this claim should be backed by a reference or softened to \"complete for the usual LK-style presentation\".","section":"Section 3.2, completeness claim"}],"recommendation":"major_revision","confidential_remarks":"The paper is a well-motivated proposal with concrete artifacts, but the Coq export lacks a formal translation and soundness theorem, and the missing eigenvariable conditions in `leftEx`/`leftNotAll` are a correctness bug in the format itself. These are fixable within the manuscript's scope, but they are load-bearing for the main claims. The paper may be better suited to a systems or workshop venue; for a journal, the soundness gaps should be closed and the format's rule definitions made fully rigorous."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nSC-TPTP is a genuine, useful artifact: a TPTP over-specification for sequent-calculus derivations, with 30 low-level rules, set semantics, explicit parameters, and a working parser and checker. The paper also ships an egraph-based unrolling of congruence closure and a Goéland-Lisa integration that lets Lisa call Goéland and get back checkable proofs. That is real work, clearly described. The low-level rule set is defensible: verification conditions for each step are spelled out and are linear-time checkable, apart from a benign alpha-equivalence cost. The related-work discussion (TESC, connection-calculus syntax, LFSC, Alethe) is honest and positions the proposal well.\n\nThe soft spots are in the Coq export. The paper claims a one-to-one mapping between SC-TPTP rules and Coq lemmas, but no translation function on arbitrary sequents and proofs is defined. The displayed lemmas do not directly match the sequent rules: rightOr is encoded as `~(~P /\\ ~Q) -> P \\/ Q`, left rules require ad hoc `_s` inversion lemmas, and Example 4.5's `Theorem drinker` is `~~(...)` rather than the original conjecture. No soundness theorem is given, no class of covered sequents is stated, and the dependence on classical axioms (NNPP) is implicit. Until that is pinned down, the export-to-Coq contribution is unverified, even though the SC-TPTP format itself may be fine.\n\nTwo smaller points: completeness of the 30 rules for first-order logic with equality is asserted without proof, and there are minor syntactic inconsistencies in the rule tables and examples. Neither is load-bearing; the format can be adopted without a completeness theorem, but a precise statement would help.\n\nNet: this is a worthwhile proposal for proof interoperability, and people building proof-exchange or ATP/ITP bridges will get value from it. It deserves a serious referee. The format and the Lisa/Goéland integration are solid enough to review and revise. The Coq export needs either a real soundness argument or a demotion to “experimental.”","headline":"SC-TPTP is a sensible, well-scoped proposal for a sequent-proof interchange format; the format deserves referee time, but the Coq export is not yet shown sound.","tokens_in":16630,"tokens_out":2833,"would_cite":true,"duration_ms":31821,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68V15"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper specifies SC-TPTP, an extension of the TPTP derivation format that makes sequent-calculus proofs from automated provers mechanically checkable and exportable to Coq.","keywords":["TPTP","sequent calculus","proof format","proof interoperability","automated theorem proving","interactive theorem proving","congruence closure","Coq export"],"falsifier":"A concrete test is to run the library's Coq export on level 1 SC-TPTP proofs of classically valid but intuitionistically invalid sequents such as Peirce's formula and check whether the generated theorem, after stripping the double-negation encoding, is provably equivalent to the original sequent for every rule; the paper's own displayed Drinker theorem is double-negated, so the soundness of that encoding for general proofs is the crux.","tokens_in":15567,"feed_emoji":"📜","tokens_out":8753,"duration_ms":92444,"temperature":0.7,"pith_summary":"The paper claims that a common derivation format for sequent-based proofs can be built by over-specifying the existing TPTP derivation format, fixing what TPTP leaves open: how each proof step was derived. SC-TPTP defines two levels of steps, thirty low-level sequent-calculus rules that are complete for first-order logic with equality and easy to verify, plus higher-level steps such as congruence closure that come with procedures to unfold them into low-level steps. The authors implement a library that parses, prints, checks, and transforms SC-TPTP proofs, exports them to Coq, and wire the format into the Lisa proof assistant and the Goéland automated prover. If the format is sound and adopted, proof exchange between sequent-based systems becomes a matter of one import and one export per tool, and ATP answers become unambiguously verifiable.","feed_headline":"SC-TPTP gives theorem provers one checkable proof format","feed_subtitle":"Interactive provers can call Goéland, verify the returned sequent proof, and export it to Coq through one format.","key_machinery":"The machinery is the two-level derivation-step system. Level 1 is a fixed set of thirty rules whose parameters are indices into the sequent, so checking a step reduces to comparing sets of formulas, and level 2 is an extensible set of advanced steps for which an elimination algorithm produces a level 1 derivation. The proof-producing e-graph, an equivalence-class data structure for terms under equalities and congruence, is the object that turns a congruence-closure justification into explicit equality edges and, recursively, into substitution proofs.","core_discovery":"The central claim is that a proof format can be faithful to mathematical tradition and still mechanically checkable if it pins down the meaning of every derivation step. SC-TPTP derivations are lists of TPTP-annotated statements whose formulas may be sequents, and each inference names a rule from a fixed table together with parameters, mostly indices, that make verification a set-comparison check rather than a search. Level 1 rules cover structural rules, left and right introduction of connectives and quantifiers, negated forms, and equality; level 2 rules, here negation normal form, simultaneous substitution, and congruence, are justified by elimination algorithms that unfold them into level 1 derivations. The implemented pipeline lets Lisa pose a conjecture, have Goéland return an SC-TPTP proof, check it, unfold congruence steps using an e-graph with an explain method, and export the result to Coq.","pith_inferences":["Beyond the paper, the same two-level design would likely extend to typed first-order logic: adding types to the rule parameters would make some checks more involved but would not change the set-comparison principle.","Beyond the paper, the Coq export could be turned into a fully verified translation by mechanically proving that the double-negation and inversion lemmas used for right and left rules are logically equivalent to the original sequent rules.","Beyond the paper, adding deskolemization as a level 2 step, as the conclusion suggests, would allow tableaux proofs with on-the-fly Skolem terms to be unfolded into level 1 derivations and would remove a major obstacle to importing such proofs.","Beyond the paper, the DRAT experience in SAT suggests that the main barrier for SC-TPTP is adoption rather than expressiveness, so an independent lightweight checker built by a third party would be a natural next step to build trust in the format."],"forward_implications":["If SC-TPTP is adopted, every sequent-based tool needs only one SC-TPTP import and one export, replacing pairwise translation between every pair of systems.","Automated theorem prover answers for first-order problems can be verified unambiguously, since each step carries enough parameters to be checked without inference.","Users of Lisa can call Goéland as a proof-producing tactic and obtain proofs that are reconstructed inside Lisa's kernel.","Sequent-style proofs can be exported to Coq, and level 2 steps such as congruence can be eliminated into level 1 steps, making advanced ATP reasoning digestible for proof assistants.","The format is extensible by design: level 2 rules such as NNF are anticipated, so tools can keep their native high-level steps and eliminate only what their target cannot consume."],"supporting_citations":[{"why":"It defines the TPTP logic language and derivation annotations that SC-TPTP over-specifies for sequent calculi.","marker":"[1]"},{"why":"It supplies the TPTP problem library and TSTP solutions that motivate a derivation format with explicit inference steps.","marker":"[7]"},{"why":"It describes the Lisa proof assistant whose sequent-calculus kernel is the target for importing SC-TPTP proofs.","marker":"[2]"},{"why":"It describes the Goéland tableau prover whose rigid e-unification steps become congruence steps in SC-TPTP.","marker":"[3]"},{"why":"It provides the e-graph data structure used to compute congruence closure while producing explicit proofs.","marker":"[27]"},{"why":"It provides the proof-producing congruence closure explain method that the unfolding algorithm uses to justify equality edges.","marker":"[41]"}],"fun_headline_variants":["SC-TPTP: one checkable format for sequent proofs","Checkable sequent proofs link ATPs to ITPs","Sequent calculus proofs, verified and exported","From Goéland to Coq via checkable sequent proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing assumption is that the Coq translation is sound: every SC-TPTP rule, including the double-negated and inverted versions used because Coq is intuitionistic, is faithfully represented by the supplied Coq lemmas, so a Coq-accepted proof really proves the original sequent.","fun_headline_variants_meta":{"raw":{"variants":["SC-TPTP: one checkable format for sequent proofs","Checkable sequent proofs link ATPs to ITPs","Sequent calculus proofs, verified and exported","From Goéland to Coq via checkable sequent proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000283,"raw_usage":{"total_tokens":1640,"prompt_tokens":881,"completion_tokens":759,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":497,"completion_tokens_details":{"reasoning_tokens":691}},"tokens_in":497,"tokens_out":759,"duration_ms":8446,"temperature":1.0,"reasoning_tokens":691,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T17:10:25.130120+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete test is to run the library's Coq export on level 1 SC-TPTP proofs of classically valid but intuitionistically invalid sequents such as Peirce's formula and check whether the generated theorem, after stripping the double-negation encoding, is provably equivalent to the original sequent for every rule; the paper's own displayed Drinker theorem is double-negated, so the soundness of that encoding for general proofs is the crux.","supporting_citations":[],"review_version":1}