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

Abstract

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 $\exists x_1\dots \exists x_n\ddot{I}•(x_1,\dots ,x_n,y_1,\dots ,y_m)$, where $\ddot{I}•$ 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.

28 pages