[Zurück]

B. Afshari:
"On the logic of induction and co-induction";
Vortrag: Gothenburg Logic Seminar, Gothenburg, Schweden (eingeladen); 12.10.2016.

Modal mu-calculus is the extension of propositional modal logic by constructors for fixed points of inductive and co-inductive definitions. Semantically, the logic acquires much of the expressive power of second-order logic over graphs. Syntactically, however, the calculus remains weak as almost all natural questions for this logic (satisfiability, validity, model checking) are decidable. This contrast together with the ubiquity of inductive definitions in formal reasoning has established modal mu-calculus as an important system in both mathematical logic and theoretical computer science. In this talk I will introduce mu-calculus, highlight key proof- and model-theoretic properties, and give recent results on finitary proof systems for the calculus.