@conference {IIIA-2006-1248,
title = {Bounded Second-Order Unification Is NP-Complete},
booktitle = {Lecture Notes in Computer Science},
volume = {4098},
year = {2006},
pages = {400-414},
publisher = {Springer-Verlag},
organization = {Springer-Verlag},
abstract = {Bounded Second-Order Unification is the problem of deciding, for a given second-order equation t=u and a positive integer m, whether there exists a unifier sigma such that, for every second-order variable F, the terms instantiated for F have at most m occurrences of every bound variable. It is already known that Bounded Second-Order Unification is decidable and NP-hard, whereas general Second-Order Unification is undecidable. We prove that Bounded Second-Order Unification is NP-complete, provided that m is given in unary encoding, by proving that a size-minimal solution can be represented in polynomial space, and then applying a generalization of Plandowski{\textquoteright}s polynomial algorithm that compares compacted terms in polynomial time.},
author = {Jordi Levy and Manfred Schmidt-Schauss and Mateu Villaret}
}