Abstract
In this paper we introduce a sound and complete axiomatization for XPath with data constraints extended with hybrid operators. First, we define \(\text {HXPath} _=({{\uparrow }{\downarrow }})\), an extension of vertical XPath with nominals and the hybrid operator @. Then, we introduce an axiomatic system for \(\text {HXPath} _=({{\uparrow }{\downarrow }})\), 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abriola, S., Descotte, M., Fervari, R., Figueira, S.: Axiomatizations for downward XPath on data trees. CoRR, abs/1605.04271 (2016)
Abriola, S., Descotte, M., Figueira, S.: Model theory of XPath on data trees. Part II: Binary bisimulation and definability. Information and Computation (to appear). http://www.glyc.dc.uba.ar/santiago/papers/xpath-part2.pdf
Abriola, S., Descotte, M.E., Figueira, S.: Definability for downward and vertical XPath on data trees. In: Kohlenbach, U., Barceló, P., Queiroz, R. (eds.) WoLLIC 2014. LNCS, vol. 8652, pp. 20–35. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44145-9_2
Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp. 821–868. Elsevier, Amsterdam (2006)
Baelde, D., Lunel, S., Schmitz, S.: A sequent calculus for a modal logic on finite data trees. In: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, pp. 32:1–32:16 (2016)
Benedikt, M., Fan, W., Geerts, F.: XPath satisfiability in the presence of DTDs. J. ACM 55(2), 1–79 (2008)
Benedikt, M., Koch, C.: XPath leashed. ACM Comput. Surv. 41(1), 1–54 (2008)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001)
Blackburn, P., ten Cate, B.: Pure extensions, proof rules, and hybrid axiomatics. Studia Logica 84(2), 277–322 (2006)
Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: van Benthem, J., Blackburn, P., Wolter, F. (eds.) Handbook of Modal Logic, pp. 1–84. Elsevier, Amsterdam (2006)
Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and XML reasoning. J. ACM 56(3), 1–48 (2009)
ten Cate, B., Litak, T., Marx, M.: Complete axiomatizations for XPath fragments. J. Appl. Logic 8(2), 153–172 (2010)
ten Cate, B., Marx, M.: Axiomatizing the logical core of XPath 2.0. Theory Comput. Syst. 44(4), 561–589 (2009)
Clark, J., DeRose, S.: XML path language (XPath). Website. W3C Recommendation (1999). http://www.w3.org/TR/xpath
Figueira, D.: Reasoning on words and trees with data. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France (2010)
Figueira, D.: Decidability of downward XPath. ACM Trans. Comput. Logic 13(4), 34 (2012)
Figueira, D., Figueira, S., Areces, C.: Basic model theory of XPath on data trees. In: International Conference on Database Theory, pp. 50–60 (2014)
Figueira, D., Figueira, S., Areces, C.: Model theory of XPath on data trees. Part I: Bisimulation and characterization. J. Artif. Intell. Res. 53, 271–314 (2015)
Figueira, D., Segoufin, L.: Bottom-up automata on data trees and vertical XPath. In: 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011), pp. 93–104 (2011)
Gottlob, G., Koch, C., Pichler, R.: Efficient algorithms for processing XPath queries. ACM Trans. Database Syst. 30(2), 444–491 (2005)
Kostylev, E., Reutter, J., Vrgoč, D.: Xpath for DL ontologies. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI 2015, pp. 1525–1531. AAAI Press (2015)
Marx, M.: XPath with conditional axis relations. In: Bertino, E., Christodoulakis, S., Plexousakis, D., Christophides, V., Koubarakis, M., Böhm, K., Ferrari, E. (eds.) EDBT 2004. LNCS, vol. 2992, pp. 477–494. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24741-8_28
Marx, M., de Rijke, M.: Semantic characterizations of navigational XPath. ACM SIGMOD Rec. 34(2), 41–46 (2005)
Sattler, U., Vardi, M.Y.: The hybrid \({\mu }\)-calculus. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 76–91. Springer, Heidelberg (2001). doi:10.1007/3-540-45744-5_7
Acknowledgments
This work was partially supported by grant ANPCyT-PICT-2013-2011, STIC-AmSud “Foundations of Graph Structured Data (FoG)” and the Laboratoire International Associé “INFINIS.”
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Areces, C., Fervari, R. (2016). Hilbert-Style Axiomatization for Hybrid XPath with Data. In: Michael, L., Kakas, A. (eds) Logics in Artificial Intelligence. JELIA 2016. Lecture Notes in Computer Science(), vol 10021. Springer, Cham. https://doi.org/10.1007/978-3-319-48758-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-48758-8_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48757-1
Online ISBN: 978-3-319-48758-8
eBook Packages: Computer ScienceComputer Science (R0)