From interpolation to completeness
Graham E. Leigh, FLoV
I will demonstrate how Walukiewicz’ seminal proof of completeness for the propositional μ-calculus can be derived (and refined) from the cyclic proof theory of the logic, notably the uniform interpolation theorem for the logic.