Text this: Unification modulo a partial theory of exponentiation