Automatisierte Logik und Programmierung II Universität Potsdam, Sommersemester 2006

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 2005/06) 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: Grundkonzepte der Programmsynthese ps pdf anim 
Einheit 18: Synthese im Kleinen: Paradigmen und Strategien ps pdf anim 
Einheit 19: Wissensbasierte Programmentwicklung ps pdf anim 
Einheit 20: Synthese von Divide & Conquer Algorithmen ps pdf anim 
Einheit 21: Synthese von Globalsuch-Algorithmen ps pdf anim 
Einheit 22: Synthese von Lokalsuch-Algorithmen ps pdf anim 
Einheit 23: Optimierung schematisch erzeugter Algorithmen ps pdf anim 
Einheit 24: Rückblick und Ausblick ps pdf anim 
Datenschutzerklärung · XHTML · CSS  Letzte Änderung:  tim at-Zeichen cs Punkt uni-potsdam Punkt de,  05.10.2006