epistemic logics can express properties of programs and distributed system protocols. The modalities of epistemic logics encode attitudes such as knowledge and belief, but dynamic changes to these attitudes, after actions such as announcements, have traditionally been formalised only in a semantic fashion. Adding epistemic modalities to dynamic logics led to logics allowing reasoning about belief updates, both syntactically and semantically. But, lacking cut-admissibility, the calculus proposed in [?] is not a basis for automatic proof search. As always, the presence of a cut rule would ensure infinite non-determinism in proof search, so we have to avoid it; its admissibility is however important for completeness. Likewise, we incorporate weakening and contraction into our logical rules (while ensuring for completeness’ sake that they are admissible) rather than having them as primitive, thus reducing the non-determinism even further. Here we develop a cut-free sequent calculus as basis for a proof search procedure for one such logic.