A Sequent Calculus for a Modal Logic on Finite Data Trees

David Baelde (1) , Simon Lunel (2) , Sylvain Schmitz (1, 3)

1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 TEA - Tim, Events and Architectures
3 DAHU - Verification in databases

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.

Mots clés: XPath; proof systems; modal logic; complexity

Domaines: Logique en informatique [cs.LO]

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⟩