Logics with Counting and Equivalence

Ian Pratt-Hartmann; Thomas Henzinger; Dale Miller

doi:10.1145/2603088.2603117

Logics with Counting and Equivalence

Ian Pratt-Hartmann, Thomas Henzinger (Editor), Dale Miller (Editor)

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

We consider the two-variable fragment of first-order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NEXPTIME-complete. We further show that the corresponding problems for two-variable first-order logic with counting and two equivalences are both undecidable.

Original language	English
Title of host publication	ACM/IEEE Symposium on Logic in Computer Science
Editors	Thomas Henzinger, Dale Miller
Publisher	Association for Computing Machinery
Pages	1-10
Number of pages	10
ISBN (Print)	978-1-4503-2886-9
DOIs	https://doi.org/10.1145/2603088.2603117
Publication status	Published - 12 Jul 2014
Event	CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Vienna Duration: 12 Jul 2014 → 24 Jul 2014

Conference

Conference	CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
City	Vienna
Period	12/07/14 → 24/07/14

Keywords

Equivalence relation
Satisfiability
Complexity

Access to Document

10.1145/2603088.2603117

Cite this

@inproceedings{a6673508a64d4729a03f965694f858a9,

title = "Logics with Counting and Equivalence",

abstract = "We consider the two-variable fragment of first-order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NEXPTIME-complete. We further show that the corresponding problems for two-variable first-order logic with counting and two equivalences are both undecidable.",

keywords = "Equivalence relation, Satisfiability, Complexity",

author = "Ian Pratt-Hartmann and Thomas Henzinger and Dale Miller",

note = "This work is supported by the EPSRC, grant number EP/K017438/1.; CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ; Conference date: 12-07-2014 Through 24-07-2014",

year = "2014",

month = jul,

day = "12",

doi = "10.1145/2603088.2603117",

language = "English",

isbn = "978-1-4503-2886-9",

pages = "1--10",

editor = "Thomas Henzinger and Dale Miller",

booktitle = "ACM/IEEE Symposium on Logic in Computer Science",

publisher = "Association for Computing Machinery",

address = "United States",

}

Pratt-Hartmann, I, Henzinger, T (ed.) & Miller, D (ed.) 2014, Logics with Counting and Equivalence. in T Henzinger & D Miller (eds), ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery, pp. 1-10, CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vienna, 12/07/14. https://doi.org/10.1145/2603088.2603117

TY - GEN

T1 - Logics with Counting and Equivalence

AU - Pratt-Hartmann, Ian

A2 - Henzinger, Thomas

A2 - Miller, Dale

A2 - Henzinger, Thomas

A2 - Miller, Dale

N1 - This work is supported by the EPSRC, grant number EP/K017438/1.

PY - 2014/7/12

Y1 - 2014/7/12

N2 - We consider the two-variable fragment of first-order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NEXPTIME-complete. We further show that the corresponding problems for two-variable first-order logic with counting and two equivalences are both undecidable.

AB - We consider the two-variable fragment of first-order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NEXPTIME-complete. We further show that the corresponding problems for two-variable first-order logic with counting and two equivalences are both undecidable.

KW - Equivalence relation

KW - Satisfiability

KW - Complexity

U2 - 10.1145/2603088.2603117

DO - 10.1145/2603088.2603117

M3 - Conference contribution

SN - 978-1-4503-2886-9

SP - 1

EP - 10

BT - ACM/IEEE Symposium on Logic in Computer Science

PB - Association for Computing Machinery

T2 - CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Y2 - 12 July 2014 through 24 July 2014

ER -

Logics with Counting and Equivalence

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this