ICC   25427
INSTITUTO DE INVESTIGACION EN CIENCIAS DE LA COMPUTACION
Unidad Ejecutora - UE
artículos
Título:
Axiomatizations for downward XPath on Data Trees
Autor/es:
FERVARI, RAUL; DESCOTTE, MAR√ćA EMILIA; ABRIOLA, SERGIO; FIGUEIRA, SANTIAGO
Revista:
JOURNAL OF COMPUTER AND SYSTEM SCIENCES
Editorial:
ACADEMIC PRESS INC ELSEVIER SCIENCE
Referencias:
Lugar: Amsterdam; Año: 2017
ISSN:
0022-0000
Resumen:
We give sound and complete axiomatizations for XPath with data tests by ?equality?or ?inequality?, and containing the single ?child? axis. This data-aware logic predicts overdata trees, which are tree-like structures whose every node contains a label from a finitealphabet and a data value from an infinite domain. The language allows us to comparedata values of two nodes but cannot access the data values themselves (i.e. there is nocomparison by constants). Our axioms are in the style of equational logic, extendingthe axiomatization of data-oblivious XPath, by B. ten Cate, T. Litak and M. Marx.We axiomatize the full logic with tests by ?equality? and ?inequality?, and also a simplerfragment with ?equality? tests only. Our axiomatizations apply both to node expressionsand path expressions. The proof of completeness relies on a novel normal form theoremfor XPath with data tests.