Equivalence closure in the two-variable guarded fragment

被引：3

作者：

Kieronski, Emanuel ^{[1
]}

Pratt-Hartmann, Ian ^{[2
,3
]}

Tendera, Lidia ^{[3
]}

机构：

[1] Univ Wroclaw, Inst Comp Sci, Wroclaw, Poland

[2] Univ Manchester, Sch Comp Sci, Manchester, Lancs, England

[3] Opole Univ, Inst Math & Informat, Oleska 48, PL-45052 Opole, Poland

来源：

JOURNAL OF LOGIC AND COMPUTATION | 2017年 / 27卷 / 04期

基金：

英国工程与自然科学研究理事会;

关键词：

Satisfiability problem; computational complexity; decidability; guarded fragment; equivalence closure; 1ST-ORDER LOGIC; FINITE SATISFIABILITY; TRANSITIVE GUARDS; VARIABLES; LANGUAGES;

D O I：

10.1093/logcom/exv075

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We consider the satisfiability and finite satisfiability problems for the extension of the two-variable guarded fragment in which an equivalence closure operator can be applied to two distinguished binary predicates. We show that the satisfiability and finite satisfiability problems for this logic are 2-ExpTime-complete. This contrasts with an earlier result that the corresponding problems for the full two-variable logic with equivalence closures of two binary predicates are 2-NExpTime-complete.

引用

页码：999 / 1021

页数：23

共 50 条

[1] The two-variable fragment with counting and equivalence
Pratt-Hartmann, Ian
[J]. MATHEMATICAL LOGIC QUARTERLY, 2015, 61 (06) : 474 - 515
[2] A polynomial translation from the two-variable guarded fragment with number restrictions to the guarded fragment
Kazakov, Y
[J]. LOGICS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, 3229 : 372 - 384
[3] Complexity of the guarded two-variable fragment with counting quantifiers
Pratt-Hartmann, Ian
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2007, 17 (01) : 133 - 155
[4] On the complexity of the two-variable guarded fragment with transitive guards
Kieronski, Emanuel
[J]. INFORMATION AND COMPUTATION, 2006, 204 (11) : 1663 - 1703
[5] ON TWO-VARIABLE GUARDED FRAGMENT LOGIC WITH EXPRESSIVE LOCAL PRESBURGER CONSTRAINTS
Lu, Chia-Hsuan
Tan, Tony
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2024, 20 (03)
[6] Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants
Kieronski, Emanuel
Tendera, Lidia
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2018, 19 (02)
[7] ADDING PATH-FUNCTIONAL DEPENDENCIES TO THE GUARDED TWO-VARIABLE FRAGMENT WITH COUNTING
Kourtis, Georgios
Pratt-Hartmann, Ian
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2017, 13 (04)
[8] The two-variable guarded fragment with transitive guards is 2EXPTIME-hard
Kieronski, E
[J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2003, 2620 : 299 - 312
[9] Two-Variable First-Order Logic with Equivalence Closure
Kieronski, Emanuel
Michaliszyn, Jakub
Pratt-Hartmann, Ian
Tendera, Lidia
[J]. 2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 431 - 440
[10] TWO-VARIABLE FIRST-ORDER LOGIC WITH EQUIVALENCE CLOSURE
Kieronski, Emanuel
Michaliszyn, Jakub
Pratt-Hartmann, Ian
Tendera, Lidia
[J]. SIAM JOURNAL ON COMPUTING, 2014, 43 (03) : 1012 - 1063

← 1 2 3 4 5 →