Selected publications at LSV

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.

   address = {Marseille, France},
   author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain},
   booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)},
   DOI = {10.4230/LIPIcs.CSL.2016.32},
   editor = {Regnier, Laurent and Talbot, Jean-Marc},
   month = sep,
   pages = {32:1-32:16},
   publisher = {Leibniz-Zentrum f{\"u}r Informatik},
   series = {Leibniz International Proceedings in Informatics},
   title = {A~Sequent Calculus for a Modal Logic on Finite Data Trees},
   url = {},
   volume = {62},
   year = {2016},

About LSV

Select by Year