Decidable variants of higher-order unification

Abstract

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. © Springer-Verlag Berlin Heidelberg 2005.