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 条
  • [21] Two-Variable Separation Logic and Its Inner Circle
    Demri, Stephane
    Deters, Morgan
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2015, 16 (02)
  • [22] Two-Variable Logic on Data Trees and XML Reasoning
    Bojanczyk, Mikoaj
    Muscholl, Anca
    Schwentick, Thomas
    Segoufin, Luc
    JOURNAL OF THE ACM, 2009, 56 (03)
  • [23] Order-Invariance of Two-Variable Logic is Decidable
    Zeume, Thomas
    Harwath, Frederik
    PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), 2016, : 807 - 816
  • [24] An Effective Characterization of the Alternation Hierarchy in Two-Variable Logic
    Krebs, Andreas
    Straubing, Howard
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2017, 18 (04)
  • [25] Towards a more efficient approach for the satisfiability of two-variable logic
    Lin, Ting-Wei
    Lu, Chia-Hsuan
    Tan, Tony
    2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2021,
  • [26] Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
    Torunczyk, Szymon
    Zeume, Thomas
    PROCEEDINGS OF THE 35TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2020), 2020, : 873 - 885
  • [27] A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic
    Place, Thomas
    Zeitoun, Marc
    32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
  • [28] TWO-VARIABLE LOGIC HAS WEAK, BUT NOT STRONG, BETH DEFINABILITY
    Andreka, Hajnal
    Nemeti, Istvan
    JOURNAL OF SYMBOLIC LOGIC, 2021, 86 (02) : 785 - 800
  • [29] On the boundedness problem for two-variable first-order logic
    Kolaitis, PG
    Otto, M
    THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 513 - 524
  • [30] Linear circuits, two-variable logic and weakly blocked monoids
    Behle, Christoph
    Krebs, Andreas
    Mercer, Mark
    THEORETICAL COMPUTER SCIENCE, 2013, 501 : 20 - 33