摘要：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 C²[⤠, 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 [Angelo Montanari et al., 2016]. We supplement our results with decidability for several sub-fragments of C²[⤠, 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.
