Tableau method and NEXPTIME-Completeness of DEL-Sequents - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Tableau method and NEXPTIME-Completeness of DEL-Sequents

(1) , (2) , (1)
1
2

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.
Fichier principal
Vignette du fichier
M4M11.pdf (183.93 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00627642 , version 1 (29-09-2011)
inria-00627642 , version 2 (30-11-2011)

Identifiers

  • HAL Id : inria-00627642 , version 2

Cite

Guillaume Aucher, Bastien Maubert, François Schwarzentruber. Tableau method and NEXPTIME-Completeness of DEL-Sequents. Methods for Modalities (M4M), Nov 2011, Sevilla, Spain. ⟨inria-00627642v2⟩
188 View
147 Download

Share

Gmail Facebook Twitter LinkedIn More