A note on C2 interpreted over finite data-words

Bartosz BednarczykBartosz Bednarczyk, Piotr WitkowskiPiotr Witkowski

Bartosz Bednarczyk, Piotr Witkowski
A note on C2 interpreted over finite data-words
In Emilio Muñoz-Velasco, Ana Ozaki, Martin Theobald, eds., Proceedings of the 27th International Symposium on Temporal Representation and Reasoning (TIME 2020), volume 178 of Leibniz International Proceedings in Informatics, 17:1--17:14, September 2020. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Details
Bibtex

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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{BW2020,
  author    = {Bartosz Bednarczyk and Piotr Witkowski},
  title     = {A note on C2 interpreted over finite data-words},
  editor    = {Emilio Mu{\~{n}}oz-Velasco and Ana Ozaki and Martin Theobald},
  booktitle = {Proceedings of the 27th International Symposium on Temporal
               Representation and Reasoning (TIME 2020)},
  series    = {Leibniz International Proceedings in Informatics},
  volume    = {178},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2020},
  month     = {September},
  pages     = {17:1--17:14},
  doi       = {10.4230/LIPIcs.TIME.2020.17}
}