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

From VoWi
Revision as of 15:22, 15 December 2019 by Ovasco (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search

Daten[edit]

Lecturers Prof. Laura Kovács
ECTS 6
Department Forschungsbereich Formal Methods in Systems Engineering
When winter semester
Language English
Links tiss:184774, Homepage, Mattermost-Channel
Zuordnungen
Master Logic and Computation Wahlmodul Logic, Mathematics, and Theoretical Computer Science
Master Software Engineering & Internet Computing Wahlmodul Formale Methoden und Theoretische Informatik
Master Technische Informatik Wahlmodul Computer-Aided Verification

Mattermost: Channel "automated-deduction"RegisterMattermost-Infos

Inhalt[edit]

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

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

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

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

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

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

Wenige Tage nach der Prüfung.

Zeitaufwand[edit]

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

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

Tipps[edit]

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

noch offen