Fixpoints and Induction in Logic and Computer Science

 

Lecture in the summer term 2022

 
fixpoints on a lattice
 

Dates

Lecture:

 

Exercise Class:
 

 
 

Content


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, probability theory (Markov chains and decision processes), program semantics and verification, automata theory and formal languages
  • Computation of fixpoints by iteration on finite lattices
  • Characterization of fixpoints on infinite lattices for continuous functions and arbitrary functions
  • Ordinal numbers, transfinite induction, well-ordering theorem
  • First-order logic with fixpoints
  • The role of induction in incompleteness theorem for Peano arithmetic

Prerequisites

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.

 

Organization

Time and Places

Lecturer

Christof Löding

 

Exam

It is planned ot have oral exams for the course. Depending on the number of students it might also be a written exam.

 

External Links