Die Folien der Veranstaltung werden in zwei Versionen bereitgestellt. Die normalen ps und pdf Files enthalten eine Druckversion der Folien ohne eventuell benutzte "Animationen". Das anim file enthält die vollständige PDF Version mit Animationen.
| Einführung | Automatisierte Logik | ps pdf anim |
| Teil I: Formalisierung | ||
| Einheit 2: | Grundkonzepte formaler Kalküle | ps pdf anim |
| Einheit 3: | Refinement Logic | ps pdf anim |
| Einheit 4: | Interaktive Beweisführung | ps pdf anim |
| Einheit 5: | Lambda-Kalkül | ps pdf anim |
| Einheit 6: | Die einfache Typentheorie | ps pdf anim |
| Einheit 7: | Abhängige Datentypen | ps pdf anim |
| Teil II: Konstruktive Typentheorie | ||
| Einheit 8: | Systematik des Aufbaus formaler Theorien | ps pdf anim |
| Einheit 9: | Logik und Programmierung in der Typentheorie | ps pdf anim |
| Einheit 10: | Fortgeschrittene Konzepte der CTT | ps pdf anim |
| Teil III: Automatisierung des formalen Schliessens | ||
| Teil IV: Programmsynthese | ||
