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 this talk I will first give an overview of this topic and, in particular, describe its connections to well-known problems in logic and its applications in computer science. I will then concentrate on specific classes of formula equations and present

  1. joint work with J. Kloibhofer on solutions of Horn formula equations in first-order logic with least fixed points and
  2. joint work with S. Zivota showing that solvability of affine formula equations is decidable, thus generalising previous results about loop invariant generation.