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], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Communication dans un congrès
Jean-Marc Talbot; Laurent Regnier. CSL 2016, Sep 2016, Marseille, France. LZI, 62 (32), pp.1--16, Leibniz International Proceedings in Informatics. 〈10.4230/LIPIcs.CSL.2016.32〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01191172
Contributeur : David Baelde <>
Soumis le : lundi 7 septembre 2015 - 16:58:03
Dernière modification le : mercredi 2 août 2017 - 10:08:18
Document(s) archivé(s) le : mercredi 26 avril 2017 - 15:31:31

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

Citation

David Baelde, Simon Lunel, Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. Jean-Marc Talbot; Laurent Regnier. CSL 2016, Sep 2016, Marseille, France. LZI, 62 (32), pp.1--16, Leibniz International Proceedings in Informatics. 〈10.4230/LIPIcs.CSL.2016.32〉. 〈hal-01191172v2〉

Partager

Métriques

Consultations de la notice

475

Téléchargements de fichiers

245