{"id":"3f2a12d6-c2d7-4fa1-9de3-92b9af191e62","arxiv_id":"2506.00163","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new algorithm (WSCAN) extracts a witness from a terminating SCAN derivation, and guarantees the witness is first-order when the derivation is one-sided.","lead":"The paper extends the SCAN algorithm for second-order quantifier elimination to also produce an explicit witness, a concrete substitution for the eliminated predicate that preserves logical equivalence. This makes SCAN applicable to formula equations, forgetting, and verification, and the authors provide a prototype in the GAPT framework.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 25's proof silently assumes the PurDel side condition is closed under further resolution with P; Definition 2 only guarantees one-step resolvents are redundant, so Theorem 15's witness-preservation step is not established as written.","rationale":"The reader's weakest-assumption pinpoints the same place: the proof of Lemma 25 moves from one-step PurDel redundancy to redundancy of the full resolution closure ResP(N'). My independent check of Appendix B confirms that Definition 2 literally states only one-step redundancy and that the proof's next sentence asserts the stronger closure property without proof. The concrete instance above shows that the stronger property is not a logical consequence of the stated redundancy axioms, so the gap is real and not merely cosmetic. This concern is load-bearing because Lemma 25 is the key ingredient in the inductive proof of Theorem 15 (Lemma 6, then Theorem 15), and Theorem 15 is the paper's main result. If the closure step cannot be justified, the witness construction may fail to produce a witness even when SCAN terminates; the advertised correctness guarantee is therefore unproven. The paper may well be repairable — for example by strengthening Definition 2 to require redundancy of all clauses in ResP(N'), or by adding a closure property for redundancy criteria — and standard SCAN implementations often satisfy such a property, but the extended preprint does not state it. The prototype implementation is a real asset but it only demonstrates that the construction runs on 21 examples; it does not validate the general theorem. The abstract's imprecise promise of first-order witnesses is a secondary issue; the proof gap in Lemma 25 is the single most load-bearing concern. Since the identified gap supports the reader's CONDITIONAL verdict rather than overturning it, my recommendation is UNCHANGED.","tokens_in":28938,"tokens_out":19243,"duration_ms":232852,"concrete_test":"Formalize Definition 2, Definition 7, and Lemma 25 in Isabelle/HOL, treating redundancy as an arbitrary predicate satisfying only properties (i) and (ii) from Section 3. Use the model finder to search for a finite PurDel configuration (small P and N' over one or two constants) that satisfies the one-step redundancy side condition while falsifying N' ⇛ C[X←pResUP] for some C in N'. Start with the concrete P and N' given above, then generalize to longer resolution chains. If a falsifying model is found, Theorem 15 fails as stated; if exhaustive search finds none, attempt an automated proof of Lemma 25 and record which additional closure axiom the proof requires.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 15, and it rests on Lemma 25. In the proof of Lemma 25 (Appendix B), the sentence \"Since P is purified in N' we have that ResP(N') is redundant in N'\" is not a consequence of Definition 2's PurDel rule. Definition 2 requires only that every one-step resolvent of P with a clause of N' be redundant in N'. But ResP(N') (Definition 7) is the closure under repeated resolution with P; its members can be obtained by resolving P with clauses that are themselves resolvents and need not belong to N'. The redundancy axioms stated in Section 3 — entailment compatibility (i) and equivalence preservation (ii) — do not imply that a resolvent of a redundant clause with P is redundant. Standard saturation redundancy criteria have such a closure property, but it is neither stated nor used. Without it, the step N' ⇛ ResP(C), needed to apply Lemma 11, is unjustified. The gap is concrete: let P = X(a)∨A and N' = {¬X(a)∨¬X(b)∨B, X(a)∨A∨B}. The one-step resolvent ¬X(b)∨B∨A is entailed by N', so the PurDel side condition holds, but the two-step closure contains b≃a∨B∨A, which is not entailed by N' (take X(a)=true, X(b)=false, A=false, B=false, a≠b). Thus closure redundancy fails under the stated assumptions. This does not by itself disprove Theorem 15, since the transformation lemma might still hold for another reason, but it invalidates the given proof and leaves the main theorem conditional on an unstated closure property.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces the problem of witnessed second-order quantifier elimination (WSOQE): given a formula ∃X φ with first-order φ, find a tuple α of predicate expressions such that ∃X φ ≡ φ[X←α]. The authors extend the SCAN algorithm to a new algorithm WSCAN, which uses a recorded SCAN derivation to construct such a witness in a bottom-up manner. The main result, Theorem 15, asserts that every X-eliminating C-derivation from N yields a witness wit(D) for ∃X N. The paper also gives sufficient conditions, one-sidedness, for the witness to be first-order (Corollary 20), discusses connections to formula equations and Ackermann's Lemma, and reports a prototype implementation in GAPT 2.18.1.","tokens_in":29269,"tokens_out":24845,"duration_ms":260837,"significance":"If Theorem 15 were correct, the paper would make a useful conceptual contribution: it connects second-order quantifier elimination with the older problem of solving formula equations, and the idea of extracting witnesses from a recorded saturation derivation is attractive. The appended proofs are detailed and the paper is generally well written. However, the central correctness claim is false as stated: I give a concrete, small counterexample in which the PurDel step is applicable, the derivation is X-eliminating, and the witness computed by Definition 14 is not a WSOQE-witness. Since the main theorem is unsound, the algorithm, its corollaries, and the implementation claims are not supported. The failure is load-bearing and cannot be repaired by local proof patching: the PurDel transformation itself is invalid.","major_comments":[{"comment":"Theorem 15 is false. Consider the clause set N0 = {X(a)∨A, ¬X(a)∨¬X(b)∨B, ¬X(b)∨B}, with P = X(a)∨A as the pointed clause. The PurDel_P step from N0 to N′ = {¬X(a)∨¬X(b)∨B, ¬X(b)∨B} is valid under Definition 2: the only resolvent of P with a clause of N′ is A∨¬X(b)∨B (after constraint elimination), which is subsumed by the clause ¬X(b)∨B and hence redundant in N′. All X-literals in N′ are negative, so ExtPurDel−_X is applicable, giving an X-eliminating C-derivation D from N0 to ∅. Following Definition 14, wit(D) is λu.¬A: the ExtPurDel−_X step sets the witness to λu.⊥, and the PurDel_P step transforms it to pResU_P[X←λu.⊥] = λu.¬A. However, ∃X N0 is logically equivalent to A∨B∨(a̸≃b): if a≠b, choose X(a)=true and X(b)=false; if A holds, choose X(a)=true; if B holds, choose X(a)=true for any X(b). Substituting λu.¬A for X turns N0 into (¬A∨A) ∧ (¬¬A∨¬¬A∨B) ∧ (¬¬A∨B), which simplifies to A∨B. This is not equivalent to A∨B∨(a̸≃b); in a model with a≠b, A=false, B=false, the former is false and the latter is true. Thus wit(D) is not a witness for ∃X N0, contradicting Theorem 15.","section":"Appendix B, Lemma 25 and Lemma 6; Section 4, Theorem 15"},{"comment":"The proof of Lemma 25 contains the unjustified assertion: 'Since P is purified in N′ we have that ResP(N′) is redundant in N′'. Definition 2 only requires every one-step resolvent of P with a clause from N′ to be redundant in N′. It does not require, and in general does not imply, that the full resolution closure ResP(N′) is redundant. In the counterexample above, the closure contains the clause a̸≃b∨B∨A, obtained by resolving P with the one-step resolvent A∨¬X(b)∨B. That clause is not entailed by N′: taking a≠b, A=false, B=false, X(b)=false satisfies both clauses of N′ but falsifies a̸≃b∨B∨A. Hence the closure redundancy used in the proof fails. Since Lemma 25 is the central device by which Lemma 6 and Theorem 15 are derived, the main proof is unsound.","section":"Appendix B, Lemma 25 proof; Definition 2 vs. Definition 7"}],"minor_comments":[{"comment":"In the paragraph explaining ExtPurDel^+_X and ExtPurDel^−_X, the sentence 'setting the X-component of TS(α) to X to λu.⊥' contains a typo; it should read 'to λu.⊥'.","section":"Section 4, text after Lemma 6"},{"comment":"The notation is inconsistent: ResU_P(C) and ResUP(C) are used interchangeably, and some occurrences of 'ResUP' should be 'Res_P'. This makes the otherwise detailed proofs harder to follow.","section":"Appendix B, Lemma 27 and surrounding text"},{"comment":"The example showing that no WSOQE-witness exists in the input language for Φ = ∃X∃u∃v(X(u)∧¬X(v)) is correct and instructive; however, its conclusion is presented as a limitation of the method rather than as a consequence of the semantics, which is worth clarifying.","section":"Section 7, 'Limitations for finding witnesses'"},{"comment":"The recurrence for the lower bound uses the notation w_i for |wit_i(D_{p,n})|, but the indexing is off by one relative to the definition of w_i in the preceding paragraph; the intended asymptotic bounds are clear, but the indices should be fixed.","section":"Section 5, proof of Proposition 32"}],"recommendation":"reject","confidential_remarks":"The counterexample in my first major comment is small and easily machine-checked; it refutes the main theorem, not merely a proof detail. I therefore recommend rejection. The paper's general idea is interesting, but the PurDel witness transformation is unsound as defined, and repairing it would require changing either the side condition of Definition 2 or the witness transformation, with corresponding re-proofs of the main results."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Sebastian — quick take on 2506.00163. The paper is worth reading and, I think, worth refereeing, but the main theorem isn't actually proved as written. The WSCAN idea is nice: run SCAN, record the derivation, then reconstruct a witness for the eliminated predicate variables by stepping backwards. The connection to formula equations and to Wernhard's ELIM-witnesses is drawn carefully, and the appendix is serious about the details. I also like that they ship a prototype in GAPT and show multiple non-equivalent witnesses for the same input.\n\nThe soft spot is Lemma 25, the transformation lemma. In the PurDel case the proof says that since P is purified in N', the whole closure ResP(N') is redundant in N'. But Definition 2 only requires every one-step resolvent of P with a clause from N' to be redundant. Redundancy as defined (entailment compatibility plus equivalence preservation) does not give you closure under further resolution with P, and that step is load-bearing. The stress-test example claiming to show a concrete failure of closure doesn't quite work—the closure only resolves on the designated literal of P, so the alleged two-step resolvent isn't actually generated—but the general concern holds. The proof needs either a stronger redundancy property or a different argument. This makes Theorem 15 conditional, not false.\n\nAlso, the abstract says the algorithm finds an instance of the quantifiers that results in an equivalent first-order formula, but the witness is only guaranteed first-order under the one-sidedness condition; in general it can be infinite. That's a minor overclaim, but it should be fixed.\n\nThe evaluation is small (26 examples, no comparison), and the authors admit that. For a paper whose main value is a new algorithm, that's acceptable for a conference version but wouldn't carry a journal version on its own.\n\nMy call: send it to peer review. The idea is novel, the writing is clear, and the gap looks repairable. A serious referee should ask for a corrected proof of Lemma 25, or a statement of the redundancy condition that actually implies the needed closure. I wouldn't cite it as a proved result yet, but I'd gladly discuss it in a reading group.","headline":"WSCAN is a genuinely new idea with a clear write-up, but the main theorem's proof has a load-bearing gap in Lemma 25, so the paper needs fixing before it can be trusted.","tokens_in":29798,"tokens_out":5519,"would_cite":false,"duration_ms":59501,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B15","03B35","68T15"],"pacs":[],"model":"deepseek-v4-flash","headline":"SCAN can be extended to compute explicit first-order witnesses for eliminated second-order quantifiers.","keywords":["second-order quantifier elimination","SCAN algorithm","formula equations","saturation theorem proving","witness construction","first-order witness","one-sided derivations","predicate elimination"],"falsifier":"Find a clause set $N$, a pointed clause $P$, and a redundancy criterion satisfying the paper's two conditions (entailment-compatible and equivalence-preserving) such that every one-step resolvent of $P$ with $N$ is redundant in $N$ but some iterated resolvent in $\\mathrm{Res}_P(N)$ is not entailed by $N$; such a counterexample would break the transformation lemma and with it the main theorem.","tokens_in":28710,"feed_emoji":"⚙️","tokens_out":7383,"duration_ms":84406,"temperature":0.7,"pith_summary":"Second-order quantifier elimination asks for a first-order formula equivalent to a quantified formula such as $\\exists X \\varphi$. This paper tackles a stronger problem: finding an actual first-order predicate expression $\\alpha$ that can be substituted for $X$ so that $\\exists X \\varphi \\equiv \\varphi[X \\leftarrow \\alpha]$. The authors show that every terminating run of the SCAN algorithm records enough information, if remembered as a derivation, to reconstruct such a witness by walking backwards through the derivation. This matters because witnessed second-order quantifier elimination sits between ordinary elimination and solving formula equations, and a witness can be used for forgetting, interpolation, and verification without rebuilding the formula from scratch.","feed_headline":"WSCAN turns terminating SCAN runs into witness formulas","feed_subtitle":"Eliminating an existential predicate now returns a concrete replacement formula, not just an equivalent clause set.","key_machinery":"The load-bearing object is the predicate expression $p\\mathrm{Res}^U_P$, defined for a pointed clause $P$ as follows: take the unit clause dual to $P$'s designated literal, close it under repeated constraint resolution with $P$, and convert the resulting (possibly infinite) clause set into a $\\lambda$-predicate by conjoining or disjoining the clauses. The witness preservation lemma shows that replacing a witness for the clause set after a derivation step with $p\\mathrm{Res}^U_P[X \\leftarrow \\alpha]$ yields a witness for the clause set before the step, which is what lets the algorithm walk backwards through the recorded SCAN run.","core_discovery":"The paper defines WSCAN, an extension of the SCAN algorithm on clause sets. Given an $X$-eliminating derivation $D$ from a clause set $N$, i.e., a recorded saturation run whose final clause set contains no predicate variables from $X$, the construction $\\mathrm{wit}(D)$ yields a tuple of predicate expressions satisfying $\\exists X N \\equiv N[X \\leftarrow \\mathrm{wit}(D)]$. The construction is bottom-up: it starts from a trivial witness at the final clause set and, for each derivation step $S$ read backwards, applies a transformation $T_S$ to the current witness; for a purified clause deletion step, the component for the deleted predicate variable becomes $p\\mathrm{Res}^U_P[X \\leftarrow \\alpha]$, built from the resolution closure of the deleted pointed clause $P$ against the unit clause dual to its designated literal. If every purified clause in $D$ is one-sided, meaning the eliminated predicate occurs with only one polarity, then $\\mathrm{wit}(D)$ is a first-order predicate. The same machinery supplies a new correctness proof for SCAN itself.","pith_inferences":["Editorial: The infinite witnesses that arise when a purified clause is not one-sided suggest a fixpoint extension: infinite $p\\mathrm{Res}^U_P$ expressions often encode least or greatest fixpoints, and adding a fixpoint constructor to the witness language could make WSCAN succeed in cases where first-order witnesses provably do not exist.","Editorial: Since different choices of pointed clauses in the saturation loop give different, incomparable witnesses, the procedure could be used to generate candidate loop invariants in Horn-clause verification by running the saturation with varied strategies.","Editorial: The Skolem-constant example indicates a testable extension: integrating reverse Skolemization would let WSCAN detect when a witness exists only in an expanded signature and report the minimal signature extension required."],"forward_implications":["If SCAN terminates on a clause set and the recorded derivation is one-sided, the algorithm outputs a first-order witness formula, not merely an equivalent clause set.","Feeding a computed witness to a first-order theorem prover decides the corresponding formula equation, because validity of $\\varphi[X \\leftarrow \\alpha]$ is then a first-order question.","On clause sets, the method generalises Ackermann's Lemma: whenever the lemma applies, there is a one-sided derivation whose witness is equivalent to the lemma's witness, and the method also covers cases where the lemma does not apply.","For one-sided derivations, witness size is at most exponential in the number of purified clauses, and linear when each purified clause contains exactly one $X$-literal; matching lower bounds show the bounds are tight.","The transformation lemma underlying the witness construction doubles as a new proof of SCAN's correctness, independent of the original argument."],"supporting_citations":[{"why":"Introduces the SCAN algorithm that WSCAN extends with witness extraction.","marker":"[22]"},{"why":"Supplies the redundancy criteria and clause-deletion rules used in the purification process.","marker":"[20]"},{"why":"Describes the SCAN elimination procedure whose derivation steps are recorded for witness construction.","marker":"[42]"},{"why":"Provides Ackermann's Lemma, the WSOQE method that the paper shows WSCAN generalises on clause sets.","marker":"[1]"},{"why":"Provides the software system in which the prototype implementation is built.","marker":"[18]"},{"why":"States the background theory of second-order quantifier elimination and Ackermann's Lemma as used in the appendix.","marker":"[23]"}],"fun_headline_variants":["SCAN extension yields explicit witnesses for quantified predicates","WSCAN: from SCAN runs to concrete replacement formulas","New algorithm computes witness formulas for second-order elimination","SCAN now outputs witnesses, not just equivalent clause sets","WSCAN: compute witnesses from any terminating SCAN run"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof assumes that once a clause's direct resolvents are redundant, all clauses obtainable by repeatedly resolving with it are also redundant, though the stated deletion rule only guarantees the direct ones are.","fun_headline_variants_meta":{"raw":{"variants":["SCAN extension yields explicit witnesses for quantified predicates","WSCAN: from SCAN runs to concrete replacement formulas","New algorithm computes witness formulas for second-order elimination","SCAN now outputs witnesses, not just equivalent clause sets","WSCAN: compute witnesses from any terminating SCAN run"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000458,"raw_usage":{"total_tokens":2277,"prompt_tokens":905,"completion_tokens":1372,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":521,"completion_tokens_details":{"reasoning_tokens":1293}},"tokens_in":521,"tokens_out":1372,"duration_ms":13783,"temperature":1.0,"reasoning_tokens":1293,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T12:14:36.862283+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a clause set $N$, a pointed clause $P$, and a redundancy criterion satisfying the paper's two conditions (entailment-compatible and equivalence-preserving) such that every one-step resolvent of $P$ with $N$ is redundant in $N$ but some iterated resolvent in $\\mathrm{Res}_P(N)$ is not entailed by $N$; such a counterexample would break the transformation lemma and with it the main theorem.","supporting_citations":[{"cited_title":"South African Computer Journal7, 35–43 (1992)","cited_arxiv_id":null,"evidence_quote":"Introduces the SCAN algorithm that WSCAN extends with witness extraction."},{"cited_title":"Diplomarbeit, Fachbereich Informatik, Univ","cited_arxiv_id":null,"evidence_quote":"Supplies the redundancy criteria and clause-deletion rules used in the purification process."},{"cited_title":"In: McRobbie, M.A., Slaney, J.K","cited_arxiv_id":null,"evidence_quote":"Describes the SCAN elimination procedure whose derivation steps are recorded for witness construction."},{"cited_title":"Mathematische Annalen110(1), 390–413 (1935)","cited_arxiv_id":null,"evidence_quote":"Provides Ackermann's Lemma, the WSOQE method that the paper shows WSCAN generalises on clause sets."},{"cited_title":"In: Olivetti, N., Tiwari, A","cited_arxiv_id":null,"evidence_quote":"Provides the software system in which the prototype implementation is built."},{"cited_title":"College Publications (2008)","cited_arxiv_id":null,"evidence_quote":"States the background theory of second-order quantifier elimination and Ackermann's Lemma as used in the appendix."}],"review_version":1}