Search

Though higher-order unification is in general undecidable, there are expressive and decidable variants. Several interesting special cases and variants stem from restricting algorithms to search only unifiers where the number of bound variables is restricted. The intention of this paper is to summarize results in this area and to shed some light on the connections between context unification, decidable variants of higher-order, second order unification and string unification. Since this paper is intended to appear in a volume in celebrating Jörg Siekmann's 60th birthday, we will take the opportunity to give hints on how the motivating power of Jörg Siekmann has contributed to and put forward the research in unification. [ABSTRACT FROM AUTHOR]

Context unification is a generalisation of string unification where words are generalized to terms with one hole. Though decidability of string unification was proved by Makanin, the decidability of context unification is currently an open question. This paper provides a step in understanding the complexity of context unification and the structure of unifiers. It is shown, that if a context unification problem of size d is unifiable, then there is also a unifier with an exponent of periodicity smaller than O(21.07d). We also prove NP-hardness for restricted cases of the context unification problem and compare the complexity of general context unification with that of general string unification. [ABSTRACT FROM AUTHOR]