Fixpoints and Induction in Logic and Computer Science
Inhalt
This course is about the proof method of induction, and about the theory of fixpoints on ordered structures, complete lattices in particular. Topics covered are:
- Induction on natural numbers, structural induction, well-founded induction
- Tarski's fixpoint theorem for monotonic functions on complete lattices and variations on complete partial orders
- Examples from games, program semantics and verification, automata theory and formal languages, probability theory (Markov chains),
- Computation of fixpoints by iteration on finite lattices
- Characterization of fixpoints on infinite lattices for continuous functions and arbitrary functions
- Modal logic with fixpoints and connection to games
- Ordinal numbers, transfinite induction, well-ordering theorem
- The role of induction in incompleteness theorem for Peano arithmetic
Voraussetzungen
It is assumed that students are familiar with basics in discrete mathematics, automata theory, computability, and mathematical logic, as taught in the corresponding bachelor courses in computer science at RWTH Aachen.
Organisation
Dozent