TU Wien:Automated Deduction VU (Laura Kovács)
- Automated Deduction VU (Kovacs) (TU Wien, 0 Materialien)
- Automated Deduction VU (Laura Kovács) (TU Wien, veraltet, 4 Materialien)
Daten[Bearbeiten | Quelltext bearbeiten]
| Vortragende | Prof. Laura Kovács |
|---|---|
| ECTS | 6 |
| Sprache | English |
| Links | tiss:184774 , Homepage |
| Masterstudium Logic and Computation | |
| Masterstudium Software Engineering & Internet Computing | |
| Masterstudium Technische Informatik |
Mattermost: Channel "automated-deduction" • Register • Mattermost-Infos
Inhalt[Bearbeiten | Quelltext bearbeiten]
Unterteilt in drei Gebiete: Zuerst SAT, dann SMT, dann Theorem Proving. Es wird jeweils kurz das Problem erklärt und dann auf Algorithmen zur Lösung eingegangen (Splitting, DPLL, Congruence Closure, Nelson-Oppen, Superposition). Fokus liegt klar auf den Algorithmen und deren Anwendung. Beweise kommen nur hin und wieder vor.
Ablauf[Bearbeiten | Quelltext bearbeiten]
Geblockte Vorlesung im Oktober und November (2*2 Einheiten pro Woche). Mitte Dezember eine schriftliche Prüfung (60 % der Note), weitere Prüfungstermine danach werden persönlich vereinbart. Pro Themengebiet ein Übungsblatt (also insgesamt drei, je eines für SAT, SMT und Theorem Proving) die via Email oder bei der Vorlesung abgegeben werden. Die Übungen tragen 40 % zur Note bei.
Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]
Vorwissen in Aussagen- und Prädikatenlogik schadet sicher nicht. Wer mit SAT und vielleicht sogar mit SMT und Binary Resolution/Superposition etwas anfangen kann hat sicher auch einen Vorteil. Prinzipiell wird aber alles erklärt.
Vortrag[Bearbeiten | Quelltext bearbeiten]
Guter Vortrag auf englisch unterstützt durch Folien am Beamer (nach den Vorlesungen auf der Website verfügbar) und Erklärungen/Beispielen/gelegentlich Beweisen an der Tafel. Der Inhalt wird gut erklärt und es ist nicht langweilig. Ich finde es zahlt sich aus, hin zu gehen, aber wenn man keine Zeit hat reicht das Lernen von den Folien bestimmt auch um die Prüfung zu bestehen.
Übungen[Bearbeiten | Quelltext bearbeiten]
Drei Übungsblätter, siehe "Ablauf". Die Aufgaben sind eine Mischung aus Beweisen (alle recht einfach), Anwendung der vorgestellten Algorithmen, Anwendung der vorgestellten Tools und Verständnisfragen (z.B. "Beschreibe die Klasse der Interpretationen, in denen x = a -> x = b gültig ist").
Prüfung, Benotung[Bearbeiten | Quelltext bearbeiten]
Eine Prüfung 60 % der Note, drei Übungsblätter insgesamt 40 % der Note (siehe "Ablauf"). Man durfte man bei der Prüfung ein handgeschriebenes A4 Blatt als "Schummelzettel" benutzen, was gerade bei den Regeln der unterschiedlichen Kalkülen durchaus hilfreich ist.
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
Wenige Tage nach der Prüfung.
Zeitaufwand[Bearbeiten | Quelltext bearbeiten]
Wenn man immer in die Vorlesung geht: 13 * 1.5 h Vorlesung, 3 * 8 h Übung, 24 h lernen für Prüfung für gute Note.
Unterlagen[Bearbeiten | Quelltext bearbeiten]
Folien und Übungsblätter sind auf der Website verfügbar: http://www.cse.chalmers.se/~laurako/links/ADuct.html
Tipps[Bearbeiten | Quelltext bearbeiten]
Bei der Übung die in der Vorlesung vorgestellten Algorithmen genau beachten und nicht irgendwelche Schritte überspringen weil sie "eh klar" sind. Bei der Prüfung gibt es meist eine Mischung aus Anwenden der Algorithmen mit ein bis zwei Beweisen. Bei den unterschiedlichen Terminen wurden zwar die Inhalte der Beispiele geändert, die grundlegende Struktur und Art der Beispiele war jedoch immer gleich.
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
noch offen