Axiomatizing Hybrid XPath with Data

C. Areces and R. Fervari. Axiomatizing Hybrid XPath with Data. Logical Methods in Computer Science, 17(3), 2021.

Download

[pdf] 

Abstract

In this paper we introduce sound and strongly complete axiomatizations for XPath with data constraints extended with hybrid operators. First, we present $HXPath_=$, a multi-modal version of XPath with data, extended with nominals and the hybrid operator @. Then, we introduce an axiomatic system for HXPath= , and we prove it is strongly complete with respect to the class of abstract data models, i.e., data models in which data values are abstracted as equivalence relations. We prove a general completeness result similar to the one presented in, e.g., [BtC06], that ensures that certain extensions of the axiomatic system we introduce are also complete. The axiomatic systems that can be obtained in this way cover a large family of hybrid XPath languages over different classes of frames, for which we present concrete examples. In addition, we investigate axiomatizations over the class of tree models, structures widely used in practice. We show that a strongly complete, finitary, first-order axiomatization of hybrid XPath over trees does not exist, and we propose two alternatives to deal with this issue. We finally introduce filtrations to investigate the status of decidability of the satisfiability problem for these languages.

BibTeX

@Article{ArecesF21,
  author =       "C. Areces and R. Fervari",
  ISSN =         "1860-5974",
  journal =      "Logical Methods in Computer Science",
  title =        "Axiomatizing Hybrid {XP}ath with Data",
  year =         "2021",
  number =       "3",
  volume =       "17",
  abstract =     "In this paper we introduce sound and strongly complete
                 axiomatizations for XPath with data constraints
                 extended with hybrid operators. First, we present
                 $HXPath_=$, a multi-modal version of XPath with data,
                 extended with nominals and the hybrid operator @. Then,
                 we introduce an axiomatic system for HXPath= , and we
                 prove it is strongly complete with respect to the class
                 of abstract data models, i.e., data models in which
                 data values are abstracted as equivalence relations. We
                 prove a general completeness result similar to the one
                 presented in, e.g., [BtC06], that ensures that certain
                 extensions of the axiomatic system we introduce are
                 also complete. The axiomatic systems that can be
                 obtained in this way cover a large family of hybrid
                 XPath languages over different classes of frames, for
                 which we present concrete examples. In addition, we
                 investigate axiomatizations over the class of tree
                 models, structures widely used in practice. We show
                 that a strongly complete, finitary, first-order
                 axiomatization of hybrid XPath over trees does not
                 exist, and we propose two alternatives to deal with
                 this issue. We finally introduce filtrations to
                 investigate the status of decidability of the
                 satisfiability problem for these languages.",
  bibsource =    "dblp computer science bibliography, https://dblp.org",
  biburl =       "https://dblp.org/rec/journals/lmcs/ArecesF21.bib",
  doi =          "10.46298/lmcs-17(3:5)2021",
  timestamp =    "Tue, 24 Jan 2023 10:48:24 +0100",
  URL =          "https://doi.org/10.46298/lmcs-17(3:5)2021",
}