TU Wien:Logic and Reasoning in Computer Science VU (Kovacs)
Daten[Bearbeiten | Quelltext bearbeiten]
| Vortragende | Agata Ciabattoni• Robin Coutelier• Josephine Femke Dik• Clemens Eisenhofer• Marton Hajdu• Laura Kovacs• Sanja Lukumbuzya• Emeric Alexander Neufeld• Maria Magdalena Ortiz de la Fuente• Anouk Michelle Oudshoorn• Johannes Schoisswohl |
|---|---|
| ECTS | 6,0 |
| Letzte Abhaltung | 2024S |
| Sprache | English |
| Mattermost | logic-and-reasoning-in-computer-science • Register • Mattermost-Infos |
| Links | tiss:192033, eLearning |
Inhalt[Bearbeiten | Quelltext bearbeiten]
Propositional Logic (SAT), First-Order Logic, SMT
Ablauf[Bearbeiten | Quelltext bearbeiten]
Vortrag von verschiedenen Vortragenden, der aufgezeichnet und gestreamt wird (SS24)
Zu jedem Themenblock eine Übung (d.h. insgesamt 3), für die man sich zu einer von 3 Übungssessions anmelden muss. Gesamter Übungsmodus sehr entspannt, es müssen zwar Leute präsentieren, aber die Präsentation hat keinen Einfluss auf die Note. Von jedem Übungsblock muss man nur die Hälfte der Beispiele verpflichtend machen und hochladen, der Rest bringt Bonuspunkte für die Prüfung.
Es gibt Quizzes auf TUWEL, die aber nicht schwer sind, wenn man die Vorlesung verfolgt hat. Auch diese haben keinen Einfluss auf die Note, abgesehen davon, dass eine gewisse Punktezahl für den Antritt zur Prüfung notwendig ist.
Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]
wird eigentlich alles von Grund auf erklärt, also eigentlich keine abgesehen von GDS
dieses Fach harmoniert dennoch sehr gut mit Programm- und Systemverifikation, wer das schon gemacht hat tut sich hier leichter - ist aber keinesfalls notwendig
Vortrag[Bearbeiten | Quelltext bearbeiten]
sehr interaktiv, Besuch empfiehlt sich durchaus
einziges Problem ist, dass die Vortragenden eine recht laute Stimme haben, was mit angeschaltetem Mikro die Akustik im INF-HS nicht verbessert
Übungen[Bearbeiten | Quelltext bearbeiten]
Es gibt 3 jeweils 2 stündige Übungseinheiten, die entspannt ablaufen. Zu jedem bsp wird jemand rausgerufen. Diese Person soll das bsp erklären. Die Präsentation wird nicht bewertet und es werden keine Punkte abgezogen.
Jedes der 3 Aufgabenblätter (zu jedem Themengebiet SAT, FOL, SMT eines) enthält 6 bsp. 4 davon sind exercise problems (EP) und 2 project problems (PP). Bei jedem Aufgabenblatt müssen 2 EP und 1 PP gelößt werden.
EP: klassische Übungsbeispiele
PP: meistens kleines Python Programm schreiben oder irgendeine Aufgabe mit einem Problem lösen (einbisschen schwerer als EP)
Die 3 benötigten bsp lassen sich an einem Tag lösen, wen man die VO geschaut hast.
Es ist zu empfehlen alle bsp zu machen, weil Prüfungsbeispiele teilweise sehr ähnlich zu Übungsbeispielen sind und jedes extra Bsp ein zusätzlicher Punkt bei der Prüfung ist.
Prüfung, Benotung[Bearbeiten | Quelltext bearbeiten]
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
ca. 3 Wochen
Wenn man beim 1. Test negativ ist, erst beim 2. Test.
Prüfung besteht größtenteils aus abgeänderten Übungsaufgeben. CNF transformation + DPLL, tableau calculus und Nelson-Oppen decision procedure kommt fast immer.
Prüfung ist open book without electronic divices. Man hat 3h zeit. Die Zeit ist sehr großzügig bemessen.
Zeitaufwand[Bearbeiten | Quelltext bearbeiten]
für 6 ECTS gering, kein aufwendiges Fach
Unterlagen[Bearbeiten | Quelltext bearbeiten]
noch offen
Tipps[Bearbeiten | Quelltext bearbeiten]
noch offen
Highlights / Lob[Bearbeiten | Quelltext bearbeiten]
insgesamt sehr spannende und empfehlenswerte LVA, man sollte sich nicht vom Namen abschrecken lassen (bei weitem nicht so "theorethisch" wie der Namen vermuten lassen würde)
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
noch offen