TitleOn the Complexity of Bounded Second-order Unification and Stratified Context Unification
Publication TypeJournal Article
Year of Publication2009
AuthorsLevy J, Schmidt-Schauss M, Villaret M
JournalJournal of Algorithms in Cognition, Informatics, and Logic

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.