Simplifying the signature in second-order unification

Second-Order Unification is undecidable even for very specialized fragments. The signature plays a crucial role in these fragments. If all symbols are monadic, then the problem is NP-complete, whereas it is enough to have just one binary constant to lose decidability. In this work we reduce Second-Order Unification to Second-Order Unification with a signature that contains just one binary function symbol and constants. The reduction is based on partially currying the equations by using the binary function symbol for explicit application. Our work simplifies the study of Second-Order Unification and some of its variants, like Context Unification and Bounded Second-Order Unification. © 2009 Springer-Verlag.This research has been partially supported by the research projects Mulog-2 (TIN2007-68005-C04-01) and SuRoS (TIN2008-04547) funded by the CICyTPeer Reviewe