Solvability of Context Equations with Two Context Variables is Decidable

Context unification is a natural variant of second-order unification that represents a generalization of word unification at the same time. While second-order unification is well known to be undecidable and word unification is decidable it is currently an open question if the solvability of context equations is decidable. We show that the solvability of systems of context equations with two context variables is decidable. The context variables may have an arbitrary number of occurrences, and the equations may also contain an arbitrary number of individual variables. The result holds under the assumption that the first-order background signature is finite.