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

Detalles Bibliográficos
Autor principal: Figueira, Santiago Daniel
Publicado: 2017
Materias:
Axiomatization
Data tree
Modal logic
Normal form
Query language
XML
XPath
Computer circuits
Query languages
Trees (mathematics)
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00220000_v89_n_p209_Abriola
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 paper:paper_00220000_v89_n_p209_Abriola
record_format dspace
spelling paper:paper_00220000_v89_n_p209_Abriola2023-06-08T14:45:04Z Axiomatizations for downward XPath on data trees Figueira, Santiago Daniel 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. 2017 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00220000_v89_n_p209_Abriola 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)
Figueira, Santiago Daniel
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.
author Figueira, Santiago Daniel
author_facet Figueira, Santiago Daniel
author_sort Figueira, Santiago Daniel
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
publishDate 2017
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00220000_v89_n_p209_Abriola
http://hdl.handle.net/20.500.12110/paper_00220000_v89_n_p209_Abriola
work_keys_str_mv AT figueirasantiagodaniel axiomatizationsfordownwardxpathondatatrees
_version_ 1768545724198289408

Ejemplares similares