Skip to main content
SpringerLink
Log in

Tableaux for Hybrid XPath with Data

  • Conference paper
  • First Online:
Progress in Artificial Intelligence (EPIA 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10423))

Included in the following conference series:

Abstract

We provide a sound, complete and terminating tableau procedure to check satisfiability of downward XPath\(_=\) formulas enriched with nominals and satisfaction operators. The calculus is inspired by ideas introduced to ensure termination of tableau calculi for certain Hybrid Logics. We prove that even though we increased the expressive power of XPath by introducing hybrid operators, the satisfiability problem for the obtained logic is still PSpace-complete.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    The well-ordered condition will be used to prove termination.

  2. 2.

    For a detailed introduction, see [3].

  3. 3.

    Some readers may call this notion “completeness”, and the one introduced in the next section “soundness”. However, we use the classical tableaux denomination.

References

  1. Abriola, S., Descotte, M., Fervari, R., Figueira, S.: Axiomatizations for downward XPath on data trees. J. Comput. Syst. Sci. (2017, in press)

    Google Scholar 

  2. Abriola, S., Descotte, M., Figueira, S.: Model theory of XPath on data trees. Part II: binary bisimulation and definability. Inf. Comput. (to appear). http://www.glyc.dc.uba.ar/santiago/papers/xpath-part2.pdf

  3. Areces, C., Fervari, R.: Hilbert-style axiomatization for hybrid XPath with data. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS, vol. 10021, pp. 34–48. Springer, Cham (2016). doi:10.1007/978-3-319-48758-8_3

    Chapter  Google Scholar 

  4. 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)

    Google Scholar 

  5. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001)

    Book  Google Scholar 

  6. Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, pp. 1–84. Elsevier (2006)

    Google Scholar 

  7. Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and XML reasoning. J. ACM 56(3), 13 (2009)

    Article  MathSciNet  Google Scholar 

  8. Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Log. Comput. 17(3), 517–554 (2007)

    Article  MathSciNet  Google Scholar 

  9. Buneman, P.: Semistructured data. In: ACM Symposium on Principles of Database Systems (PODS 1997), pp. 117–121 (1997)

    Google Scholar 

  10. ten Cate, B., Litak, T., Marx, M.: Complete axiomatizations for XPath fragments. J. Appl. Log. 8(2), 153–172 (2010)

    Article  MathSciNet  Google Scholar 

  11. Clark, J., DeRose, S.: XML path language (XPath). W3C Recommendation (1999). http://www.w3.org/TR/xpath

  12. D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.): Handbook of Tableau Methods. Springer, Heidelberg (1999)

    MATH  Google Scholar 

  13. Figueira, D.: Decidability of downward XPath. ACM Trans. Comput. Log. 13(4), 34 (2012)

    Article  MathSciNet  Google Scholar 

  14. Figueira, D.: On XPath with transitive axes and data tests. In: Fan, W. (ed.) ACM Symposium on Principles of Database Systems (PODS 2013), pp. 249–260. ACM Press, New York (2013)

    Google Scholar 

  15. 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)

    Article  MathSciNet  Google Scholar 

  16. Gottlob, G., Koch, C., Pichler, R.: Efficient algorithms for processing XPath queries. ACM Trans. Database Syst. 30(2), 444–491 (2005)

    Article  Google Scholar 

Download references

Acknowledgements

This work was partially supported by grant ANPCyT-PICT-2013-2011, STIC-AmSud “Foundations of Graph Structured Data (FoG)”, SeCyT-UNC, the Laboratoire International Associé “INFINIS”, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skodowska-Curie grant agreement No. 690974 for the project MIREL: MIning and REasoning with Legal texts.

Author information

Authors and Affiliations

  1. FaMAF, Universidad Nacional de Córdoba, Córdoba, Argentina

    Carlos Areces, Raul Fervari & Nahuel Seiler

  2. CONICET, Córdoba, Argentina

    Carlos Areces & Raul Fervari

Authors
  1. Carlos Areces
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raul Fervari
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nahuel Seiler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Raul Fervari .

Editor information

Editors and Affiliations

  1. Universidade do Porto, Porto, Portugal

    Eugénio Oliveira

  2. Universidade do Porto, Porto, Portugal

    João Gama

  3. Polytechnic Institute of Porto, Porto, Portugal

    Zita Vale

  4. Universidade do Porto, Porto, Portugal

    Henrique Lopes Cardoso

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Areces, C., Fervari, R., Seiler, N. (2017). Tableaux for Hybrid XPath with Data. In: Oliveira, E., Gama, J., Vale, Z., Lopes Cardoso, H. (eds) Progress in Artificial Intelligence. EPIA 2017. Lecture Notes in Computer Science(), vol 10423. Springer, Cham. https://doi.org/10.1007/978-3-319-65340-2_50

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65340-2_50

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65339-6

  • Online ISBN: 978-3-319-65340-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation