Complexity of two-variable Dependence Logic and IF-Logic

被引:4
|
作者
Kontinen, Juha [1 ]
Kuusisto, Antti [2 ]
Lohmann, Peter [3 ]
Virtema, Jonni [2 ]
机构
[1] Univ Helsinki, FIN-00014 Helsinki, Finland
[2] Univ Tampere, FIN-33101 Tampere, Finland
[3] Leibniz Univ Hannover, Hannover, Germany
基金
芬兰科学院;
关键词
dependence logic; independence-friendly logic; two-variable logic; decidability; complexity; satisfiability; expressivity; 1ST-ORDER LOGIC; 2; VARIABLES; QUANTIFIERS;
D O I
10.1109/LICS.2011.14
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We study the two-variable fragments D-2 and IF2 of dependence logic and independence-friendly logic. We consider the satisfiability and finite satisfiability problems of these logics and show that for D-2, both problems are NEXPTIME-complete, whereas for IF2, the problems are Pi(0)(1) and Sigma(0)(1)-complete, respectively. We also show that D-2 is strictly less expressive than IF2 and that already in D-2, equicardinality of two unary predicates and infinity can be expressed (the latter in the presence of a constant symbol). An extended version of this publication can be found at arxiv.org.
引用
收藏
页码:289 / 298
页数:10
相关论文
共 50 条
  • [31] Communicating Finite-State Machines and Two-Variable Logic
    Bollig, Benedikt
    Fortin, Marie
    Gastin, Paul
    35TH SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2018), 2018, 96
  • [32] Linear circuits, two-variable logic and weakly blocked monoids
    Behle, Christoph
    Krebs, Andreas
    Mercer, Mark
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2007, PROCEEDINGS, 2007, 4708 : 147 - +
  • [33] REGISTER AUTOMATA WITH EXTREMA CONSTRAINTS, AND AN APPLICATION TO TWO-VARIABLE LOGIC
    Toruńczyk, Szymon
    Zeume, Thomas
    Logical Methods in Computer Science, 2022, 18 (01): : 1 - 42
  • [34] TWO-VARIABLE FIRST-ORDER LOGIC WITH EQUIVALENCE CLOSURE
    Kieronski, Emanuel
    Michaliszyn, Jakub
    Pratt-Hartmann, Ian
    Tendera, Lidia
    SIAM JOURNAL ON COMPUTING, 2014, 43 (03) : 1012 - 1063
  • [35] On the decision problem for two-variable first-order logic
    Gradel, E
    Kolaitis, PG
    Vardi, MY
    BULLETIN OF SYMBOLIC LOGIC, 1997, 3 (01) : 53 - 69
  • [36] Two-Variable First-Order Logic with Equivalence Closure
    Kieronski, Emanuel
    Michaliszyn, Jakub
    Pratt-Hartmann, Ian
    Tendera, Lidia
    2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 431 - 440
  • [37] Thompson transformations for IF-logic
    Dechesne, F
    SYNTHESE, 2006, 149 (02) : 31 - 55
  • [38] Thompson Transformations for If-Logic
    Francien Dechesne
    Synthese, 2006, 149 : 285 - 309
  • [39] ON TWO-VARIABLE GUARDED FRAGMENT LOGIC WITH EXPRESSIVE LOCAL PRESBURGER CONSTRAINTS
    Lu, Chia-Hsuan
    Tan, Tony
    LOGICAL METHODS IN COMPUTER SCIENCE, 2024, 20 (03) : 1 - 16
  • [40] On the satisfiability problem for fragments of two-variable logic with one transitive relation
    Szwast, Wieslaw
    Tendera, Lidia
    JOURNAL OF LOGIC AND COMPUTATION, 2019, 29 (06) : 881 - 911