A note on C2 interpreted over finite data-words

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

A note on C2 interpreted over finite data-words

Bartosz BednarczykBartosz Bednarczyk,  Piotr WitkowskiPiotr Witkowski
A note on C2 interpreted over finite data-words


Bartosz Bednarczyk, Piotr Witkowski
A note on C2 interpreted over finite data-words
27th International Symposium on Temporal Representation and Reasoning (TIME 2020), to appear
  • KurzfassungAbstract
    We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C2[≤,succ,∼,πbin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from π_bin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ~. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [MontanariPS16]. We supplement our results with decidability for several sub-fragments of C2[≤, succ, ∼ ,π_bin], e.g., without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant.
  • Forschungsgruppe:Research Group: Computational Logic
@inproceedings{BW2020,
  author    = {Bartosz Bednarczyk and Piotr Witkowski},
  title     = {A note on C2 interpreted over finite data-words},
  booktitle = {27th International Symposium on Temporal Representation and
               Reasoning (TIME 2020)},
  year      = {2020},
  month     = {September}
}