On Symbol Elimination and Uniform Interpolation in Theory Extensions

Viorica Sofronie-Stokkermans

REVIEW 2 major objections 3 minor 1 cited by

On Symbol Elimination and Uniform Interpolation in Theory Extensions

T0 review · 2 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read 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…

desk verdict 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. read the letter →

arxiv 2506.01664 v1 pith:YIHEVX5B submitted 2025-06-02 cs.LO

Viorica Sofronie-Stokkermans This is my paper

classification cs.LO MSC 03B7003C4068T15

keywords generaluniforminterpolationsymboleliminationlocaltheoryextensionsquantifierquantifier-freecoversuninterpretedfunctionsymbolshierarchicalreasoning

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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).

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

Now 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.

It 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.

The 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.

Who 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.

Referee Report

2 major / 3 minor

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.

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 (2)

[Theorem 7(2), Section 5.1] 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.
[Lemma 12, Section 5.2.2] 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.

minor comments (3)

[Section 4, before Definition 2] 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.
[Algorithm 1, Step 2] 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.
[Theorem 7(2)] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Algorithm 1's output is derived by quantifier elimination from the input formula and verified against the semantic characterization of general uniform interpolants.

full rationale

The paper's central claim is proved rather than assumed. Definition 2 defines a general uniform interpolant, and Theorem 6 gives a direct semantic characterization with proof. Algorithm 1 computes Gamma by purifying K[T] union G, replacing the non-shared constants with existentially quantified variables, and eliminating them via quantifier elimination in T0; this is a syntactic/semantic reduction of the input formula, not a fitted parameter. Theorem 7(1) proves G entails Gamma by a model argument, and Theorem 7(2) verifies the semantic condition (2') using the locality/weak-embeddability framework, which is cited from prior published work but used as an assumption about the theory extension, not as a way of defining the interpolant. The same pattern holds in Theorems 10, 14, 16, and 17: the interpolants are constructed from G (and K[T]) and then checked against the defining conditions. The paper even exhibits Example 3 where no finite uniform interpolant exists, showing the boundary is not masked. Although the paper cites the author's own earlier work extensively, those citations supply the locality criterion and external uniform-interpolation algorithms; they are not equivalent to the target theorem, and the target theorem is not obtained by renaming a known result. A reviewer concern that the weak-embeddability step in Theorem 7(2) may require finiteness of T(P), which fails when Sigma_s-functions are total on an infinite domain, is a technical correctness issue about the applicability of a cited theorem, not a circularity: the conclusion would not be identical to the hypothesis by construction. No step reduces the claimed prediction to its own input by definition, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central claim is conditional on standard model-theoretic hypotheses (locality, flat/linear clauses, quantifier-elimination-capable base theory, uniform interpolation in EUF combinations) and uses no fitted parameters. No new entities are postulated. The paper proves its main theorems from these assumptions using the author's prior framework for local theory extensions and symbol elimination.

assumptions (6)

standard math Compactness and standard model theory.
Used in the proof of Theorem 6 to show that inconsistency of a finite set of literals from the diagram implies a contradiction, and to build models extending partial structures.
domain assumption The base theory T0 allows quantifier elimination.
Algorithm 1 Step 3 and Theorems 7, 10, 14 require that the existential formula over eliminated constants can be reduced to a quantifier-free formula with respect to T0.
domain assumption T0 is convex, stably infinite, equality interpolating, universal and admits uniform quantifier-free interpolation when combined with UIF.
Theorems 10 and 14 rely on Theorem 5 of [3] for uniform interpolation in T0 union UIF-Sigma; these hypotheses are standard for combination results.
domain assumption The extension T0 subset T0 union K is local (or Psi-local) and K is flat and linear.
Locality (condition Loc-Psi-f in Section 2.2) justifies replacing K by the finite instance set K[Psi(G)] and underlies the embeddability argument in the proof of Theorem 7(2); flatness and linearity are required for the partial-model characterization in Appendix A.
domain assumption Every variable in a clause of K occurs below an extension symbol.
Assumed throughout (e.g., Theorem 7 and Theorem 14) so that hierarchical reasoning terminates and the partial structure P has the needed defined terms.
domain assumption Implicit definability of functions in Sigma_d with respect to T0 union UIF-Sigma_f for Theorem 16.
Theorem 16 assumes the functions to be eliminated are implicitly definable, which is needed for the equivalence f approx f' to be derivable and for extracting explicit definitions.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On Symbol Elimination and Uniform Interpolation in Theory Extensions." pith.science (2026). https://pith.science/paper/YIHEVX5B

