On Constructing Most General Solutions for Parametric Constraints (Extended Preprint)
2026-07-09 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study a way to find the most general solutions to certain logic formulas that say "there exist some values" meeting specific conditions. They focus on formulas where the conditions don’t have nested "exists" statements and involve known functions in the theory. They show that if the theory includes functions similar to "if-then-else" rules, then these solutions can be described clearly and generally. Their work extends earlier results about finding general solutions in specialized algebraic settings. They also provide examples to explain their approach.
existential quantifier eliminationmost general solutionquantifier-free formulalogical theoryif-then-else functiondiscriminator varietyunificationmodel theoryliteralsfree variables
Authors
Viorica Sofronie-Stokkermans
Abstract
Let ${\cal 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.\ ${\cal T}$ for formulae of the form $\exists x_1 \dots \exists x_n φ(x_1, \dots, x_n, y_1, \dots, y_m)$, where $φ$ is a quantifier-free conjunction of literals in the signature of ${\cal 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 ${\cal 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.