Tableau method and NEXPTIME-Completeness of DEL-SequentsReportar como inadecuado




Tableau method and NEXPTIME-Completeness of DEL-Sequents - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.





Autor: Guillaume Aucher - Bastien Maubert - François Schwarzentruber -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados