The mu-calculus is obtained from basic modal logic by adding least and greatest fixpoint operators. By doing so a lot of expressive power is added to the logic. However, the semantics can only be evaluated over labelled transition systems. Coalgebraic modal logic generalizes the basic modal logic and lets us evaluate the semantics over different coalgebras, instead of only labelled transition systems. In the coalgebraic mu-calculus, the expressive power of the mu-calculus and the generality of coalgebraic modal logic are combined.

In this talk we will introduce the coalgebraic mu-calculus and how to handle proof systems for this family of logics.