TU Wien:Automated Deduction VU (Laura Kovács)

Aus VoWi
Wechseln zu: Navigation, Suche

Daten[Bearbeiten]

Inhalt[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]

Geblockte Vorlesung im Oktober und November (2*2 Einheiten pro Woche). Mitte Dezember eine schriftliche Prüfung (60 % der Note). 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]

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]

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]

Drei Übungsblätter, siehe "Ablauf". Die Aufgaben sind eine Mischung aus Beweisen (alle recht einfach), Anwendung der vorgestellten Algorithmen, und Verständnisfragen (z. B. "Beschreibe die Klasse der Interpretationen, in denen x = a -> x = b gültig ist").

Prüfung, Benotung[Bearbeiten]

Eine Prüfung 60 % der Note, drei Übungsblätter insgesamt 40 % der Note (siehe "Ablauf"). Im WS16 durfte man bei der Prüfung ein handbeschriebenes A4 Blatt als "Schummelzettel" benutzen.

Dauer der Zeugnisausstellung[Bearbeiten]

Wenige Tage nach der Prüfung.

Zeitaufwand[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]

Folien und Übungsblätter sind auf der Website verfügbar: http://www.cse.chalmers.se/~laurako/links/ADuct.html

Tipps[Bearbeiten]

Bei der Übung die in der Vorlesung vorgestellten Algorithmen genau beachten und nicht irgendwelche Schritte überspringen weil sie "eh klar" sind.

Verbesserungsvorschläge / Kritik[Bearbeiten]

noch offen