TitleOn the complexity of Bounded Second-Order Unification and Stratified Context Unification
Publication TypeJournal Article
Year of Publication2011
AuthorsLevy J, Schmidt-Schauss M, Villaret M
JournalLogic Journal of the IGPL
Date Published2011
KeywordsHigher-Order Unification

Bounded Second-Order Unification is a decidable variant of undecidable Second-Order Unification. Stratified Context Unification is a decidable restriction of Context Unification, whose decidability is a long-standing open problem. This paper is a join of two separate previous, preliminary papers on NP-completeness of Bounded Second-Order Unification and Stratified Context Unification. It clarifies some omissions in these papers, joins the algorithmic parts that construct a minimal solution, and gives a clear account of a method of using singleton tree grammars for compression that may have potential usage for other algorithmic questions in related areas.