Axiomatizations for downward XPath on data trees

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 over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Abriola, S., Descotte, M.E., Fervari, R., Figueira, S.
Formato: JOUR
Materias:
Axiomatization
Data tree
Modal logic
Normal form
Query language
XML
XPath
Computer circuits
Query languages
Trees (mathematics)
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_00220000_v89_n_p209_Abriola
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_00220000_v89_n_p209_Abriola
record_format dspace
spelling todo:paper_00220000_v89_n_p209_Abriola2023-10-03T14:25:23Z Axiomatizations for downward XPath on data trees Abriola, S. Descotte, M.E. Fervari, R. Figueira, S. Axiomatization Data tree Modal logic Normal form Query language XML XPath Computer circuits Query languages XML Axiomatization Data tree Modal logic Normal form XPath Trees (mathematics) 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 over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e. there is no comparison by constants). Our axioms are in the style of equational logic, extending the 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 simpler fragment with ‘equality’ tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests. © 2017 Elsevier Inc. Fil:Figueira, S. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00220000_v89_n_p209_Abriola
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Axiomatization
Data tree
Modal logic
Normal form
Query language
XML
XPath
Computer circuits
Query languages
XML
Axiomatization
Data tree
Modal logic
Normal form
XPath
Trees (mathematics)
spellingShingle Axiomatization
Data tree
Modal logic
Normal form
Query language
XML
XPath
Computer circuits
Query languages
XML
Axiomatization
Data tree
Modal logic
Normal form
XPath
Trees (mathematics)
Abriola, S.
Descotte, M.E.
Fervari, R.
Figueira, S.
Axiomatizations for downward XPath on data trees
topic_facet Axiomatization
Data tree
Modal logic
Normal form
Query language
XML
XPath
Computer circuits
Query languages
XML
Axiomatization
Data tree
Modal logic
Normal form
XPath
Trees (mathematics)
description 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 over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e. there is no comparison by constants). Our axioms are in the style of equational logic, extending the 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 simpler fragment with ‘equality’ tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests. © 2017 Elsevier Inc.
format JOUR
author Abriola, S.
Descotte, M.E.
Fervari, R.
Figueira, S.
author_facet Abriola, S.
Descotte, M.E.
Fervari, R.
Figueira, S.
author_sort Abriola, S.
title Axiomatizations for downward XPath on data trees
title_short Axiomatizations for downward XPath on data trees
title_full Axiomatizations for downward XPath on data trees
title_fullStr Axiomatizations for downward XPath on data trees
title_full_unstemmed Axiomatizations for downward XPath on data trees
title_sort axiomatizations for downward xpath on data trees
url http://hdl.handle.net/20.500.12110/paper_00220000_v89_n_p209_Abriola
work_keys_str_mv AT abriolas axiomatizationsfordownwardxpathondatatrees
AT descotteme axiomatizationsfordownwardxpathondatatrees
AT fervarir axiomatizationsfordownwardxpathondatatrees
AT figueiras axiomatizationsfordownwardxpathondatatrees
_version_ 1782030556145385472

Ejemplares similares