@article {IIIA-2008-1686, title = {The Complexity of Monadic Second-Order Unification}, journal = {SIAM Journal on Computing}, volume = {38}, number = {3}, year = {2008}, pages = {1113-1140}, abstract = {Monadic Second-Order Unification is Second-Order Unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using singleton context free grammars. We prove that Monadic Second-Order Matching is also NP-complete.}, keywords = {Lambda Calculus, second-order unification}, author = {Jordi Levy and Manfred Schmidt-Schauss and Mateu Villaret} }