@misc{pith2026250601664,
  author       = {Pith},
  title        = {Pith review of: On Symbol Elimination and Uniform Interpolation in Theory Extensions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YIHEVX5B}},
  note         = {Machine review of arXiv:2506.01664}
}

read the original abstract

We define a notion of general uniform interpolant, generalizing the notions of cover and of uniform interpolant and identify situations in which symbol elimination can be used for computing general uniform interpolants. We investigate the limitations of the method we propose, and identify theory extensions for which the computation of general uniform interpolants can be reduced to symbol elimination followed by the computation of uniform quantifier-free interpolants in extensions with uninterpreted function symbols of theories allowing uniform quantifier-free interpolation.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

On Constructing Most General Solutions for Parametric Constraints (Extended Preprint)
cs.LO 2026-07 accept novelty 6.0 of 10

Theories admitting quantifier elimination plus if-then-else operators on a suitable model possess most-general (conditional) solutions for parametric existential conjunctions of literals, expressible as terms.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages · cited by 1 Pith paper

[2]

Calvanese, S

D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Model com- pleteness, uniform interpolants and superposition calculus.J. Autom. Reason., 65(7):941–969, 2021

work page 2021
[1]

Bruttomesso, S

R. Bruttomesso, S. Ghilardi, and S. Ranise. Quantifier-free interpolation in com- binations of equality interpolating theories.ACM Trans. Comput. Log., 15(1):5:1– 5:34, 2014

work page 2014
[3]

Calvanese, S

D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combination of uniform interpolants via Beth definability.J. Autom. Reason., 66(3):409–435, 2022

work page 2022
[4]

Ganzinger

H. Ganzinger. Relating semantic and proof-theoretic concepts for polynominal time decidability of uniform word problems. In16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 81–90. IEEE Computer Society, 2001

work page 2001
[5]

Ghilardi, A

S. Ghilardi, A. Gianola, and D. Kapur. Uniform interpolants in EUF: algorithms using dag-representations.Log. Methods Comput. Sci., 18(2), 2022

work page 2022
[6]

Gulwani and M

S. Gulwani and M. Musuvathi. Cover algorithms and their combination. In S. Drossopoulou, editor,Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, LNCS 4960, pages 193–207. Springer, 2008

work page 2008
[7]

Hoder, L

K. Hoder, L. Kovács, and A. Voronkov. Interpolation and symbol elimination in Vampire. In J. Giesl and R. Hähnle, editors,Automated Reasoning, 5th Interna- tional Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 188–195. Springer, 2010

work page 2010
[8]

Hodges.Model theory, volume 42 ofEncyclopedia of mathematics and its ap- plications

W. Hodges.Model theory, volume 42 ofEncyclopedia of mathematics and its ap- plications. Cambridge University Press, 1993

work page 1993

Show all 36 references

[9]

Horbach and V

M. Horbach and V. Sofronie-Stokkermans. Obtaining finite local theory axiomati- zations via saturation. In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings, LNCS 8152, pages 198–213. ...

2013
[10]

Horbach and V

M. Horbach and V. Sofronie-Stokkermans. Locality transfer: From constrained axiomatizations to reachability predicates. In S. Demri, D. Kapur, and C. Weiden- bach, editors,Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Proceedings, LNCS 8562, pages 192–2...

