A Sequent Calculus for a Modal Logic on Finite Data Trees

Authors David Baelde, Simon Lunel, Sylvain Schmitz

Thumbnail PDF


  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

David Baelde
Simon Lunel
Sylvain Schmitz

Cite AsGet BibTex

David Baelde, Simon Lunel, and Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e., over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.
  • XPath
  • proof systems
  • modal logic
  • complexity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Sergio Abriola, María Emilia Descotte, Raul Fervari, and Santiago Figueira. Axiomatizations for downward XPath on data trees. Preprint, 2016. URL: http://arxiv.org/abs/1605.04271.
  2. Arnon Avron. On modal systems having arithmetical interpretations. J. Symb. Log., 49(3):935-942, 1984. URL: http://dx.doi.org/10.2307/2274147.
  3. Michael Benedikt, Wenfei Fan, and Floris Geerts. XPath satisfiability in the presence of DTDs. Journal of the ACM, 55(2):1-79, 2008. URL: http://dx.doi.org/10.1145/1346330.1346333.
  4. Michael Benedikt, Wenfei Fan, and Gabriel Kuper. Structural properties of XPath fragments. Theor. Comput. Sci., 336(1):3-31, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.10.030.
  5. Michael Benedikt and Christoph Koch. XPath leashed. ACM Computing Surveys, 41(1):3:1-3:54, 2009. URL: http://dx.doi.org/10.1145/1456650.1456653.
  6. Patrick Blackburn, Marteen de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. Google Scholar
  7. Mikołaj Bojańczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. Journal of the ACM, 56(3):1-48, 2009. URL: http://dx.doi.org/10.1145/1516512.1516515.
  8. Kai Brünnler and Lutz Straßburger. Modular sequent systems for modal logic. In Tableaux 2009, volume 5607 of LNCS, pages 152-166. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02716-1_12.
  9. A. V. Chagrov and M. N. Rybakov. How many variables does one need to prove PSPACE-hardness of modal logics? In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, AiML 2002, pages 71-82. King’s College Publications, 2003. Google Scholar
  10. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114-133, 1981. URL: http://dx.doi.org/10.1145/322234.322243.
  11. Diego Figueira. Alternating register automata on finite words and trees. Logic. Meth. in Comput. Sci., 8(1):1-43, 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:22)2012.
  12. Diego Figueira. Decidability of downward XPath. ACM Trans. Comput. Logic, 13(4):1-40, 2012. URL: http://dx.doi.org/10.1145/2362355.2362362.
  13. Diego Figueira. On XPath with transitive axes and data tests. In PODS 2013, pages 249-260. ACM, 2013. URL: http://dx.doi.org/10.1145/2463664.2463675.
  14. Diego Figueira, Santiago Figueira, and Carlos Areces. Model theory of XPath on data trees. Part I: bisimulation and characterization. J. Artif. Intell. Res., 53(1):271-314, 2015. URL: http://dx.doi.org/10.1613/jair.4658.
  15. Diego Figueira and Luc Segoufin. Bottom-up automata on data trees and vertical XPath. In STACS 2011, volume 9 of LIPIcs, pages 93-104. LZI, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2011.93.
  16. Andrzej Indrzejczak. Linear time in hypersequent framework. Bull. Symb. Logic, 22(1):121-144, 2016. URL: http://dx.doi.org/10.1017/bsl.2016.2.
  17. M. Jurdziński and R. Lazić. Alternating automata on data trees and XPath satisfiability. ACM Trans. Comput. Logic, 12(3):1-21, 2011. URL: http://dx.doi.org/10.1145/1929954.1929956.
  18. Emmanuel Kieroński and Lidia Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In LICS 2009, pages 123-132, 2009. URL: http://dx.doi.org/10.1109/LICS.2009.39.
  19. Simon Lunel. Systèmes de preuves pour logiques modales à données. Mémoire de Master, LMFI, Université Paris-Diderot, September 2015. Google Scholar
  20. Sara Negri. Proof analysis in modal logic. J. Phil. Log., 34(5-6):507-544, 2005. URL: http://dx.doi.org/10.1007/s10992-005-2267-3.
  21. Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In David Makinson, Jacek Malinowski, and Heinrich Wansing, editors, Towards Mathematical Philosophy, volume 28 of Trends in Logic, pages 31-51. Springer, 2009. URL: http://dx.doi.org/10.1007/978-1-4020-9084-4_3.
  22. Jonathan Robie, Don Chamberlin, Michael Dyck, and John Snelson. XML Path Language (XPath) 3.0. W3C Recommendation, World Wide Web Consortium (W3C), 2014. URL: http://www.w3.org/TR/xpath-30/.
  23. Balder ten Cate, Gaëlle Fontaine, and Tadeusz Litak. Some modal aspects of XPath. J. Appl. Non-Classical Log., 20(3):139-171, 2010. URL: http://dx.doi.org/10.3166/jancl.20.139-171.
  24. Balder ten Cate, Tadeusz Litak, and Maarten Marx. Complete axiomatizations for XPath fragments. J. Appl. Logic, 8(2):153-172, 2010. URL: http://dx.doi.org/10.1016/j.jal.2009.09.002.
  25. Balder ten Cate and Maarten Marx. Axiomatizing the logical core of XPath 2.0. Theor. Comput. Sys., 44(4):561-589, 2009. URL: http://dx.doi.org/10.1007/s00224-008-9151-9.
  26. Heinrich Wansing. Sequent calculi for normal modal propositional logics. J. Logic Comput., 4(2):125-142, 1994. URL: http://dx.doi.org/10.1093/logcom/4.2.125.