Skip to Main content Skip to Navigation
New interface
Conference papers

A Sequent Calculus for a Modal Logic on Finite Data Trees

David Baelde 1 Simon Lunel 2 Sylvain Schmitz 1, 3 
2 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : David Baelde Connect in order to contact the contributor
Submitted on : Monday, September 7, 2015 - 4:58:03 PM
Last modification on : Saturday, June 25, 2022 - 7:40:18 PM
Long-term archiving on: : Wednesday, April 26, 2017 - 3:31:31 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License



David Baelde, Simon Lunel, Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. CSL 2016, Sep 2016, Marseille, France. pp.1--16, ⟨10.4230/LIPIcs.CSL.2016.32⟩. ⟨hal-01191172v2⟩



Record views


Files downloads