Tableau method and NEXPTIME-Completeness of DEL-Sequents

Guillaume Aucher 1 Bastien Maubert 2 François Schwarzentruber 1
1 DISTRIBCOM - Distributed and Iterative Algorithms for the Management of Telecommunications Systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Dynamic Epistemic Logic (DEL) deals with the representation of situations in a multi-agent and dynamic setting. It can express in a uniform way statements about: (i) what is true about an initial situation (ii) what is true about an event occurring in this situation (iii) what is true about the resulting situation after the event has occurred. After proving that what we can infer about (ii) given (i) and (iii) and what we can infer about (i) given (ii) and (iii) are both reducible to what we can infer about (iii) given (i) and (ii), we provide a tableau method deciding whether such an inference is valid. We implement it in LOTRECscheme and show that this decision problem is NEXPTIME-complete. This contributes to the proof theory and the study of the computational complexity of DEL which have rather been neglected so far.
Type de document :
Communication dans un congrès
Methods for Modalities (M4M), Nov 2011, Sevilla, Spain. Elsevier, 2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00627642
Contributeur : Guillaume Aucher <>
Soumis le : mercredi 30 novembre 2011 - 08:42:25
Dernière modification le : mercredi 16 mai 2018 - 11:23:04
Document(s) archivé(s) le : jeudi 1 mars 2012 - 02:25:15

Fichier

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

Identifiants

  • HAL Id : inria-00627642, version 2

Citation

Guillaume Aucher, Bastien Maubert, François Schwarzentruber. Tableau method and NEXPTIME-Completeness of DEL-Sequents. Methods for Modalities (M4M), Nov 2011, Sevilla, Spain. Elsevier, 2011. 〈inria-00627642v2〉

Partager

Métriques

Consultations de la notice

473

Téléchargements de fichiers

120