On the Satisfiability of Two-Variable Logic over Data Words

Claire David; Leonid Libkin; Tony Tan

doi:10.1007/978-3-642-16242-8_18

On the Satisfiability of Two-Variable Logic over Data Words

Claire David, Leonid Libkin, Tony Tan

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 undocidable 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 non-trivial, 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.

Original language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning.
Subtitle of host publication	International Conference on Logic for Programming Artificial Intelligence and Reasoning
Editors	CG Fermuller, A Voronkov
Place of Publication	BERLIN
Publisher	Springer
Pages	248-262
Number of pages	15
ISBN (Print)	978-3-642-16241-1
DOIs	https://doi.org/10.1007/978-3-642-16242-8_18
Publication status	Published - 2010
Event	17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Yogyakarta Duration: 10 Oct 2010 → 15 Oct 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	6397
ISSN (Print)	0302-9743

Conference

Conference	17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
City	Yogyakarta
Period	10/10/10 → 15/10/10

Access to Document

10.1007/978-3-642-16242-8_18

https://link.springer.com/chapter/10.1007%2F978-3-642-16242-8_18

XML with Incomplete Information: Representation, Querying and Applications
Libkin, L.
EPSRC
1/09/09 → 30/11/13
Project: Research

Cite this

David, C., Libkin, L., & Tan, T. (2010). On the Satisfiability of Two-Variable Logic over Data Words. In CG. Fermuller, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning.: International Conference on Logic for Programming Artificial Intelligence and Reasoning (pp. 248-262). (Lecture Notes in Computer Science; Vol. 6397). Springer. https://doi.org/10.1007/978-3-642-16242-8_18

David, Claire ; Libkin, Leonid ; Tan, Tony. / On the Satisfiability of Two-Variable Logic over Data Words. Logic for Programming, Artificial Intelligence, and Reasoning.: International Conference on Logic for Programming Artificial Intelligence and Reasoning. editor / CG Fermuller ; A Voronkov. BERLIN : Springer, 2010. pp. 248-262 (Lecture Notes in Computer Science).

@inproceedings{36c56ecdaef84a0aa8eba24126b0d2b6,

title = "On the Satisfiability of Two-Variable Logic over Data Words",

abstract = "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 undocidable 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 non-trivial, 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.",

author = "Claire David and Leonid Libkin and Tony Tan",

year = "2010",

doi = "10.1007/978-3-642-16242-8_18",

language = "English",

isbn = "978-3-642-16241-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "248--262",

editor = "CG Fermuller and A Voronkov",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning.",

address = "United Kingdom",

note = "17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ; Conference date: 10-10-2010 Through 15-10-2010",

}

David, C, Libkin, L & Tan, T 2010, On the Satisfiability of Two-Variable Logic over Data Words. in CG Fermuller & A Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning.: International Conference on Logic for Programming Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, vol. 6397, Springer, BERLIN, pp. 248-262, 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Yogyakarta, 10/10/10. https://doi.org/10.1007/978-3-642-16242-8_18

On the Satisfiability of Two-Variable Logic over Data Words. / David, Claire; Libkin, Leonid; Tan, Tony.
Logic for Programming, Artificial Intelligence, and Reasoning.: International Conference on Logic for Programming Artificial Intelligence and Reasoning. ed. / CG Fermuller; A Voronkov. BERLIN: Springer, 2010. p. 248-262 (Lecture Notes in Computer Science; Vol. 6397).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - On the Satisfiability of Two-Variable Logic over Data Words

AU - David, Claire

AU - Libkin, Leonid

AU - Tan, Tony

PY - 2010

Y1 - 2010

N2 - 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 undocidable 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 non-trivial, 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.

AB - 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 undocidable 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 non-trivial, 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.

U2 - 10.1007/978-3-642-16242-8_18

DO - 10.1007/978-3-642-16242-8_18

M3 - Conference contribution

SN - 978-3-642-16241-1

T3 - Lecture Notes in Computer Science

SP - 248

EP - 262

BT - Logic for Programming, Artificial Intelligence, and Reasoning.

A2 - Fermuller, CG

A2 - Voronkov, A

PB - Springer

CY - BERLIN

T2 - 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning

Y2 - 10 October 2010 through 15 October 2010

ER -

David C, Libkin L, Tan T. On the Satisfiability of Two-Variable Logic over Data Words. In Fermuller CG, Voronkov A, editors, Logic for Programming, Artificial Intelligence, and Reasoning.: International Conference on Logic for Programming Artificial Intelligence and Reasoning. BERLIN: Springer. 2010. p. 248-262. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-16242-8_18

On the Satisfiability of Two-Variable Logic over Data Words

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

XML with Incomplete Information: Representation, Querying and Applications

Cite this