On Constructing Most General Solutions for Parametric Constraints (Extended Preprint)

Let $\mathcal{T}$ be a theory allowing a form of elimination of existential quantifiers (possibly for formulae in a certain class). We analyze possibilities of constructing (most general) solutions w.r.t.\ $\mathcal{T}$ for formulae of the form $\mathrm{\exists }{x}_1\dots \mathrm{\exists }{x}_n\phi (x_1,\dots ,x_n,y_1,\dots ,y_m)$, where $\phi$ is a quantifier-free conjunction of literals in the signature of $\mathcal{T}$, and the free variables $y_1,\dots ,y_m$ are regarded as parameters. We show that in the presence of function symbols which describe ``{\sf if}-{\sf then}-{\sf else}‘’ constructions in certain models of $\mathcal{T}$, we can describe the most general solution of such formulae, thus generalizing results about the existence of most general unifiers in discriminator varieties. We illustrate the ideas on examples.