Back to Search
Start Over
Bounded Second-Order Unification Is NP-Complete.
- Source :
- Term Rewriting & Applications (9783540368342); 2006, p400-414, 15p
- Publication Year :
- 2006
-
Abstract
- Bounded Second-Order Unification is the problem of deciding, for a given second-order equation ${t {\stackrel{_?}=} u}$ and a positive integer m, whether there exists a unifier σ such that, for every second-order variable F, the terms instantiated for F have at most m occurrences of every bound variable. It is already known that Bounded Second-Order Unification is decidable and NP-hard, whereas general Second-Order Unification is undecidable. We prove that Bounded Second-Order Unification is NP-complete, provided that m is given in unary encoding, by proving that a size-minimal solution can be represented in polynomial space, and then applying a generalization of Plandowski's polynomial algorithm that compares compacted terms in polynomial time. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISBNs :
- 9783540368342
- Database :
- Complementary Index
- Journal :
- Term Rewriting & Applications (9783540368342)
- Publication Type :
- Book
- Accession number :
- 32910458
- Full Text :
- https://doi.org/10.1007/11805618_30