Hilbert-style Axiomatization for Hybrid XPath with Data

C. Areces and R. Fervari. Hilbert-style Axiomatization for Hybrid XPath with Data. In Proceedings of the 15th European Conference On Logics In Artificial Intelligence (JELIA'2016), Larnaca, Cyprus, 2016.

Download

[pdf] 

Abstract

In this paper we introduce a sound and complete axiomatization for XPath with data constraints extended with hybrid operators. First, we define HXPath_=(\down\up), an extension of vertical XPath with nominals and the hybrid operator @. Then, we introduce an axiomatic system for HXPath_=(\down\up), and we prove it is complete with respect to the class of abstract data trees, i.e., data trees in which data values are abstracted as equivalence relations. As a corollary, we also obtain completeness with respect to the class of concrete data trees.

BibTeX

@InCollection{Areces2016,
  author =       "C. Areces and R. Fervari",
  booktitle =    "Proceedings of the 15th European Conference On Logics
                 In Artificial Intelligence (JELIA'2016)",
  title =        "Hilbert-style Axiomatization for Hybrid {XP}ath with
                 Data",
  year =         "2016",
  address =      "Larnaca, Cyprus",
  abstract =     "In this paper we introduce a sound and complete
                 axiomatization for XPath with data constraints extended
                 with hybrid operators. First, we define
                 HXPath_=(\down\up), an extension of vertical XPath with
                 nominals and the hybrid operator @. Then, we introduce
                 an axiomatic system for HXPath_=(\down\up), and we
                 prove it is complete with respect to the class of
                 abstract data trees, i.e., data trees in which data
                 values are abstracted as equivalence relations. As a
                 corollary, we also obtain completeness with respect to
                 the class of concrete data trees.",
  owner =        "areces",
  timestamp =    "2016.09.30",
  ISBN =         "978-3-319-48757-1",
}