{"id":"5c5f0ea4-8d9a-44e9-afc0-8fc638e864b8","arxiv_id":"2608.09190","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"The GK prover reports positive support, negative support, conflict, and ignorance by retaining proof provenance and resolving opposing evidence at the atom where it arises.","lead":"A first-order logic reasoning system gains new ways to report how confident its answers are, tracking which uncertain facts each proof uses and where opposing evidence cancels. It combines uncertainty, rules with exceptions, and proof search without needing to ground every possible instance, which matters for large or function-rich knowledge bases.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the central claims are conditional on explicitly disclosed semantic postulates, and the correspondence theorem's fragment conditions are stated precisely enough to support the reported agreements.","rationale":"The reader's weakest assumption (shared-threshold coupling) is a genuine caveat, but the paper explicitly treats it as a semantic postulate and never claims coupling-independent semantics; Proposition 6 is conditional on that postulate. The more concrete residual risk is that some implementation conditions of the correspondence fragment are not self-checked (factoring exclusion, coarse index merging), so an unlabelled output can be outside the fragment. The paper documents this and marks Example 12 as outside the fragment, so the theoretical claim remains intact. Given the disclosed assumptions, the analytic checks, and the independent sampler agreement on the stated fragment, the ACCEPT verdict does not need adjustment.","tokens_in":45490,"tokens_out":17585,"duration_ms":187295,"concrete_test":"Instrument the public binary's proof replay to detect classical factoring steps and coarse dependency-index merges, then rerun all 43 example-suite rows with report details enabled. Confirm that every DA/in row is factoring-free and index-merge-free and that the GK tuple matches the ST sampler within tolerance; if a DA/in row violates a fragment condition, the reported agreement for that row would not be evidence for Proposition 6.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I find no load-bearing defect in the central claim. Proposition 6 is explicitly conditional on the correspondence fragment (Section 5.5), and the shared-threshold coupling, noisy-or pooling, directed reading, and auxiliary contrary-gated threshold are all identified in Sections 5.2.1, 5.2.2, 5.4.3, and 6.4 as semantic postulates rather than empirical findings; the reported four components are therefore relative to those postulates by design. The manuscript also discloses the main implementation gaps: factoring-derived answers are outside the fragment without being detected (Section 11, Example 12), the coarse dependency index can merge distinct ground predecessors (Section 6.6), and proof replay does not cover all equality histories (Section 6.2). These weaken the practical claim that every unlabelled run is a completed shared-threshold result, but they do not falsify the conditional correspondence claim or the Section 8 agreement on the stated common fragment. I found no internal inconsistency in the arithmetic or in the proof sketch sufficient to move the verdict.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends the GK first-order resolution prover with two post-search quantitative report calculations. The first recomputes the probability that at least one retained proof is available, reconstructing ground activation events so that premises shared by several proofs are counted once. The second defines a shared-threshold semantics over directed ground applications and computes four region probabilities — positive support, negative support, conflict, and ignorance — by a report-time dependency traversal. The paper proves local algebraic properties (Propositions 1–5), states a conditional correspondence between the dependency-aware evaluator and the shared-threshold semantics (Proposition 6), and evaluates the implementation with analytic examples, Monte Carlo samplers, and comparisons with ProbLog, PASTA, plingo, smProbLog, TweetyProject, clingo, DLV, I-DLV, and s(CASP). It also contains an extensive and unusually explicit limitation section.","tokens_in":45675,"tokens_out":13046,"duration_ms":131569,"significance":"If the conditional claims are taken at face value, the contribution is significant for query-directed first-order reasoning with uncertainty and defaults: the system avoids global grounding, keeps conflict distinct from ignorance, and preserves shared dependencies in proof combination. The manuscript is also unusually careful in several respects: the shared-threshold semantics is presented as an authored postulate rather than an empirical finding; the shared-threshold sampler is a separate code base that does not call the reasoner; the clause-activation sampler's missing completion counts are disclosed and its values are not treated as semantic estimates; the status taxonomy distinguishes completed shared-threshold results from proof-pool decompositions; and Section 11 lists silent failure modes such as unflagged factoring and coarse dependency-index merging. The main caveat is that the reported agreement between GK and the samplers is internal consistency: the samplers implement the same defined semantics, so the evaluation validates implementation consistency and analytic arithmetic rather than providing independent confirmation of the semantics against an external model.","major_comments":[],"minor_comments":[{"comment":"The general statement in Section 5.4.1 that conflicted and ignorant exception states do not block a default is not applied in the contrary-gated case: there the default is blocked whenever the ordinary opposing pool is active, including the region UA ≤ min(a,b) that would otherwise be classified as conflict. Please add an explicit sentence stating that the contrary-gated local rule overrides the general exception-blocking rule, since a reader applying the general sentence would obtain different tuples.","section":"Section 5.4.3"},{"comment":"The sensitivity interval [max(0,a−b), min(a,1−b)] is an interval for P(E+ \\ E-), not for the reported s+ component; the shared-threshold report itself is a point value under the maximal-overlap coupling. Consider stating this explicitly near the interval, because the current wording could be read as making the report interval-valued.","section":"Section 5.2.2, Proposition 2"},{"comment":"The paper-level codes such as RP/out and DA/in are not all emitted by the implementation; Example 12 is a row with no emitted flag and a paper-level outside-fragment classification. Please state near the example-suite table that these codes are the paper's classification, not necessarily the implementation's output fields, so that readers do not expect a flag where none exists.","section":"Section 6.6 and Table 8"},{"comment":"The clause-activation sampler uses the same GK prover for derivability checks; the paper says this, but it is worth repeating when the CA column is discussed in Section 8 that agreement with CA is not an independent test of proof search, and that only the shared-threshold sampler is independent of the reasoner's uncertainty code.","section":"Section 7.2.1 and Section 8.1"},{"comment":"Several inline mathematical examples have spacing artifacts from PDF rendering, such as 'Consider0.5 ::bird(a)' in Section 2 and 'Example 18, f lies(a)' in Table 7. These should be cleaned in the final version.","section":"Throughout"}],"recommendation":"minor_revision","confidential_remarks":"The manuscript is carefully written and honestly scoped. My only substantive requests are editorial: clarify that the contrary-gated local rule overrides the general exception-blocking sentence, and clarify the provenance of the paper-level status codes. The proof sketch for Proposition 6 is acceptable for the level of formality in this venue; if the editor prefers a fully formal proof, expanding the sketch into an appendix would be a low-cost improvement. The evaluation is internal-consistency rather than independent validation, but this is a disclosed limitation rather than a reason to reject."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Punchline first: this is a genuine, carefully scoped extension of the author's GK system, and the main claims hold under the postulates it discloses. The retained-proof union with shared ground-instance identities and the dependency-aware shared-threshold evaluator are real contributions, and the paper is unusually honest about their limits.\n\nWhat is new and what works: Equation (11) replaces the earlier scalar interpolation with exact inclusion–exclusion over reconstructed activation events, which fixes double-counting cleanly. The dependency-aware calculation resolves positive/negative support at the atom where it enters, before propagation, and the four-component report (positive, negative, conflict, ignorance) is a useful way to separate contradiction from missing evidence. The paper carefully distinguishes its two reference models and never runs them together. The limitations section is exemplary: it flags the factoring exclusion, the coarse dependency index, open premises, and the unflagged directionality restriction. The public repository includes binaries, examples, and samplers, which is a real plus.\n\nSoft spots, in proportion: I agree with the stress-test that there is no load-bearing flaw, but the caveats are real. Proposition 6, the central correspondence claim, is a proof sketch on a narrow fragment; it is conditional on many enumerated conditions, and the paper says so, but a reader should not expect a full theorem. The shared-threshold coupling is a stipulation (maximal-overlap, Fréchet lower bound), not an empirical finding. The paper gives sensitivity bounds and calls it a semantic postulate, but a user who wants independence will get different numbers. Also, the Section 8 agreements are mostly internal consistency: the clause-activation sampler reuses GK for derivability, and the shared-threshold sampler implements the same semantics defined in the paper. So the check is more about implementation fidelity than independent confirmation. The paper is transparent about this, but it does weaken the evidential value.\n\nWho it is for: people building knowledge-representation systems that need uncertainty, defaults, and explicit negation over non-ground clauses. It is a working engineering approach with clearly marked semantics, not a general probabilistic logic. The comparisons with ProbLog, ASP, and s(CASP) are useful context.\n\nRecommendation: this deserves peer review. It is a serious, careful contribution, and the disclosed conditions are testable. I would send it to a competent referee rather than desk-reject; the referee should check Proposition 6 and the fragment conditions carefully. My own verdict would be a qualified accept or major revision, not a reject.","headline":"A genuine, carefully scoped extension of GK; accept with close checking of the fragment conditions.","tokens_in":46173,"tokens_out":3945,"would_cite":true,"duration_ms":38489,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A first-order prover now computes uncertainty reports from retained proof histories, counting shared premises once and resolving opposing support at the atom where it occurs, without grounding the knowledge base.","keywords":["first-order theorem proving","uncertainty propagation","proof provenance","default rules with exceptions","shared-threshold semantics","probabilistic logic programming","nonmonotonic reasoning","dependency-aware evaluation"],"falsifier":"Run the contested-premise example 0.5::bird(a), 0.5::¬bird(a), 0.9::flies(a)←bird(a) through a Monte Carlo sampler that draws independent thresholds for the two polarities. The independent-coupling positive support is 0.5·0.5·0.9 = 0.225, whereas the paper's shared-threshold report is (0,0,0,1); if an implementation returns the independent value on this input while claiming a completed dependency-aware result, the claimed shared-threshold semantics is not what is computed.","tokens_in":45214,"feed_emoji":"⚖️","tokens_out":6329,"duration_ms":63300,"temperature":0.7,"pith_summary":"The paper claims that a query-directed first-order theorem prover can produce quantitative uncertainty reports without grounding the whole knowledge base, by keeping proof histories and re-analyzing them after proof search. One calculation reconstructs the uncertain ground premises each proof actually used and computes the probability that at least one retained proof is available, counting shared premises once instead of once per proof. A second, dependency-aware calculation resolves positive versus negative support at the atom where the opposition occurs before that atom is used by later rules, and reports four components: unopposed positive support, unopposed negative support, conflict, and ignorance. The same mechanism evaluates uncertain exception conditions of default rules. If the paper's formal correspondence holds, these reports are exact region probabilities of a defined shared-threshold semantics on a finite acyclic fragment, while bounded search flags incomplete calculations instead of hiding them.","feed_headline":"Prover resolves opposing evidence before it propagates","feed_subtitle":"First-order proof histories yield positive support, negative support, conflict, and ignorance — no global grounding","key_machinery":"The carrying objects are retained proof-history DAGs with activation-event identifiers, each naming an identified input-clause occurrence together with the ground instance it was used at, and the report-time directed dependency graph built from the clausified knowledge base. The retained-proof calculation uses inclusion-exclusion over activation-event sets (Equation (11)) so that shared premises are counted once. The dependency-aware calculation pools same-polarity support by noisy-or, then applies one shared Uniform(0,1) threshold per ground atom to both polarities, producing the four-region partition of Equation (2): (max(a-b,0), max(b-a,0), min(a,b), 1-max(a,b)). Contrary-gated defaults add an independent auxiliary threshold, and priorities assign overlap regions by rank. This machinery carries the argument because it replaces both double-counted scalar proof values and deferred query-level opposition with atom-level region measures computed from reconstructed ground instances.","core_discovery":"GK's central claim is that provenance-aware reporting can be layered onto bounded first-order proof search without changing the search's clauses or requiring a finite global grounding. Retained proof histories are replayed to recover the ground instances of uncertain input clauses used by each derivation; same-polarity proofs are combined by inclusion-exclusion over activation-event sets, so a premise shared by two proofs is counted once. When a ground atom is potentially two-sided, a separate report-time traversal builds a bounded directed dependency graph and applies shared-threshold semantics: same-polarity contributions are pooled by noisy-or and the two pools are compared against one shared Uniform(0,1) threshold per atom, partitioning the query atom's sample space into positive-only, negative-only, conflict, and ignorance regions; uncertain exception conditions are evaluated in the same framework as usable-region probabilities rather than subtracted from rule confidence. Proposition 6 states that within the correspondence fragment, which requires a finite acyclic relevant graph, supported inference forms, and complete enumeration, the evaluator returns exactly the measures induced by the shared-threshold world definition, and the reported evaluation shows all 54 scalar frequencies within Monte Carlo precision of their closed forms.","pith_inferences":["The same dependency graph could also emit the full coupling interval [max(0,a-b), min(a,1-b)] instead of only the shared-threshold lower bound, giving users a built-in sensitivity report on the opposition assumption.","Because the four-component report is computed from reconstructed ground instances, it could be extended to report which shared predecessors contributed to conflict, turning contested-atom identification into a fuller explanation trace.","The usable-region treatment of exceptions suggests a quantitative bridge to structured argumentation: undercutting attacks become conditional probabilities of blocked applications, while rebutting attacks enter the opposite pool; one testable extension would learn exception strength rather than stipulate it.","If the correspondence proposition holds, then on every finite acyclic query with one-sided rules GK's report should coincide with distribution-semantics query probabilities, while on contested-premise queries it should deliberately differ; users comparing systems should align the coupling choice before treating numerical differences as disagreements."],"forward_implications":["On one-sided derivations where each uncertain instance is used at most once, both reference semantics and the exact-translation comparisons return the same query values, so the new calculations reduce to standard probabilistic proof combination on that fragment.","A premise with equal opposing support no longer yields a propagated value like 0.45; the rule does not fire and the conclusion is reported as pure ignorance with the contested atom identified.","Two proofs sharing uncertain premises are combined as one union event rather than as independent noisy-or sources, and a duplicated proof contributes nothing beyond the original.","Default exceptions act as undercutting conditions: support for an exception condition reduces the rule's usable region but does not directly support the opposite conclusion, which instead enters the opposing pool.","Because the calculations run after bounded proof search and traverse only query-relevant ground instances, inputs with function terms and large irrelevant constant sets still produce reports, with fallback flags when reconstruction or traversal cannot complete."],"supporting_citations":[{"why":"Supplies the confidence-carrying resolution proof search whose retained histories the new calculations replay.","marker":"[48]"},{"why":"Supplies the recursively checked prioritized default mechanism that the exception semantics extends.","marker":"[49]"},{"why":"Defines the distribution-semantics ground-choice interpretation that Model 1 matches on its fragment.","marker":"[17]"},{"why":"Supplies the relevant-grounding compilation perspective used for exact-translation comparisons.","marker":"[21]"},{"why":"Provides the distribution-semantics activation convention for independent ground instances.","marker":"[43]"},{"why":"Provides the same-polarity pooling rule that noisy-or aggregation resembles.","marker":"[44]"},{"why":"Supplies the default-rule justification semantics that the paper adapts to quantified defaults and exceptions.","marker":"[39]"},{"why":"Supplies the undercutting-versus-rebutting distinction that the quantitative exception handling implements.","marker":"[37]"}],"fun_headline_variants":["Proof search computes support, conflict, and ignorance without global grounding","Uncertainty propagation in first-order proofs: shared premises counted once","Prover reports positive, negative, conflict, ignorance from proof histories","Structure-preserving uncertainty: no global grounding needed for proof support","First-order prover evaluates opposing evidence per atom via shared thresholds"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The reported numbers depend on a stipulated coupling: positive and negative support at an atom are resolved with one shared random threshold, and contrary-gated defaults get an independent auxiliary threshold; choose a different coupling and the reported four components change.","fun_headline_variants_meta":{"raw":{"variants":["Proof search computes support, conflict, and ignorance without global grounding","Uncertainty propagation in first-order proofs: shared premises counted once","Prover reports positive, negative, conflict, ignorance from proof histories","Structure-preserving uncertainty: no global grounding needed for proof support","First-order prover evaluates opposing evidence per atom via shared thresholds"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001302,"raw_usage":{"total_tokens":5342,"prompt_tokens":1007,"completion_tokens":4335,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":623,"completion_tokens_details":{"reasoning_tokens":4247}},"tokens_in":623,"tokens_out":4335,"duration_ms":28870,"temperature":1.0,"reasoning_tokens":4247,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T21:42:07.671899+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the contested-premise example 0.5::bird(a), 0.5::¬bird(a), 0.9::flies(a)←bird(a) through a Monte Carlo sampler that draws independent thresholds for the two polarities. The independent-coupling positive support is 0.5·0.5·0.9 = 0.225, whereas the paper's shared-threshold report is (0,0,0,1); if an implementation returns the independent value on this input while claiming a completed dependency-aware result, the claimed shared-threshold semantics is not what is computed.","supporting_citations":[{"cited_title":"Tammet, D","cited_arxiv_id":null,"evidence_quote":"Supplies the confidence-carrying resolution proof search whose retained histories the new calculations replay."},{"cited_title":"Tammet, D","cited_arxiv_id":null,"evidence_quote":"Supplies the recursively checked prioritized default mechanism that the exception semantics extends."},{"cited_title":"De Raedt, A","cited_arxiv_id":null,"evidence_quote":"Defines the distribution-semantics ground-choice interpretation that Model 1 matches on its fragment."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the distribution-semantics activation convention for independent ground instances."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the same-polarity pooling rule that noisy-or aggregation resembles."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the undercutting-versus-rebutting distinction that the quantitative exception handling implements."}],"review_version":1}