The Complexity of Monadic Second-Order Unification

Abstract. 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. Key words. second-order unification, theorem proving, lambda calculus, context-free grammars, rewriting systems AMS subject classifications. 03B15, 68Q42, 68T15 DOI. 10.1137/050645403

• Type: Journal
• Year: 2008
• Where: SIAMCOMP
• Authors: Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret
• Keywords: Monadic Second-order, Monadic Second-order Unification, Second-order Unification, SIAMCOMP 2008