Vienna University of Technology
A formula equation is a formula in first-order logic with unknowns representing predicates. Solving a formula equation consists of finding first-order instances of these unknowns that result in a valid formula. In the first part of this talk I will give a general overview of formula equations, linking them, in particular, to applications in automated theorem proving. In the second part I will present joint work with Sebastian Zivota showing that solvability of affine formula equations is decidable, thus generalising previous results about loop invariant generation.