zbMATH — the first resource for mathematics

Definability for downward and vertical XPath on data trees. (English) Zbl 1317.68038
Kohlenbach, Ulrich (ed.) et al., Logic, language, information, and computation. 21st international workshop, WoLLIC 2014, Valparaíso, Chile, September 1–4, 2014. Proceedings. Berlin: Springer (ISBN 978-3-662-44144-2/pbk). Lecture Notes in Computer Science 8652, 20-35 (2014).
Summary: We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over data trees. We give necessary and sufficient conditions for a class of pointed data trees to be definable by a set of formulas or by a single formula of each of the studied logics. To do so, we introduce a notion of saturation, and show that over saturated data trees bisimulation coincides with logical equivalence.
For the entire collection see [Zbl 1295.03005].

68P05 Data structures
03B70 Logic in computer science
Full Text: DOI