2014
[11]

Horbach and C

M. Horbach and C. Weidenbach. Deciding the inductive validity of FOR ALL THERE EXISTS* queries. In E. Grädel and R. Kahle, editors,Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Proceedings, LNCS 5771, pages 332–347. Springer, 2009

2009
[12]

Ihlemann, S

C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. On local reasoning in ver- ification. In C. R. Ramakrishnan and J. Rehof, editors,Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint Europe...

2008
[13]

Ihlemann and V

C. Ihlemann and V. Sofronie-Stokkermans. On hierarchical reasoning in combi- nations of theories. In J. Giesl and R. Hähnle, editors,Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 30–45. Springer, 2010

2010
[14]

Jhala and K

R. Jhala and K. L. McMillan. Interpolant-based transition relation approxima- tion. In K. Etessami and S. K. Rajamani, editors,Computer Aided Verification, 17th International Conference, CAV 2005, Proceedings, LNCS 3576, pages 39–51. Springer, 2005

2005
[15]

Kapur, R

D. Kapur, R. Majumdar, and C. G. Zarba. Interpolation for data structures. In M. Young and P. T. Devanbu, editors,Proceedings of the 14th ACM SIGSOFT In- ternational Symposium on Foundations of Software Engineering, FSE 2006, pages 105–116. ACM, 2006

2006
[16]

Konev, D

B. Konev, D. Walther, and F. Wolter. Forgetting and uniform interpolation in extensions of the description logicEL. In B. C. Grau, I. Horrocks, B. Motik, and U. Sattler, editors,Proceedings of the 22nd International Workshop on Description Logics (DL 2009), volume 477 ofCEUR W...

2009
[17]

Konev, D

B. Konev, D. Walther, and F. Wolter. Forgetting and uniform interpolation in large-scale description logic terminologies. In C. Boutilier, editor,IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pages 830–835, 2009

2009
[18]

Lutz and F

C. Lutz and F. Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In T. Walsh, editor,IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pages 989–995. IJCAI/AAAI, 2011

2011
[19]

D. A. McAllester. Automatic recognition of tractability in inference relations.J. ACM, 40(2):284–303, 1993

1993
[20]

K. L. McMillan. Interpolation and SAT-based model checking. In W. Hunt Jr. and F. Somenzi, editors,Computer Aided Verification, 15th International Conference, CAV 2003, Proceedings, LNCS 2725, pages 1–13. Springer, 2003

2003
[21]

K. L. McMillan. An interpolating theorem prover. In K. Jensen and A. Podel- ski, editors,Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Softw...

2004
[22]

K. L. McMillan. Applications of Craig interpolants in model checking. In N. Halb- wachs and L. D. Zuck, editors,Tools and Algorithms for the Construction and 30 Viorica Sofronie-Stokkermans (B) Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the...

2005
[23]

Peuter and V

D. Peuter and V. Sofronie-Stokkermans. On invariant synthesis for parametric systems. In P. Fontaine, editor,Automated Deduction - CADE 27 - 27th Inter- national Conference on Automated Deduction, Proceedings, LNCS 11716, pages 385–405. Springer, 2019

2019
[24]

Peuter, V

D. Peuter, V. Sofronie-Stokkermans, and S. Thunert. OnP-interpolation in local theory extensions and applications to the study of interpolation in the description logicsEL,EL +. In B. Pientka and C. Tinelli, editors,Automated Deduction - CADE 29 - 29th International Conference...

2023
[25]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In R. Nieuwenhuis, editor,Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Proceedings, LNCS 3632, pages 219–234. Springer, 2005

2005
[26]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Interpolation in local theory extensions. In U. Furbach and N. Shankar, editors,Automated Reasoning, Third International Joint Confer- ence, IJCAR 2006, Proceedings, LNCS 4130, pages 235–250. Springer, 2006

2006
[27]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Interpolation in local theory extensions.Logical Methods in Computer Science, 4(4), 2008

