The complexity of monadic second-order unification

被引：12
|
作者：
Levy, Jordi [1 ]
Schmidt-Schauss, Manfred [2 ]
Villaret, Mateu [3 ]
机构：
[1] CSIC, IIIA, Barcelona 08193, Spain
[2] Univ Frankfurt, Inst Informat, D-60054 Frankfurt, Germany
[3] Univ Girona, Informat & Matemat Aplicada, Girona 17071, Spain
来源：
SIAM JOURNAL ON COMPUTING | 2008年 / 38卷 / 03期
关键词：
second-order unification; theorem proving; lambda calculus; context-free grammars; rewriting systems;
D O I：
10.1137/050645403
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：1113 / 1140
页数：28
相关论文
共 50 条
  • [1] A UNIFICATION ALGORITHM FOR SECOND-ORDER MONADIC TERMS
    FARMER, WM
    ANNALS OF PURE AND APPLIED LOGIC, 1988, 39 (02) : 131 - 174
  • [2] Monadic second-order unification is NP-complete
    Levy, J
    Schmidt-Schauss, M
    Villaret, M
    REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, 2004, 3091 : 55 - 69
  • [3] Lower Bounds for the Complexity of Monadic Second-Order Logic
    Kreutzer, Stephan
    Tazari, Siamak
    25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 189 - 198
  • [4] On the complexity of Bounded Second-Order Unification and Stratified Context Unification
    Levy, Jordi
    Schmidt-Schauss, Manfred
    Villaret, Mateu
    LOGIC JOURNAL OF THE IGPL, 2011, 19 (06) : 763 - 789
  • [5] The complexity of first-order and monadic second-order logic revisited
    Frick, M
    Grohe, M
    17TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2002, : 215 - 224
  • [6] The complexity of first-order and monadic second-order logic revisited
    Frick, M
    Grohe, M
    ANNALS OF PURE AND APPLIED LOGIC, 2004, 130 (1-3) : 3 - 31
  • [7] MONADIC (SECOND-ORDER) THEORY OF ORDER
    SHELAH, S
    NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1973, 20 (01): : A22 - A22
  • [8] Monadic Second-Order Classes of Forests with a Monadic Second-Order 0-1 Law
    Bell, Jason P.
    Burris, Stanley N.
    Yeats, Karen A.
    DISCRETE MATHEMATICS AND THEORETICAL COMPUTER SCIENCE, 2012, 14 (01): : 87 - 107
  • [9] Monadic Second-Order Logic with Arbitrary Monadic Predicates
    Fijalkow, Nathanael
    Paperman, Charles
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2014, PT I, 2014, 8634 : 279 - 290
  • [10] Monadic Second-Order Logic with Arbitrary Monadic Predicates
    Fijalkow, Nathanael
    Paperman, Charles
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2017, 18 (03)
12345