The Complexity of Monadic Second-Order Unification

Monadic second-order unification is second-order unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using single...

Full description

Saved in:
Bibliographic Details
Published in:SIAM journal on computing 2008-01, Vol.38 (3), p.1113-1140
Main Authors: Levy, Jordi, Schmidt-Schauß, Manfred, Villaret, Mateu
Format: Article
Language:English
Subjects:
Variables
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Monadic second-order unification is second-order unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using singleton context-free grammars. We prove that monadic second-order matching is also NP-complete.
ISSN:0097-5397
1095-7111
DOI:10.1137/050645403