Title | On the complexity of Bounded Second-Order Unification and Stratified Context Unification |

Publication Type | Journal Article |

Year of Publication | 2011 |

Authors | Levy J [1], Schmidt-Schauss M [2], Villaret M [3] |

Journal | Logic Journal of the IGPL |

Volume | 19 |

Pagination | 763-789 |

Date Published | 2011 |

Keywords | Higher-Order Unification [4] |

Abstract | 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. |