2008
[28]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Hierarchical reasoning for the verification of parametric systems. In J. Giesl and R. Hähnle, editors,Automated Reasoning, 5th Interna- tional Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 171–187. Springer, 2010

2010
[29]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Hierarchical reasoning and model generation for the verification of parametric hybrid systems. In M. P. Bonacina, editor,Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Proceedings, LNCS 7898, pages 360–376. Springer, 2013

2013
[30]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex- tensions. In N. Olivetti and A. Tiwari, editors,Automated Reasoning - 8th Inter- national Joint Conference, IJCAR 2016, Proceedings, LNCS 9706, pages 273–289. Springer, 2016

2016
[31]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Representation theorems and locality for subsumption testing and interpolation in the description logicsEL,EL + and their extensions withn-ary roles and numerical domains.Fundamenta Informaticae, 156(3-4):361– 411, 2017

2017
[32]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex- tensions.Log. Methods Comput. Sci., 14(3), 2018

2018
[33]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. Parametric systems: Verification and synthesis.Funda- menta Informaticae, 173(2-3):91–138, 2020

2020
[34]

Sofronie-Stokkermans

V. Sofronie-Stokkermans. On symbol elimination and uniform interpolation in theory extensions. InAutomated Deduction - CADE 30 - 30th International Con- ference on Automated Deduction, Proceedings. Springer, 2025. To appear

2025
[35]

Sofronie-Stokkermans and C

V. Sofronie-Stokkermans and C. Ihlemann. Automated reasoning in some local extensions of ordered structures. In37th International Symposium on Multiple- Valued Logic, ISMVL 2007, 13-16 May 2007, Oslo, Norway. IEEE Computer So- ciety, 2007

2007
[36]

Sofronie-Stokkermans and C

V. Sofronie-Stokkermans and C. Ihlemann. Automated reasoning in some local extensions of ordered structures.Multiple-Valued Logic and Soft Computing, 13(4- 6):397–414, 2007. 31 A Local theory extensions In [25] we proved that if every weak partial model of an extensionT0 ∪ Kof...

2007

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [2]

Calvanese, S

D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Model com- pleteness, uniform interpolants and superposition calculus.J. Autom. Reason., 65(7):941–969, 2021

work page 2021

[2] [1]

Bruttomesso, S

R. Bruttomesso, S. Ghilardi, and S. Ranise. Quantifier-free interpolation in com- binations of equality interpolating theories.ACM Trans. Comput. Log., 15(1):5:1– 5:34, 2014

work page 2014

[3] [3]

Calvanese, S

D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, and A. Rivkin. Combination of uniform interpolants via Beth definability.J. Autom. Reason., 66(3):409–435, 2022

work page 2022

[4] [4]

Ganzinger

H. Ganzinger. Relating semantic and proof-theoretic concepts for polynominal time decidability of uniform word problems. In16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 81–90. IEEE Computer Society, 2001

work page 2001

[5] [5]

Ghilardi, A

S. Ghilardi, A. Gianola, and D. Kapur. Uniform interpolants in EUF: algorithms using dag-representations.Log. Methods Comput. Sci., 18(2), 2022

work page 2022

[6] [6]

Gulwani and M

S. Gulwani and M. Musuvathi. Cover algorithms and their combination. In S. Drossopoulou, editor,Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, LNCS 4960, pages 193–207. Springer, 2008

work page 2008

[7] [7]

Hoder, L

K. Hoder, L. Kovács, and A. Voronkov. Interpolation and symbol elimination in Vampire. In J. Giesl and R. Hähnle, editors,Automated Reasoning, 5th Interna- tional Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 188–195. Springer, 2010

work page 2010

[8] [8]

Hodges.Model theory, volume 42 ofEncyclopedia of mathematics and its ap- plications

W. Hodges.Model theory, volume 42 ofEncyclopedia of mathematics and its ap- plications. Cambridge University Press, 1993

work page 1993