TU Wien:Logic and Reasoning in Computer Science VU (Kovacs)
Daten[Bearbeiten | Quelltext bearbeiten]
Vortragende | Agata Ciabattoni• Robin Coutelier• Huimin Dong• Clemens Eisenhofer• Marton Hajdu• Laura Kovacs• Maria Magdalena Ortiz de la Fuente• Henri Thölke |
---|---|
ECTS | 6,0 |
Letzte Abhaltung | 2025S |
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.
SS25
2 Vorlesungen pro Woche mit Aufzeichnungen (die nur manchmal nicht ganz geklappt haben, dann wurden alte Aufzeichnungen zur Verfügung gestellt).
Zusätzlich ca. alle 3 Wochen ein TUWEL Quiz und außerdem 3 Exercise-Blätter, bei denen die Theorie-Aufgaben freiwillig waren, ein Project verpflichtend und das zweite Project für Extra-Punkte freiwillig gemacht werden konnten.
Am Ende eine Open-Book Klausur mit Wiederholungsmöglichkeit am Ende der Ferien.
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.
Wer das Fach zusammen mit Einführung in Artificial Intelligence macht, spart sich dort einen von 5 Themen-Blöcken, da man Logic dann schon genug drauf hat.
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
SS25:
Vorlesungen wurden nicht gestreamed aber dafür aufgezeichnet. Die LVA ist auch ohne den Vortrag und nur mit den Folien machbar.
Der Vortrag ist an sich sehr lieb gemacht, die Vortragenden sind alle sehr motiviert und wechseln sich mit den Themen ab. Manchmal wird ein bisschen lange um den heißen Brei geredet und auch einfache Beispiele werden 5 mal ausgeführt oder es wird viel hin- und her geredet, anstatt auf den Punkt zu kommen. Dementsprechend war der Vortrag manchmal etwas wirr oder langweilig bzw. man hätte die Themen auch schneller und klarer erklären können. Die Vortragenden sind keine alteingesessenen TU-Professoren, weswegen es manchmal auch noch Unklarheiten mit der Technik gab. Alles in allem aber kein schlechter Vortrag und sehr lieb gemacht.
Übungen[Bearbeiten | Quelltext bearbeiten]
SS25:
Eine UE bestehen noch immer aus Problemen und Projekten. Es musste nur aus jeder UE ein Projekt gelöst werden, der Rest war freiwillig. Es gab immer 2 Übungseinheiten in Präsenz und eine über Zoom, Anwesenheitspflicht oder Tafelleistung gab's bei den Einheiten aber nicht.
Quiz
Über das Semester verteilt gab es 5 TUWEL-Quizzes (also ca. alle 3 Wochen). Pro Quiz gab es 10 Fragen und 25 Minuten Zeit, wobei man 10 Punkte (auch halbe) erreichen konnte. Die Fragen waren aufgrund der kurzen Zeit zwar nicht schwer, man musste also keine langen Rechnungen machen, aber man musste trotzdem meistens etwas Nachdenken. Pro Quiz hat man 2 Versuche, der bessere zählt. Da die Fragen immer den gleichen Aufbau haben, aber die Werte automatisch generiert werden, konnte man die Antworten nicht 1:1 kopieren. ChatGPT ist bei den Fragen nur mittel hilfreich. Wenn man sich aber vorab ein paar Tests von anderen Personen anschaut und die Aufgabentypen durchrechnet und versteht, schafft man es gut immer 9-10 Punkte zu bekommen.
Exercise Blätter
Über das Semester gab es 3 Exercise Blätter mit je ca. 10 Theorie Aufgaben. Diese waren allerdings freiwillig. Wer wollte, konnte zu den Übungseinheiten gehen, wo die Blätter besprochen werden. Die Blätter eignen sich super zur Prüfungsvorbereitung, da die Aufgaben sehr ähnlich sind.
Projects
Auf den Exercise Blättern waren zusätzlich 2 Projects. Diese sind praktische Aufgaben, d.h. Programmieren. Das erste Project musste man verpflichtend abgeben und alle 3 Pflichtabgaben zählen 10% der Note. Die Pflicht Projects waren aber immer sehr einfach, meistens nur ca. 10 Zeilen Code. Dafür wurden in der Vorlesung entsprechende SAT Solver etc. vorgestellt und man konnte die Aufgaben damit sehr leicht lösen. Das zweite Project war je umfangreicher und es ging meistens darum in Python irgendwas zu schreiben / zu vervollständigen. Hier konnte man schon etwas mehr Zeit reinstecken, je nach Vorwissen 3-7 Stunden pro Blatt. Die zweiten Projects zählen zusammen nochmal 10% der Note, wobei diese 10% Bonuspunkte sind, d.h. es mit Klausur, Quizzes und Projects zusammen 110% zu erreichen gab.
SS24:
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 (ein bisschen schwerer als EP)
Die 3 benötigten Beispiele lassen sich an einem Tag lösen, wen man die VO geschaut hast.
Es ist zu empfehlen alle Beispiele zu machen, weil Prüfungsbeispiele teilweise sehr ähnlich zu Übungsbeispielen sind und jedes extra Bsp ein zusätzlicher Punkt bei der Prüfung ist.
Klausur[Bearbeiten | Quelltext bearbeiten]
SS25:
Die Klausur ist Open Book, man durfte jegliche nicht-digitale Aufzeichnung mitbringen, also wenn man will auch 500 Seiten Vorlesungsfolien oder alle Exercise Beispiele und Altklausuren durchgerechnet. Man hat 3* Stunden Zeit, was recht viel ist, aber da einige Aufgaben auch recht schreibaufwändig sind, braucht man die auch. Stress hat man trotzdem keinen. Grundsätzlich war die Klausur recht fair, wobei es in unserem Semester ein Beispiel (Stably infinite Theories) gab, was doch recht überraschend kam, da es in der Vorlesung eher nur nebenbei kurz erwähnt wurde. Dementsprechend konnten diese eine Aufgabe (10/80 Punkten) nur wenige lösen. An dieser Stelle hat sich ausgezahlt, die Bonusprojects gemacht zu haben, wenn man eine sehr gute Note wollte. Die restlichen Aufgaben waren aber sehr vorhersehbar und glichen den Altklausuren und Übungsaufgaben. Man konnte auch ohne das stably infinte Beispiel eine gute Note erreichen.
An dieser Stelle sei angemerkt, dass die 3 Altklausuren des Vorjahrs alle exakt die gleichen Aufgabentypen hatten, die Klausur von diesem Jahr aber ein bisschen anders war. Die SMT Aufgabe am Schluss und die ersten beiden Aufgaben waren gleich. Es ist also anzunehmen, dass alle 3 Klausuren PRO SEMESTER gleich aufgebaut sind, sich die Klausuren zwischen den Semestern aber schon ein bisschen unterscheiden. Trotzdem wie gesagt inhaltlich ähnlich und wer die Übungsaufgaben und Altklausuren lösen kann, schafft auch das. Von der LVA selbst wurden die 3 Altklausuren des letzten Jahres (ohne Lösungen) bereit gestellt.
*Es wurde von der LVA zwar 3 Stunden angesagt und es steht hier auch mehrfach 3, aber bei uns im Hörsaal waren es nur 2,5 Stunden. Es gab bei uns aber auch ein bisschen Trubel weil die Hörsaal-Größe falsch berechnet wurde und zu viele Leute da waren und außerdem die Aufsichten zu spät kamen und selbst nicht wussten, wie viel Zeit wir jetzt haben. Also vielleicht war das auch ein Fehler :)
Weitere Meinungen:
Es wurden 3 Altprüfungen aus 2024 zur Verfügung gestellt. Unsere Prüfung hatte allerdings 6 Beispiele, wobei man mit dem Wissen aus dem Altprüfungen noch positiv sein konnte. Inhalt: PureAtom/CNF/DPLL, Herleitung Polarity, Aussagenlogik, Nelson-Oppen Decision Procedure, Entailment un dnoch eins.
--- Prüfung besteht größtenteils aus abgeänderten Übungsaufgaben. 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.
Andere Meinung: 3h hört sich nach durchaus viel an, mMn braucht man die Zeit aber auch. Es waren 6 Beispiele, wovon die ganzen Entailments, Nelson-Oppen einfach sehr viel Schreibaufwand sind.
Benotung[Bearbeiten | Quelltext bearbeiten]
SS25
Die Benotung setzt sich wie folgt zusammen:
10% Quizzes
10% Verpflichtende Projects
80% Klausur
+ 10% Bonuspunkte für Extra-Projects
Notenschlüssel:
- grade 5: < 60 points
- grade 4: 60-69 points
- grade 3: 70-79 points
- grade 2: 80-89 points
- grade 1: 90-100+ points
Die Benotung ist fair. Da man mit den Quizzes und Projecten schon einige Punkte gut machen konnte, hat man in der Klausur auch nicht zu viel Druck.
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
ca. 3 Wochen
Wenn man beim 1. Test negativ ist, erst beim 2. Test.
SS25: es gibt die Möglichkeit schon frühzeitig ein Zeugnis ausgestellt zu bekommen, wenn man sich dafür über tuwel anmeldet, Testkorrektur hat ca. 2 Wochen benötigt.
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)
SS25:
Andere Meinung: Habe die Abhaltung der LVA im SS25 als doch eher trocken und nicht besonders spannend wahrgenommen.
Zusätzliche Meinung: Der Vortrag von Prof. Kovacs ist besser als die der anderen beiden Damen. Trotzdem ist und bleibt der Stoff eigentlich nur Theorie.
Weitere Meinung: Ich fand die Vorträge von Prof. Ortiz auch sehr gut, sie hat sichtlich Spaß an der Materie. Die Vorträge von Prof. Ciabattoni fand ich teils trocken, sie gleicht es allerdings mit eigens erstellten Handouts aus , welche um einiges besser verständlich sind als die Folien.
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
SS25:
Die Übungsbewertungen wirken manchmal ein wenig aus der Nase gezogen, bspw. gab es bei einer Abgabe vom Bonusbeispiel vom 1. Übungsblatt 1/4 der Punkte wenn die Abgabe innerhalb von 10% so schnell war wie die des Tutors.
Ich finde man könnte evtl. auch in den Vorlesungen versuchen den Vortrag ein wenig interaktiver zu gestalten. Die Handouts mit mehr Informationen als die Folien haben mir eigentlich sehr geholfen.
Materialien
Neues Material hinzufügen2
- 2024-06-26 Prüfung mit Lösung.pdf (details)
- 2024-06-26 Prüfung ohne Lösungpdf.pdf (details)
- 2025SS-Quiz-5-6.pdf (details)
- 2025SS-Quiz1-1.pdf (details)
- 2025SS-Quiz1-2.pdf (details)
- 2025SS-Quiz1-3.pdf (details)
- 2025SS-Quiz1-4.pdf (details)
- 2025SS-Quiz2-1.pdf (details)
- 2025SS-Quiz2-2.pdf (details)
- 2025SS-Quiz2-3.pdf (details)
- 2025SS-Quiz3-1.pdf (details)
- 2025SS-Quiz3-2.pdf (details)
- 2025SS-Quiz3-3.pdf (details)
- 2025SS-Quiz3-4.pdf (details)
- 2025SS-Quiz3-5.pdf (details)
- 2025SS-Quiz3-6.pdf (details)
- 2025SS-Quiz4-1.pdf (details)
- 2025SS-Quiz4-2.pdf (details)
- 2025SS-Quiz4-3.pdf (details)
- 2025SS-Quiz4-4.pdf (details)
- 2025SS-Quiz4-5.pdf (details)
- 2025SS-Quiz4-6.pdf (details)
- 2025SS-Quiz5-1.pdf (details)
- 2025SS-Quiz5-2.pdf (details)
- 2025SS-Quiz5-3.pdf (details)
- 2025SS-Quiz5-4.pdf (details)
- 2025SS-Quiz5-5.pdf (details)
- 2025SS-Quiz5-6.pdf (details)
- 2025SS-Quiz5-7.pdf (details)
- 2025SS-Quiz5-8.pdf (details)