Decidability of affine solution problems

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 Auflosungsproblem and loop invariant generation. In the case of the language of affine terms over Q, we translate a quantifier-free formula equation into an equivalent statement about affine spaces over Q, which can then be decided by an iteration procedure.