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 I (Winter 2008/09) | 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 |
| Einführung | Automatisierte Logik II | ps pdf anim |
| Teil III: Automatisierung des formalen Schliessens | ||
| Einheit 11: | Interaktive Beweisassistenten | ps pdf anim |
| Einheit 12: | Taktiken: Benutzerdefinierbare Beweisstrategien | ps pdf anim |
| Einheit 13: | Entscheidungsprozeduren | ps pdf anim |
| Einheit 14: | Beweisautomatisierung für die Logik erster Stufe | ps pdf anim |
| Einheit 15: | Formalisierung mathematischen Wissens | ps pdf anim |
| Einheit 16: | Anwendungsbeispiele | ps pdf anim |
| Teil IV: Programmsynthese | ||
| Einheit 17: | Paradigmen und Strategien | ps pdf anim |
| Einheit 18: | Synthese von Divide & Conquer Algorithmen | ps pdf anim |
| Einheit 19: | Synthese von Globalsuch-Algorithmen | ps pdf anim |
| Einheit 20: | Synthese von Problemreduktionsgeneratoren | ps pdf anim |
| Einheit 21: | Synthese von Lokalsuch-Algorithmen | ps pdf anim |
| Einheit 22: | Optimierung schematisch erzeugter Algorithmen | ps pdf anim |
| Einheit 23: | Rückblick und Ausblick | ps pdf anim |
