{"id":"3713e5ea-d38b-44da-b232-eb203e6225ec","arxiv_id":"2506.01664","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Introduces general uniform interpolants extending covers and uniform interpolants, and shows how symbol elimination in local theory extensions computes them by reducing to uniform interpolation in extensions with uninterpreted functions.","lead":"This paper defines a more general kind of logical summary called a 'general uniform interpolant', which can forget both constants and function symbols while keeping all consequences about the remaining symbols. It shows when and how such summaries can be computed by combining symbol elimination with existing interpolation algorithms, which is useful for program verification and ontology reasoning.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 7(2) invokes weak embeddability for a partial model with infinitely many defined terms, a case not covered by the stated criterion; the main reduction is therefore not rigorously established as written.","rationale":"The reader correctly identified locality as a key assumption in the paper's reduction. My concern is more specific: the proofs use the weak embeddability characterization of locality, but they apply it to partial structures that do not satisfy the finiteness condition T(A) finite stated in that characterization. This is a genuine gap in the written proof of Theorem 7(2), and since this theorem underpins the later results (Theorems 10, 14, 16, 17), the central claim is not rigorously established as written. The gap appears repairable by a finite-submodel argument, but that argument is absent, so the appropriate verdict is CONDITIONAL rather than a full rejection. I do not see evidence of a false claim or an internal inconsistency; the concern is about the rigor of the proof step, not the validity of the stated theorems. The paper's careful discussion of limitations (Example 3) suggests the authors are aware of the boundaries of the method, which supports a conditional acceptance rather than rejection.","tokens_in":30597,"tokens_out":41981,"duration_ms":421805,"concrete_test":"Take the partial model P from the proof of Theorem 7(2) and replace it by the finite submodel P_S whose universe is the set of all subterms of G, Γ, θ, and K[G] (closed under subterms), with functions defined only when their value lies in this set. Verify that P_S satisfies the hypotheses of Theorem 18: T(P_S) is finite, all terms in est(K, T(P_S)) are defined, and P_S is a weak partial model of T0∪K. Then check whether the weak-embeddability argument goes through for P_S and yields the required total model B with the same Π_r-reduct embedding. If this finite-submodel repair works, the proof gap is benign; if it does not, the central reduction of general uniform interpolation to symbol elimination plus uniform interpolation is not justified.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The proof of Theorem 7(2) constructs a partial structure P with the same support as A, in which all symbols in Π0, Σs, and Σi are total and interpreted as in A, while only the Σ1-terms from Def are defined. It then asserts: 'By the locality of the extension T0 ⊆ T0∪K, P weakly embeds into a total model B of T0∪K.' This step uses the weak embeddability characterization of locality (Theorem 18 and the definition of PMod^Ψ_w,f in Appendix A), which applies only to partial models A with T(A) finite. Here T(A) is the set of all defined extension-ground terms. Because Σs and Σi are total on an infinite universe, T(P) is infinite; for instance, any unary f ∈ Σs applied to every element of |P| generates infinitely many terms in T(P). Hence P is not in PMod_w,f, and the cited embeddability theorem does not license the inference. The same issue recurs in Lemma 12, Proposition 9, and Theorem 16, where partial structures with total Σs/Σi functions on an infinite domain are embedded on the strength of locality. This is load-bearing because the correctness of Algorithm 1 as a uniform-interpolant-producing procedure, and hence Theorems 7, 10, 14, 16, and 17, depends on this embeddability step. The gap may be repairable by replacing P with a finite submodel generated by the terms occurring in G, Γ, K[G], and θ, which would restore T(P) finiteness; however, the paper does not supply this argument, and the proofs as written are incomplete.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a notion of general uniform interpolant that generalizes both covers and uniform interpolants, proves a semantic characterization (Theorem 6), and proposes an algorithm (Algorithm 1) that reduces the computation of general uniform interpolants in local theory extensions to quantifier elimination in a base theory and uniform quantifier-free interpolation in extensions with uninterpreted function symbols. The main theorems (7, 10, 14, 16, 17) claim correctness of this reduction under locality, flat/linearity, and definability conditions. The paper also gives a limitation example (Example 3) showing that finite general uniform interpolants need not exist in general, and a method for extracting explicit definitions of implicitly definable functions.","tokens_in":30856,"tokens_out":10719,"duration_ms":124808,"significance":"If correct, this gives a useful reduction method for a demanding form of interpolation, and the semantic characterization and limitation example are valuable contributions. The paper is careful in separating the steps and in identifying the conditions (A1)-(A2) and the closure operator Theta_K under which the reduction works. The reliance on existing algorithms for uniform interpolation in UIF is appropriate, and Example 3 provides a clear boundary of the method.","major_comments":[{"comment":"The locality step in the proof of Theorem 7(2) is not justified as written. The proof constructs a partial structure P in which Pi0, Sigma_s, and Sigma_i are total on the whole universe of A, with only Sigma1-terms from Def defined, and then states that 'By the locality of the extension T0 subset T0 union K, P weakly embeds into a total model B of T0 union K.' The weak-embeddability characterization used for this step (Appendix A, Definition 6 and Theorem 18) applies only to partial models A with T(A) finite. Here T(P) is infinite whenever the universe is infinite, because every application of a total symbol in Sigma_s or Sigma_i to every tuple of elements is a defined term in T(P). Therefore P is not in the class PMod^Psi_w,f, and locality does not license the inference. The same gap occurs in the proofs of Proposition 9, Lemma 12, and Theorem 16 (Claim 2, Step 2), where partial structures with total Sigma_s or Sigma_f functions on an infinite domain are embedded on the strength of locality. Since the final condition A restricted to Pi_r embeds into B restricted to Pi_r requires agreement on all of A, replacing P by a finite submodel generated by G would not trivially repair the argument. Thus the correctness of Algorithm 1 as a uniform-interpolant-producing procedure is not established as written.","section":"Theorem 7(2), Section 5.1"},{"comment":"Lemma 12's proof has the same infinite-partial-model problem. Given a model A of T0 union Ks[T] union K1 union theta, the proof defines P with Sigma1 total on |A| and Sigma_s' partial on terms in T, and then says that 'By the locality assumption, P weakly embeds into a total model B of T0 union Ks union K1.' Since Sigma1 is total on |A|, T(P) is again infinite, so the finite-T(A) hypothesis of the embeddability theorem is not met. This matters because Lemma 12 is the bridge used in Proposition 13 and Theorem 14 to replace Ks by its finite instantiation Ks[T]; without a valid proof of Lemma 12, the reduction in those results is unsupported.","section":"Lemma 12, Section 5.2.2"}],"minor_comments":[{"comment":"The notation Pi^r_r is used for the signature of non-eliminated symbols, but the subscripts and superscripts make it hard to distinguish from the earlier Pi_s; a single symbol such as Pi_keep would improve readability.","section":"Section 4, before Definition 2"},{"comment":"The variable c is used both for the sequence of constants to be eliminated and as an argument placeholder in G1(cp, cf, c), which makes the step unnecessarily hard to parse.","section":"Algorithm 1, Step 2"},{"comment":"The statement says that C_s consists of Cs together with all constants occurring as arguments of Sigma_s-functions in G, but the general uniform interpolant is defined w.r.t. Sigma_s union C_s; the relation between C_s and Cs should be made explicit at the point of use.","section":"Theorem 7(2)"}],"recommendation":"major_revision","confidential_remarks":"I see no issue of novelty or scope. The main obstacle is the infinite-partial-model gap in the embeddability steps; if the authors can supply a corrected embeddability argument that preserves the required embedding, the paper should be publishable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick read, in case you are deciding whether to engage: this is a serious paper and worth refereeing, but it is not quite done. The genuinely new thing is Definition 2, the general uniform interpolant, which lets you eliminate function symbols and constants together, not just constants. Theorem 6's semantic characterization is clean and correctly extends the one in [2]. Algorithm 1 plus the reduction to uniform interpolation in extensions with uninterpreted functions is a real method, and the paper is careful about where finite interpolants fail, as Example 3 shows. The author also discloses the overlap with the CADE version. Credit where it is due.\n\nNow the soft spot. The stress-test note lands. In the proof of Theorem 7(2), a partial structure P is built with the same support as A, with Sigma_s and Sigma_i total on an infinite universe and only Sigma_1 terms from Def defined. The proof then invokes locality to assert that P weakly embeds into a total model. But the weak embeddability characterization in Appendix A, Theorem 18, is stated for PMod^Psi_w,f, which requires T(P) finite. Here T(P) is infinite, because total Sigma_s and Sigma_i functions generate infinitely many defined terms on an infinite domain. The same move appears in Lemma 12, Proposition 9, and Theorem 16. Since this embeddability step is what delivers condition (2') and hence the main reduction, the proof as written has a gap.\n\nIt is probably repairable. Rather than embedding the whole infinite partial structure, one can work with finite subsets of the diagram of A restricted to the preserved signature, apply locality to the finite partial structures those subsets determine, and then use compactness to obtain the required model B. That is standard in this area and I would be surprised if it failed here. But the paper does not supply that argument, so the referees should ask for it.\n\nThe paper also leans on existing uniform-interpolation algorithms and earlier locality results. That is legitimate, but it means the central reduction is not machine-checked, and the confidence should stay moderate. The statements themselves are cautious enough that I do not see overclaiming.\n\nWho is this for: people working on interpolation, forgetting in description logics, and symbol elimination for verification. I would bring it to a reading group. Send it to serious referees; once the proof gap is closed, it should be a solid contribution.","headline":"A real generalization of uniform interpolation with a plausible reduction, but the key embeddability step in Theorem 7(2) overreaches and needs a repair before publication.","tokens_in":31439,"tokens_out":4257,"would_cite":true,"duration_ms":53942,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","03C40","68T15"],"pacs":[],"model":"deepseek-v4-flash","headline":"For a class of local theory extensions, general uniform interpolants — strongest consequences restricted to shared symbols — can be computed by symbol elimination via quantifier elimination in the base theory followed by uniform…","keywords":["general uniform interpolation","symbol elimination","local theory extensions","quantifier elimination","uniform quantifier-free interpolation","covers","uninterpreted function symbols","hierarchical reasoning"],"falsifier":"Take a local flat-and-linear extension with a quantifier-elimination base theory, run Algorithm 1 on a fixed input $G$ and shared symbols $\\Sigma_s \\cup C_s$, and test the output $\\psi$ by the semantic criterion of Theorem 6: build a model of $T_0 \\cup K$ satisfying $\\psi$ whose restriction to the shared signature cannot be embedded into any model satisfying $G$. Finding such a model would refute completeness. A second, readily checkable boundary is the paper's Example 3: in $\\text{LI}([0,1])$ extended with a monotone function $f$ satisfying $f(x) \\le 1$, the formula $(a \\le b) \\land (b \\le f(b))$ has, according to the paper, no finite general uniform interpolant w.r.t. $\\{f,a\\}$; verifying this infinite consequence set directly settles where the method must stop.","tokens_in":30338,"feed_emoji":"🧩","tokens_out":8636,"duration_ms":88676,"temperature":0.7,"pith_summary":"This paper tries to show that for a wide class of theory extensions, the strongest consequence of a formula expressible with a chosen set of shared symbols — its 'general uniform interpolant' — can be computed algorithmically. The class consists of local theory extensions $T_0 \\subseteq T_0 \\cup K$, where $K$ is a finite set of flat and linear clauses in which every variable occurs below an extension function symbol, and the base theory $T_0$ admits quantifier elimination. The proposed computation runs in two stages: Algorithm 1 eliminates the unshared function symbols by instantiating the axioms on the ground terms of the input, purifying, and applying quantifier elimination in $T_0$; a second stage eliminates remaining constants by computing uniform quantifier-free interpolants in extensions with uninterpreted function symbols, for which cover algorithms already exist. If correct, this turns a hard projection problem into two well-understood subproblems, which matters for verification tasks such as computing reachable-state approximations and for 'forgetting' in knowledge representation. The paper also identifies a boundary: for some monotone bounded extensions no finite general uniform interpolant exists.","feed_headline":"Uniform interpolants become computable in local theory extensions","feed_subtitle":"Strongest shared-symbol consequences reduce to quantifier elimination plus covers.","key_machinery":"The load-bearing mechanism is the locality of the extension, expressed as condition (Loc${}^\\Psi_f$): for every finite ground $G$, $T_0 \\cup K \\cup G$ is unsatisfiable exactly when $T_0 \\cup K[\\Psi_K(G)] \\cup G$ is, so checking consistency never needs more than the finite instantiation $K[\\Psi_K(G)]$. On top of this, Algorithm 1 performs hierarchical reasoning — purify the instantiated clauses by introducing new constants for extension terms, collect the resulting base-sorted clauses plus congruence axioms, and eliminate the non-shared constants by quantifier elimination in $T_0$. The other half is Theorem 6, a semantic characterization that says a formula $\\psi$ is a general uniform interpolant precisely when every model of $\\psi$ embeds its shared reduct into some model of the original formula; this is what lets the proofs verify the output of the algorithm.","core_discovery":"The central claim is that general uniform interpolation in these local extensions is reducible to symbol elimination followed by uniform interpolation in free-function extensions. For a ground formula $G$ and chosen shared symbols $\\Sigma_s \\cup C_s$, Algorithm 1 — which uses the locality of the extension to replace $K$ by its finite instantiation $K[\\Psi_K(G)]$, flattens and purifies to a base-sorted clause set, existentially quantifies the unshared constants, and performs quantifier elimination in $T_0$ — yields a formula $\\Gamma$ that is already a general uniform interpolant with respect to the shared function symbols (Theorem 7). When constants occurring below shared function symbols also need elimination, $\\Gamma$ is passed to a uniform-interpolation routine for $T_0 \\cup \\text{UIF}_\\Sigma$ to obtain the final interpolant (Theorem 10, Proposition 9, Theorem 14). For chains of local extensions with definable functions, the same mechanism extracts explicit definitions and then uses them to eliminate definable symbols (Theorems 16–17).","pith_inferences":["The reduction suggests a practical recipe for verification tools: axiomatize transition systems as local theory extensions, then use quantifier elimination plus existing EUF-cover algorithms to project reachable states onto shared signatures; the paper does not implement this.","Because locality for flat/linear clauses is decidable via weak embeddability of partial models, the applicability of the method could be checked automatically for a given axiom set, turning the theorem into a decision procedure for membership in the tractable class.","The failure in Example 3 — an infinite chain of consequences $a \\le f^n(1)$ — matches the fixpoint-style representations known in description-logic forgetting; a natural extension would represent such interpolants by fixpoint or automaton terms, though the paper only points toward this.","The two-stage structure suggests that improvements in either subproblem (faster quantifier elimination in $T_0$, or better uniform-interpolation algorithms for uninterpreted functions) lift immediately to the whole class covered by the theorems."],"forward_implications":["For every base theory satisfying the hypotheses (convex, stably infinite, equality interpolating, universal, with quantifier elimination), every ground formula has a general uniform interpolant with respect to any choice of uninterpreted symbols and constants from the formula, and the interpolant is computable by Algorithm 1 plus an existing cover method.","Algorithm 1 turns the problem into two calls: one to a quantifier-elimination routine for $T_0$, one to a uniform-interpolation routine for $T_0 \\cup \\text{UIF}_\\Sigma$; both are available for example for linear real arithmetic with free functions, so the method is directly realizable for that theory.","For extensions whose shared and eliminated axiom sets are disjoint, the interpolant output by Algorithm 1 already contains only the shared function symbols, and the remaining constants can be eliminated by a $T_0 \\cup \\text{UIF}$ uniform interpolant, giving a clean decomposition of the interpolation problem.","When functions are implicitly definable in a chain of local extensions, Algorithm 1 yields explicit definitions (Theorems 15–16); those definitions can then replace the definable symbols anywhere, so general uniform interpolation reduces again to free-function extension interpolation.","The paper's semantic characterization (Theorem 6) provides a model-theoretic certificate for any candidate interpolant: checking the embeddability condition is an independent, local verification of correctness."],"supporting_citations":[{"why":"Defines T-covers/uniform interpolants and the semantic characterization (Theorem 3) that Definition 2 generalizes, and supplies the superposition method for UIF$\\Sigma$.","marker":"[2]"},{"why":"Provides DAG/tableau algorithms that compute UIF$\\Sigma$-uniform interpolants, used in the second stage of the reduction.","marker":"[5]"},{"why":"Shows how to combine uniform interpolants via Beth definability, used to compute uniform interpolants in $T_0 \\cup \\text{UIF}_{\\Sigma_s \\cup \\Sigma_1}$.","marker":"[3]"},{"why":"Introduces the cover notion that general uniform interpolants generalize, fixing the semantic intuition and the target of the method.","marker":"[6]"},{"why":"Establishes general ground interpolation and equality interpolation for quantifier-elimination theories, supplying hypotheses used in Theorems 10 and 14.","marker":"[1]"},{"why":"Introduces local theory extensions and hierarchical reasoning, the basis of the instantiation-and-purification step in Algorithm 1.","marker":"[25]"},{"why":"Gives the embeddability characterization of $\\Psi$-locality and locality-transfer results used in the proofs of Theorem 7(2) and Theorem 16.","marker":"[13]"},{"why":"The earlier symbol-elimination method that Algorithm 1 adapts, connecting the paper to previous work on parameter constraints.","marker":"[32]"}],"fun_headline_variants":["General uniform interpolants via symbol elimination","Uniform interpolation reducible to symbol elimination","Local extensions make general uniform interpolation computable","Symbol elimination computes general uniform interpolants"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole method rests on the assumption that the theory extension is 'local', meaning that checking consistency of any concrete finite problem needs only finitely many instances of the extension axioms; if that fails, the hierarchical reduction produces an incomplete answer.","fun_headline_variants_meta":{"raw":{"variants":["General uniform interpolants via symbol elimination","Uniform interpolation reducible to symbol elimination","Local extensions make general uniform interpolation computable","Symbol elimination computes general uniform interpolants"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000141,"raw_usage":{"total_tokens":1102,"prompt_tokens":821,"completion_tokens":281,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":437,"completion_tokens_details":{"reasoning_tokens":228}},"tokens_in":437,"tokens_out":281,"duration_ms":3426,"temperature":1.0,"reasoning_tokens":228,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:38:01.494419+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a local flat-and-linear extension with a quantifier-elimination base theory, run Algorithm 1 on a fixed input $G$ and shared symbols $\\Sigma_s \\cup C_s$, and test the output $\\psi$ by the semantic criterion of Theorem 6: build a model of $T_0 \\cup K$ satisfying $\\psi$ whose restriction to the shared signature cannot be embedded into any model satisfying $G$. Finding such a model would refute completeness. A second, readily checkable boundary is the paper's Example 3: in $\\text{LI}([0,1])$ extended with a monotone function $f$ satisfying $f(x) \\le 1$, the formula $(a \\le b) \\land (b \\le f(b))$ has, according to the paper, no finite general uniform interpolant w.r.t. $\\{f,a\\}$; verifying this infinite consequence set directly settles where the method must stop.","supporting_citations":[{"cited_title":"Calvanese, S","cited_arxiv_id":null,"evidence_quote":"Defines T-covers/uniform interpolants and the semantic characterization (Theorem 3) that Definition 2 generalizes, and supplies the superposition method for UIF$\\Sigma$."},{"cited_title":"Ghilardi, A","cited_arxiv_id":null,"evidence_quote":"Provides DAG/tableau algorithms that compute UIF$\\Sigma$-uniform interpolants, used in the second stage of the reduction."},{"cited_title":"Calvanese, S","cited_arxiv_id":null,"evidence_quote":"Shows how to combine uniform interpolants via Beth definability, used to compute uniform interpolants in $T_0 \\cup \\text{UIF}_{\\Sigma_s \\cup \\Sigma_1}$."},{"cited_title":"Gulwani and M","cited_arxiv_id":null,"evidence_quote":"Introduces the cover notion that general uniform interpolants generalize, fixing the semantic intuition and the target of the method."},{"cited_title":"Bruttomesso, S","cited_arxiv_id":null,"evidence_quote":"Establishes general ground interpolation and equality interpolation for quantifier-elimination theories, supplying hypotheses used in Theorems 10 and 14."},{"cited_title":"Sofronie-Stokkermans","cited_arxiv_id":null,"evidence_quote":"Introduces local theory extensions and hierarchical reasoning, the basis of the instantiation-and-purification step in Algorithm 1."},{"cited_title":"Ihlemann and V","cited_arxiv_id":null,"evidence_quote":"Gives the embeddability characterization of $\\Psi$-locality and locality-transfer results used in the proofs of Theorem 7(2) and Theorem 16."},{"cited_title":"Sofronie-Stokkermans","cited_arxiv_id":null,"evidence_quote":"The earlier symbol-elimination method that Algorithm 1 adapts, connecting the paper to previous work on parameter constraints."}],"review_version":1}