Two-variable logic on data words
The work
| Authors | Mikołaj Bojańczyk; Claire David; Anca Muscholl; Thomas Schwentick; Luc Segoufin |
|---|---|
| Editors | |
| Type | article |
| Year | 2011 |
| Citekey | bojanczyk2011twovariable |
Where it appeared
| Published in | ACM Transactions on Computational Logic |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 12 |
| Issue | 4 |
| Pages | 1--26 |
Identifiers
| DOI | 10.1145/1970398.1970403 |
|---|---|
| OpenAlex | W2073614038 |
Access
| Landing page | https://doi.org/10.1145/1970398.1970403 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
In a data word each position carries a label from a finite alphabet and a data value from some infinite domain. This model has been already considered in the realm of semistructured data, timed automata, and extended temporal logics. This article shows that satisfiability for the two-variable fragment FO 2 (∼,<,+1) of first-order logic with data equality test ∼ is decidable over finite and infinite data words. Here +1 and < are the usual successor and order predicates, respectively. The satisfiability problem is shown to be at least as hard as reachability in Petri nets. Several extensions of the logic are considered; some remain decidable while some are undecidable.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 15:58 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{bojanczyk2011twovariable,
title = {Two-variable logic on data words},
author = {Mikołaj Bojańczyk and Claire David and Anca Muscholl and Thomas Schwentick and Luc Segoufin},
year = {2011},
journal = {ACM Transactions on Computational Logic},
publisher = {Association for Computing Machinery},
volume = {12},
number = {4},
pages = {1--26},
doi = {10.1145/1970398.1970403},
}
This record lives at https://refs.drheap.org/bojanczyk2011twovariable/ and will keep doing so.