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.
On Symbol Elimination and Uniform Interpolation in Theory Extensions
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
fields
cs.LO 1years
2026 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
On Constructing Most General Solutions for Parametric Constraints (Extended Preprint)
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.