IIIA CSIC
Published on IIIA CSIC (http://iiia.csic.es)

Inici > Bounded Second-Order Unification Is NP-Complete

Bounded Second-Order Unification Is NP-Complete

TítolBounded Second-Order Unification Is NP-Complete
Publication TypeConference Paper
Year of Publication2006
AuthorsLevy J [1], Schmidt-Schauss M [2], Villaret M [3]
Conference NameLecture Notes in Computer Science
Volume4098
EditorSpringer-Verlag
Paginació400-414
Resum

Bounded Second-Order Unification is the problem of deciding, for a given second-order equation t=u and a positive integer m, whether there exists a unifier sigma 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.


Source URL: http://iiia.csic.es/ca/node/55466

Enllaços
[1] http://iiia.csic.es/ca/staff/jordi-levy
[2] http://iiia.csic.es/ca/staff/manfred-schmidt-schauss
[3] http://iiia.csic.es/ca/staff/mateu-villaret