2016年12月6日，Malvin Gattinger教授应邀在一教105室进行了题目为“Craig Interpolation for PDL”的学术讲座。讲座的主要内容如下：

If A implies B, then there is a C which only uses the common vocabulary of A and B such that A implies C and C implies B. This property is called Craig Interpolation and it has been shown for many logics, including ?rst-order logic, di?erent modal logics and the mu-calculus. For Propositional Dynamic Logic (PDL) however, the question is still open, according to textbooks and recent papers. On the other hand, at least three proofs have been written, two of them published and only one of those o?cially revoked. This talk will ?rst give an introduction to Interpolation and discuss how to prove it for propositional and ?rst-order logic. We will then highlight the challenges in showing Craig Interpolation for PDL and give a historical overview of the attempts so far. Special attention will be given to a proof by Leivant (1981) which apparently was put aside after it was criticized by Kracht (1999). We will argue that the proof can be repaired to answer this criticism and present it in modern notation. The talk will be accessible for everyone who has a background in modal logic and is not afraid of typewriters and stars.