Decidability of bounded second order unification

AbstractIt is well-known that first order unification is decidable, whereas second order (and higher-order) unification is undecidable. Bounded second order unification is second order unification under the restriction that only a bounded number of bound variables in the instantiating terms for second order variables is permitted, however, the size of the instantiation is not restricted. In this paper, a decision algorithm for bounded second order unification is described. This is the first nontrivial decidability result for second order unification, where the signature is not restricted and there are no restrictions on the occurrences of variables. This supports the claim that bounded second order unification is easier than context unification, whose decidability is currently an open question