The Complexity of Monadic Second-Order Unification

DOI10.1137/050645403MaRDI QIDQ3631904zbMATH OpenOpenAlexFDO

Authors Jordi Levy, Mateu Villaret, Manfred Schmidt-Schauß

Publication date 22 June 2009

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/050645403

zbMATH Keywords

context-free grammarslambda calculusrewriting systemssecond-order unificationtheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Grammars and rewriting systems (68Q42)

Recommendations

• Rewriting Techniques and Applications
• Bounded Second-Order Unification Is NP-Complete
• On the complexity of bounded second-order unification and stratified context unification
• Monadic simultaneous rigid E-unification and related problems
• Monadic simultaneous rigid E-unification

Cited in

(10)

• A unification algorithm for second-order monadic terms
• Farmer's theorem revisited
• Fusion in relational structures and the verification of monadic second-order properties
• Grammar-Based Tree Compression
• Bounded Second-Order Unification Is NP-Complete
• Parameter reduction and automata evaluation for grammar-compressed trees
• Linear pattern matching of compressed terms and polynomial rewriting
• Rewriting Techniques and Applications
• One is all you need: associative second-order unification without first-order variables
• Simplifying the signature in second-order unification

This page was built for publication: The Complexity of Monadic Second-Order Unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3631904)