Technical University of Denmark
Abstract: Dynamic Epistemic Logic (DEL) deals with the representation and the
study in a multi-agent setting of knowledge and belief change.
It can express
in a uniform way epistemic statements about:
\begin{enumerate}
\item[(i)]
what is true about an initial situation
\item[(ii)] what is true about an
event occurring in this situation
\item[(iii)] what is true about the
resulting situation after the event has occurred.
\end{enumerate}
We
axiomatize within the DEL framework what we can infer about (iii) given (i) and
(ii), what we can infer about (ii) given (i) and (iii), and what we can infer
about (i) given (ii) and (iii). These three inference problems are related to
classical problems addressed under different guises in artificial intelligence
and theoretical computer science, which we call respectively progression,
epistemic planning and regression. Given three formulas $\phi$, $\phi'$ and
$\phi''$ describing respectively (i), (ii) and (iii), we also show how to build
three formulas $\phi\otimes\phi'$, $\phi\varoslash\phi''$ and
$\phi'\varobslash\phi''$ which capture respectively all the information which
can be inferred about (iii) from $\phi$ and $\phi'$, all the information which
can be inferred about (ii) from $\phi$ and $\phi''$, and all the information
which can be inferred about (i) from $\phi'$ and $\phi''$. We show how our
results extend to other modal logics than $\logicK$. In our proofs and
definitions, we resort to a large extent to the normal form formulas for modal
logic originally introduced by Kit Fine.