Two-variable logic on data words
Top Cited Papers
- 22 July 2011
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computational Logic
- Vol. 12 (4), 1-26
- https://doi.org/10.1145/1970398.1970403
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.Keywords
Funding Information
- Polish MNII (4 T11C 042 25)
This publication has 19 references indexed in Scilit:
- Two-variable logic on data trees and XML reasoningJournal of the ACM, 2009
- LTL with the freeze quantifier and register automataACM Transactions on Computational Logic, 2009
- Finite state machines for strings over infinite alphabetsACM Transactions on Computational Logic, 2004
- First-Order Logic with Two Variables and Unary Temporal LogicInformation and Computation, 2002
- Two variable first-order logic over ordered domainsThe Journal of Symbolic Logic, 2001
- On logics with two variablesTheoretical Computer Science, 1999
- Finite-memory automataTheoretical Computer Science, 1994
- Shuffle languages, Petri nets, and context-sensitive grammarsCommunications of the ACM, 1981
- On languages with two variablesMathematical Logic Quarterly, 1975
- Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime FactorsAmerican Journal of Mathematics, 1913