### Introduction

The lecture is blocked. Instead of a weekly 1-hour lecture, there will be 4 sessions of 3 hours each. Related courses to some of the discussed topics are given in parentheses.

session 1: | formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming) |

session 2: | simplification (term rewriting), function definitions, induction, calculational reasoning |

session 3: | natural deduction, propositional logic, predicate logic (logic) |

session 4: | (inductively defined) sets, relations, advanced topics, |