Decidability of affine solution problems
Stefan Hetzl, Sebastian Zivota · Journal of Logic and Computation · 2019
Abstract We present formula equations—first-order formulas with unknowns standing for predicates—as a general formalism for treating certain questions in logic and computer science, like the Auflösungsproblem and loop invariant generation. In the case of the language of affine terms over $\mathbb{Q}$, we translate a quantifier-free formula equation into an equivalent statement about affine spaces over $\mathbb{Q}$, which can then be decided by an iteration procedure.