Sciweavers

Share
LPAR
2010
Springer

On the Satisfiability of Two-Variable Logic over Data Words

8 years 3 months ago
On the Satisfiability of Two-Variable Logic over Data Words
Data trees and data words have been studied extensively in connection with XML reasoning. These are trees or words that, in addition to labels from a finite alphabet, carry labels from an infinite alphabet (data). While in general logics such as MSO or FO are undecidable for such extensions, decidablity results for their fragments have been obtained recently, most notably for the two-variable fragments of FO and existential MSO. The proofs, however, are very long and nontrivial, and some of them come with no complexity guarantees. Here we give a much simplified proof of the decidability of two-variable logics for data words with the successor and data-equality predicates. In addition, the new proof provides several new fragments of lower complexity. The proof mixes database-inspired constraints with encodings in Presburger arithmetic.
Claire David, Leonid Libkin, Tony Tan
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Claire David, Leonid Libkin, Tony Tan
Comments (0)
books