Mikolaj Bojańczyk
Thomas Schwentick
ABSTRACT
Motivated by reasoning tasks in the context of XML languages, the satisfiability problem of logics on data trees is investigated. The nodes of a data tree have a label from a finite set and a data value from a possibly infinite set. It is shown that satisfiability for two-variable first-order logic is decidable if the tree structure can be accessed only through the child and the next sibling predicates and the access to data values is restricted to equality tests. From this main result decidability of satisfiability and containment for a data-aware fragment of XPath and of the implication problem for unary key and inclusion constraints is concluded.
- N. Alon, T. Milo, F. Neven, D. Suciu and V. Vianu. XML with Data Values: Typechecking Revisited In Journal of Computer and System Sciences, 66(4): 688--727 (2003). Google Scholar
Digital Library
- M. Arenas, W. Fan and L. Libkin. Consistency of XML specifications. In Inconsistency Tolerance, Springer LNCS vol. 3300, 2005, pages 15--41. Google ScholarDigital Library
- M. Benedikt, W. Fan, and F. Geerts. XPath Satisfiability in the Presence of DTDs. In PODS'05, 2005. Google ScholarDigital Library
- M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on words with data. LIAFA research report, available at http://www.liafa.jussieu.fr/web9/rapportrech/description_fr.php?idrapportrech=678Google Scholar
- P. Bouyer, A. Petit and D. Thérien. An algebraic approach to data languages and timed languages. Inf. Comput., 182(2): 137--162 (2003). Google ScholarDigital Library
- P. Buneman, S. B. Davidson, W. Fan, C. S. Hara, W. C. Tan. Reasoning about keys for XML. In Inf. Syst., 28(8): 1037--1063 (2003). Google ScholarDigital Library
- J. Cristau, C. Löding, W. Thomas. Deterministic Automata on Unranked Trees. In Proceedings of the 15th International Symposium on Fundamentals of Computation Theory (FCT), LNCS (to appear), 2005. Google ScholarDigital Library
- C. David. Mots et données infinis. Master's thesis, Université Paris 7, LIAFA, 2004.Google Scholar
- P. de Groote, B. Guillaume, and S. Salvati. Vector Addition Tree Automata. In LICS'04, pp. 64--73, 2004. Google ScholarDigital Library
- S. Demri, R. Lazic, D. Nowak. On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. In TIME'05, 2005. Google ScholarDigital Library
- K. Etessami, M.Y. Vardi, and Th. Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Inf. Comput., 179(2): 279--295 (2002). Google ScholarDigital Library
- F. Geerts and W. Fan. Satisfiability of XPath Queries with Sibling Axes. In DBPL'05, 2005. Google ScholarDigital Library
- G. Gottlob, C. Koch, and R. Pichler. Efficient Algorithms for Processing XPath Queries. In VLDB, 2002. Google ScholarDigital Library
- E. Grädel and M. Otto. On Logics with Two Variables. Theor. Comp. Sci., 224:73--113 (1999). Google ScholarDigital Library
- M. Kaminski and N. Francez. Finite memory automata. Theor. Comp. Sci., 134(2):329--363 (1994). Google ScholarDigital Library
- E. Kieroński and M. Otto. Small Substructures and Decidability Issues for First-Order Logic with Two Variables. In LICS'05, 2005. Google ScholarDigital Library
- W. Martens, J. Niehren. Minimizing Tree Automata for Unranked Trees. In 10th International Symposium on Database Programming Languages, LNCS 3774, 2005. Google ScholarDigital Library
- M. Marx. First order paths in ordered trees. In ICDT'05, 2005. Google ScholarDigital Library
- M. Mortimer. On languages with two variables. Zeitschr. f. math. Logik u. Grundlagen d. Math., 21: 135--140 (1975).Google Scholar
- F. Neven and T. Schwentick. XPath Containment in the Presence of Disjunction, DTDs, and Variables. In ICDT'03, 2003. Google ScholarDigital Library
- K. Neeraj Verma, H. Seidl, T. Schwentick. On the Complexity of Equational Horn Clauses. In CADE'05, 2005. Google ScholarDigital Library
- F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 15(3): 403--435 (2004). Google ScholarDigital Library
- XML Path Language (XPath), W3C Recommendation 16 November 1999. Available at http://www.w3.org/TR/xpath.Google Scholar
Index Terms
- Two-variable logic on data trees and XML reasoning
Recommendations
Principles of dataspace systems
PODS '06: Proceedings of the twenty-fifth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systemsThe most acute information management challenges today stem from organizations relying on a large number of diverse, interrelated data sources, but having no means of managing them in a convenient, integrated, or principled fashion. These challenges ...
Two-variable logic on data trees and XML reasoning
Motivated by reasoning tasks for XML languages, the satisfiability problem of logics on data trees is investigated. The nodes of a data tree have a label from a finite set and a data value from a possibly infinite set. It is shown that satisfiability ...
Comments