Inproceedings3251

PublikationenPublications

• Nach AutorBy Author
  • Bartosz BednarczykBartosz Bednarczyk
• Nach ForschungsgruppeBy Research Group
  • Computational LogicComputational Logic

Toggle side column

A note on C2 interpreted over finite data-words

Bartosz BednarczykBartosz Bednarczyk,  Piotr WitkowskiPiotr Witkowski

• Download
• DOI Link

Bartosz Bednarczyk, Piotr Witkowski
A note on C2 interpreted over finite data-words
27th International Symposium on Temporal Representation and Reasoning (TIME 2020), September 2020

• 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},
  booktitle = {27th International Symposium on Temporal Representation and
               Reasoning (TIME 2020)},
  year      = {2020},
  month     = {September},
  doi       = {10.4230/LIPIcs.TIME.2020.17}
}