https://iccl.inf.tu-dresden.de/w/api.php?action=feedcontributions&feedformat=atom&user=Markus+Kr%C3%B6tzsch 2026-06-03T21:35:05Z Benutzerbeiträge MediaWiki 1.43.1 https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44441 2026-06-01T09:10:45Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-06-overlay.pdf, TheoLog2026-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-07-overlay.pdf, TheoLog2026-Vorlesung-07-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2026-05-03<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-03.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 4<br /> |Room=--<br /> |Date=2026-05-10<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-04.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=8. NP<br /> |Room=HÜL/S386<br /> |Date=2026-05-11<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-08-overlay.pdf, TheoLog2026-Vorlesung-08-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=9. NP-Vollständigkeit<br /> |Room=HÜL/S386<br /> |Date=2026-05-18<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-09-overlay.pdf, TheoLog2026-Vorlesung-09-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=10. NP-Vollständigkeit (2)<br /> |Room=HSZ/0002<br /> |Date=2026-05-21<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-10-overlay.pdf, TheoLog2026-Vorlesung-10-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=11. NL und PSpace<br /> |Room=HÜL/S386<br /> |Date=2026-06-01<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-11-overlay.pdf, TheoLog2026-Vorlesung-11-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=5. Übungsblatt<br /> |Room=--<br /> |Date=2026-05-17<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-05.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=12. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-04<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=13. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=14. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-11<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=15. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-15<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=16. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-18<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=17. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=18. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-29<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=19. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-02<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=20. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-07-06<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=21. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-09<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=22. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-07-13<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=23. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-16<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=24. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-20<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Konsultation<br /> |Title=Probeklausur<br /> |Room=HSZ/0002<br /> |Date=2026-07-23<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 6<br /> |Room=--<br /> |Date=2026-05-28<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-06.pdf<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-11-print.pdf&diff=44440 2026-06-01T09:10:38Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-11-overlay.pdf&diff=44439 2026-06-01T09:10:31Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:FS2025-Vorlesung-04-print.pdf&diff=44435 2026-05-22T08:51:24Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:FS2025-Vorlesung-04-print.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:FS2025-Vorlesung-09-print.pdf&diff=44434 2026-05-22T08:51:14Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:FS2025-Vorlesung-09-print.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44429 2026-05-21T06:42:15Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-06-overlay.pdf, TheoLog2026-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-07-overlay.pdf, TheoLog2026-Vorlesung-07-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2026-05-03<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-03.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 4<br /> |Room=--<br /> |Date=2026-05-10<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-04.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=8. NP<br /> |Room=HÜL/S386<br /> |Date=2026-05-11<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-08-overlay.pdf, TheoLog2026-Vorlesung-08-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=9. NP-Vollständigkeit<br /> |Room=HÜL/S386<br /> |Date=2026-05-18<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-09-overlay.pdf, TheoLog2026-Vorlesung-09-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=10. NP-Vollständigkeit (2)<br /> |Room=HSZ/0002<br /> |Date=2026-05-21<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-10-overlay.pdf, TheoLog2026-Vorlesung-10-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=11. NL und PSpace<br /> |Room=HÜL/S386<br /> |Date=2026-06-01<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=5. Übungsblatt<br /> |Room=--<br /> |Date=2026-05-17<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-05.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=12. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-04<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=13. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=14. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-11<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=15. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-15<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=16. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-18<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=17. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=18. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-29<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=19. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-02<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=20. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-07-06<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=21. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-09<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=22. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-07-13<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=23. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-16<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=24. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-20<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Konsultation<br /> |Title=Probeklausur<br /> |Room=HSZ/0002<br /> |Date=2026-07-23<br /> |DS=DS4<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-10-print.pdf&diff=44428 2026-05-21T06:42:08Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-10-overlay.pdf&diff=44427 2026-05-21T06:41:59Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-09-print.pdf&diff=44426 2026-05-21T06:40:29Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-09-print.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-09-overlay.pdf&diff=44425 2026-05-21T06:40:16Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-09-overlay.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44416 2026-05-18T08:23:38Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-06-overlay.pdf, TheoLog2026-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-07-overlay.pdf, TheoLog2026-Vorlesung-07-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2026-05-03<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-03.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 4<br /> |Room=--<br /> |Date=2026-05-10<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-04.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=8. NP<br /> |Room=HÜL/S386<br /> |Date=2026-05-11<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-08-overlay.pdf, TheoLog2026-Vorlesung-08-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=9. NP-Vollständigkeit<br /> |Room=HÜL/S386<br /> |Date=2026-05-18<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-09-overlay.pdf, TheoLog2026-Vorlesung-09-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=10. Pseudopolynomialität und NL<br /> |Room=HSZ/0002<br /> |Date=2026-05-21<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=11. PSpace<br /> |Room=HÜL/S386<br /> |Date=2026-06-01<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=5. Übungsblatt<br /> |Room=--<br /> |Date=2026-05-17<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-05.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=12. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-04<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=13. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=14. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-11<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=15. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-15<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=16. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-06-18<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=17. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=18. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-29<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=19. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-02<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=20. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-07-06<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=21. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-09<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=22. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-07-13<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=23. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-16<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=24. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-07-20<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Konsultation<br /> |Title=Probeklausur<br /> |Room=HSZ/0002<br /> |Date=2026-07-23<br /> |DS=DS4<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-09-print.pdf&diff=44415 2026-05-18T08:21:17Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-09-overlay.pdf&diff=44414 2026-05-18T08:21:07Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44402 2026-05-11T14:24:23Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-06-overlay.pdf, TheoLog2026-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-07-overlay.pdf, TheoLog2026-Vorlesung-07-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2026-05-03<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-03.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 4<br /> |Room=--<br /> |Date=2026-05-10<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-04.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=8. NP<br /> |Room=HÜL/S386<br /> |Date=2026-05-11<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-08-overlay.pdf, TheoLog2026-Vorlesung-08-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=9. NP-Vollständigkeit<br /> |Room=HÜL/S386<br /> |Date=2026-05-18<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=10. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-05-21<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=11. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-01<br /> |DS=DS3<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-08-print.pdf&diff=44401 2026-05-11T14:24:02Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-08-overlay.pdf&diff=44400 2026-05-11T14:23:53Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Inproceedings3461&diff=44399 2026-05-11T12:20:52Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Alex<br /> |ErsterAutorNachname=Ivliev<br /> |FurtherAuthors=Markus Krötzsch; Maximilian Marx<br /> }}<br /> {{Inproceedings<br /> |Referiert=1<br /> |Title=SPARQLing Datalog for Rule-Based Reasoning over Large Knowledge Graphs<br /> |To appear=0<br /> |Year=2026<br /> |Booktitle=Proceedings of the 23rd European Semantic Web Conference (ESWC 2026), Part I<br /> |Pages=518-536<br /> |Publisher=Springer<br /> |Editor=Maribel Acosta, Marieke van Erp, Sebastian Rudolph, Olaf Hartig, Blerina Spahiu, Anisa Rula, Daniel Garijo, Francesco Osborne<br /> |Series=LNCS<br /> |Volume=16549<br /> }}<br /> {{Publikation Tool<br /> |Tool=Nemo<br /> }}<br /> {{Publikation Details<br /> |Abstract=We propose a new integration of rule reasoners with one or more RDF stores, using selective SPARQL queries to fetch relevant data. In contrast to previous implementations that merely import results of fixed SPARQL queries, our approach relies on pure logic programs over RDF triple data. Transparent to the user, optimised SPARQL queries then are constructed and evaluated during reasoning. To ensure good performance, we develop optimisation methods that adopt ideas from logic program optimisation, including semi-naive evaluation, magic sets, and static filtering. Based on the integration of our methods into the open source rule engine Nemo, we empirically evaluate our approach with complex rule sets over large knowledge graphs.<br /> |Download=Ivliev-Kroetzsch-Marx Optimising-SPARQL-for-Datalog eswc2026.pdf<br /> |DOI Name=10.1007/978-3-032-25156-5_27<br /> |Projekt=CPEC, SECAI, ScaDS.AI<br /> |Forschungsgruppe=Wissensbasierte Systeme<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Regelbasiertes Schließen<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Semantische Technologien<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Wissensrepräsentation und logisches Schließen<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44386 2026-05-07T09:23:08Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-06-overlay.pdf, TheoLog2026-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-07-overlay.pdf, TheoLog2026-Vorlesung-07-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2026-05-03<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-03.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 4<br /> |Room=--<br /> |Date=2026-05-10<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-04.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=8. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-05-11<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=9. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-05-18<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=10. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-05-21<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=11. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-06-01<br /> |DS=DS3<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-07-print.pdf&diff=44385 2026-05-07T09:20:42Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-07-overlay.pdf&diff=44384 2026-05-07T09:20:29Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44378 2026-05-04T09:10:47Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-06-overlay.pdf, TheoLog2026-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2026-05-03<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-03.pdf<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-06-print.pdf&diff=44377 2026-05-04T09:10:42Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-06-overlay.pdf&diff=44376 2026-05-04T09:10:32Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-05-print.pdf&diff=44371 2026-04-30T16:33:19Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-05-print.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-05-overlay.pdf&diff=44370 2026-04-30T16:33:09Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-05-overlay.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44365 2026-04-29T09:51:16Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. DPLL und SMT<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-05-overlay.pdf, TheoLog2026-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Einführung in die Komplexitätstheorie<br /> |Room=HÜL/S386<br /> |Date=2026-05-04<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=7. Beziehungen zwischen Komplexitätsklassen / Effizient lösbare Probleme<br /> |Room=HSZ/0002<br /> |Date=2026-05-07<br /> |DS=DS4<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-05-print.pdf&diff=44364 2026-04-29T09:49:20Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-05-overlay.pdf&diff=44363 2026-04-29T09:49:09Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-04-print.pdf&diff=44337 2026-04-23T13:06:57Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-04-print.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-04-overlay.pdf&diff=44336 2026-04-23T13:06:47Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-04-overlay.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44335 2026-04-23T13:06:27Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Termin entfällt<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS1<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44333 2026-04-23T11:02:37Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Resolution und Horn-Logik<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-04-overlay.pdf, TheoLog2026-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS1<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-04-print.pdf&diff=44332 2026-04-23T11:02:29Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-04-overlay.pdf&diff=44331 2026-04-23T11:02:19Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44330 2026-04-22T11:36:05Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=HSZ/0002<br /> |Date=2026-05-14<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=HÜL/S386<br /> |Date=2026-05-25<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=HSZ/0002<br /> |Date=2026-05-28<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=HSZ/0002<br /> |Date=2026-06-25<br /> |DS=DS1<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44329 2026-04-22T11:32:57Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2026-04-26<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Himmelfahrt (gesetzlicher Feiertag)<br /> |Room=--<br /> |Date=2026-05-14<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstmontag (gesetzlicher Feiertag)<br /> |Room=--<br /> |Date=2026-05-25<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=OUTPUT.DD (keine Lehre am Nachmittag)<br /> |Room=--<br /> |Date=2026-06-25<br /> |DS=DS1<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Pfingstwoche (keine Lehre)<br /> |Room=--<br /> |Date=2026-05-28<br /> |DS=DS1<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Formale_Systeme_(WS2025)&diff=44328 2026-04-22T11:25:49Z

<p>Markus Krötzsch: +link zu WHILE/LOOP</p> <hr /> <div>{{Vorlesung<br /> |Title=Formale Systeme<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Stefan Borgwardt; Anton Claußnitzer; Florens Förster; Lukas Gerlach; Anna Hornschild; Cornelius Lübke; Maximilian Marx<br /> |Term=WS<br /> |Year=2025<br /> |Lecture series=Formale Systeme<br /> |Matrix=#fosys:tu-dresden.de<br /> |Module=INF-25-BA-AUB, INF-B-270, INF-B-275, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=Die Lehrveranstaltung ''Formale Systeme'' vermittelt eine Einleitung in die Gebiete der formalen Sprachen, Automatentheorie und Berechenbarkeit. Dies beinhaltet einige der wichtigsten Grundlagen der Informatik, wie z.B. reguläre Ausdrücke, formale Grammatiken sowie grundlegende Begriffe der Berechenbarkeits- und Komplexitätstheorie. Damit bildet die Vorlesung die Grundlage für viele vertiefende Vorlesungen.<br /> <br /> == Prüfung ==<br /> <br /> === Klausureinsicht ===<br /> <br /> Sie können sich ab sofort einen Termin in [https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/51472400384/CourseNode/1775702163415913006 Opal] für die Einsichtnahme Ihrer Klausur buchen. Bitte beachten Sie die Hinweise auf der Einschreibungsseite.<br /> <br /> === Lernraum ===<br /> <br /> Wir bieten Ihnen zwei Lernräume in der vorlesungsfreien Zeit an. Zu diesen Terminen können Sie uns weitere Fragen stellen, die Ihnen während des Lernens aufgefallen sind. Bitte nutzen Sie auch den entsprechenden Matrixkanal zur Lehrveranstaltung. Ihre Kommilitonen wissen häufig auch die richtigen Antworten.<br /> <br /> * Dienstag, 10. Februar 2026 DS4 (13:00-15:00 Uhr) in [[APB E023]]<br /> * Montag, 23. Februar 2026 DS4 (13:00-15:00 Uhr) in [[APB E023]]<br /> <br /> === Zeit ===<br /> <br /> Die Klausur über 90 Minuten findet '''am Montag, den 02.03.2026''' ab '''8:00 Uhr''' statt. Wir beginnen mit dem Einlass um '''7:40 Uhr''' im entsprechenden Raum (siehe unten). Bitte seien Sie pünktlich, damit wir in allen Räumen um 8:00 Uhr mit der Klausur beginnen können.<br /> <br /> === Ort ===<br /> <br /> Für die Prüfung stehen und die Räume [[HSZ/AUDI]], [[HSZ/0003]] sowie [[HSZ/0004]] zur Verfügung. Die Einteilung in die Räume erfolgt per Anfangsbuchstaben des Nachnamens:<br /> * '''A-J''' in [[HSZ/0003]]<br /> * '''K-M''' in [[HSZ/0004]]<br /> * '''N-Z''' in [[HSZ/AUDI]]<br /> <br /> === Hilfsmittel ===<br /> <br /> Es sind '''keine Hilfsmittel''' erlaubt, insbesondere keine technischen und elektronischen Hilfsmittel oder Formelsammlungen und Nachschlagewerke.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[BAR/SCHÖ]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0003]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. Oktober 2025 statt.<br /> <br /> == Übungen ==<br /> <br /> Der Übungsbetrieb startet '''am 20. Oktober 2025''' zu Ihren jeweiligen Terminen in den angegebenen Räumen statt. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden. Eine vorherige Einschreibung in die angebotenen Übungstermine ist verpflichtend bevor Sie an der Übungsgruppe teilnehmen. Welche Übungstermine wir anbieten, geben wir rechtzeitig bekannt. Die Einschreibung wird am '''Montag, den 13.10.2025 um 15:00 Uhr''' freigeschalten:<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://tud.link/sdutby die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/FormaleSysteme<br /> <br /> Alle Foliensätze der Vorlesungen können entsprechend den Lizensbedingungen von [https://creativecommons.org/licenses/by/3.0/de/ Creative Commons CC By 3.0 Deutschland] genutzt, weitergegeben und modifiziert werden. Als Namensnennung ist folgende Angabe einzufügen:<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/FS2025, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Besonderen Dank gilt allen [https://github.com/knowsys/FormaleSysteme/graphs/contributors Contributors], die Anmerkungen und Verbesserungen beigetragen haben: [[Daniel Borchmann]], [[Maximilian Marx]], [https://github.com/chlewe Christian Lewe], [https://github.com/tidenhub David Tiede], [https://github.com/jhaye Johannes (jhaye)], [https://github.com/DerKolibri Andrej Bereza], [https://github.com/CniKKoR CniKKoR], [https://github.com/marcusrossel Marcus Rossel], [https://github.com/MaxHaertwig Max Haertwig], [https://github.com/eknoes Sönke (eknoes)], [https://github.com/bennofs Benno Fünfstück], [https://github.com/voidless Julius Schmitt]. (Stand März 2021; Ergänzungen sind willkommen.)<br /> <br /> == WHILE/LOOP Simulator ==<br /> <br /> Wir bieten einen [https://tools.iccl.inf.tu-dresden.de/while/ Online-Simulator für WHILE- und LOOP-Programme] an. Der Simulator unterstützt zusätzlich zu den Grundsprachen einige der Abkürzungen aus der Vorlesung. Im Menü unter ''Beispiele'' finden sich einige Beispielprogramme, die in das Programmfeld kopiert werden können.<br /> <br /> Der Simulator wurde von Simon Meusel entwickelt. Der Quellcode ist frei verfügbar unter https://github.com/knowsys/while-simulator . Pull-Requests sind Willkommen.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#fosys:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/FormaleSysteme<br /> Alternativ können Hinweise zu Tippfehlern in den Vorlesungsfolien auch an die Mailingliste geschickt werden.<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> == Formale Sprachen, Komplexität und Entscheidbarkeit ==<br /> <br /> === Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zu Sprachen und Berechnungskomplexität; leider nur auf Englisch)''<br /> <br /> === Online verfügbare Skripte ===<br /> <br /> * [[Franz Baader]]: '''[https://lat.inf.tu-dresden.de/teaching/ws2013-2014/FS/script_2016-02.pdf Skript Formale Systeme, Teil 1 &amp;ndash; Automaten und formale Sprachen].''' TU Dresden.<br /> <br /> Die Vorlesungen haben kleine Abweichungen von diesem Text, stimmen aber in vielen wichtigen Punkten überein.<br /> <br /> Andere Scripte scheinen zurzeit nicht (mehr) online verfügbar zu sein. Hinweise zu weiteren Links auf sinnvolle Materialien sind willkommen.<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Einleitung formale Sprachen<br /> |Room=BAR/SCHÖ<br /> |Date=2025-10-13<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-01-overlay.pdf, FS2025-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Grammatiken und die Chomsky-Hierarchie<br /> |Room=HSZ/0003<br /> |Date=2025-10-16<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-02-overlay.pdf, FS2025-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Endliche Automaten<br /> |Room=BAR/SCHÖ<br /> |Date=2025-10-20<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-03-overlay.pdf, FS2025-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Nichtdeterministische Automaten<br /> |Room=HSZ/0003<br /> |Date=2025-10-23<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-04-overlay.pdf, FS2025-Vorlesung-04-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Abschlusseigenschaften regulärer Sprachen<br /> |Room=BAR/SCHÖ<br /> |Date=2025-10-27<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-05-overlay.pdf, FS2025-Vorlesung-05-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Reguläre Ausdrücke (1)<br /> |Room=HSZ/0003<br /> |Date=2025-10-30<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-06-overlay.pdf, FS2025-Vorlesung-06-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Reguläre Ausdrücke (2)<br /> |Room=BAR/SCHÖ<br /> |Date=2025-11-03<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-07-overlay.pdf, FS2025-Vorlesung-07-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Entfällt<br /> |Title=Interne Veranstaltung<br /> |Room=HSZ/0003<br /> |Date=2025-11-06<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Minimale Automaten (1)<br /> |Room=BAR/SCHÖ<br /> |Date=2025-11-10<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-08-overlay.pdf, FS2025-Vorlesung-08-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Minimale Automaten (2)<br /> |Room=HSZ/0003<br /> |Date=2025-11-13<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-09-overlay.pdf, FS2025-Vorlesung-09-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Grenzen regulärer Sprachen / Probleme für Automaten<br /> |Room=BAR/SCHÖ<br /> |Date=2025-11-17<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-10-overlay.pdf, FS2025-Vorlesung-10-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Von regulären zu kontextfreien Sprachen<br /> |Room=HSZ/0003<br /> |Date=2025-11-20<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-11-overlay.pdf, FS2025-Vorlesung-11-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Das Wortproblem für kontextfreie Sprachen<br /> |Room=BAR/SCHÖ<br /> |Date=2025-11-24<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-12-overlay.pdf, FS2025-Vorlesung-12-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Das Pumping Lemma kontextfreier Sprachen<br /> |Room=HSZ/0003<br /> |Date=2025-11-27<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-13-overlay.pdf, FS2025-Vorlesung-13-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Abschlusseigenschaften kontextfreier Sprachen<br /> |Room=BAR/SCHÖ<br /> |Date=2025-12-01<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-14-overlay.pdf, FS2025-Vorlesung-14-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Einleitung Kellerautomaten<br /> |Room=HSZ/0003<br /> |Date=2025-12-04<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-15-overlay.pdf, FS2025-Vorlesung-15-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Kellerautomaten und CFGs<br /> |Room=BAR/SCHÖ<br /> |Date=2025-12-08<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-16-overlay.pdf, FS2025-Vorlesung-16-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Deterministische Sprachen / Entscheidungsprobleme<br /> |Room=HSZ/0003<br /> |Date=2025-12-11<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-17-overlay.pdf, FS2025-Vorlesung-17-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Turingmaschinen<br /> |Room=BAR/SCHÖ<br /> |Date=2025-12-15<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-18-overlay.pdf, FS2025-Vorlesung-18-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Konsultation<br /> |Title=Repetitorium (1)<br /> |Room=HSZ/0003<br /> |Date=2025-12-18<br /> |DS=DS4<br /> |Download=FS2025-Repetitorium-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Nichtdeterminismus und Turingmächtigkeit<br /> |Room=BAR/SCHÖ<br /> |Date=2026-01-05<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-19-overlay.pdf, FS2025-Vorlesung-19-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Berechenbarkeit und Unentscheidbarkeit<br /> |Room=HSZ/0003<br /> |Date=2026-01-08<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-20-overlay.pdf, FS2025-Vorlesung-20-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=WHILE und LOOP<br /> |Room=BAR/SCHÖ<br /> |Date=2026-01-12<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-21-overlay.pdf, FS2025-Vorlesung-21-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Das Halteproblem und Reduktionen<br /> |Room=HSZ/0003<br /> |Date=2026-01-15<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-22-overlay.pdf, FS2025-Vorlesung-22-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Der Satz von Rice und das Postsche Korrespondenzproblem<br /> |Room=BAR/SCHÖ<br /> |Date=2026-01-19<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-23-overlay.pdf, FS2025-Vorlesung-23-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Typ 0 und Typ 1<br /> |Room=HSZ/0003<br /> |Date=2026-01-22<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-24-overlay.pdf, FS2025-Vorlesung-24-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Unentscheidbare Probleme formaler Sprachen<br /> |Room=BAR/SCHÖ<br /> |Date=2026-01-26<br /> |DS=DS3<br /> |Download=FS2025-Vorlesung-25-overlay.pdf, FS2025-Vorlesung-25-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Zusammenfassung und Ausblick<br /> |Room=HSZ/0003<br /> |Date=2026-01-29<br /> |DS=DS4<br /> |Download=FS2025-Vorlesung-26-overlay.pdf, FS2025-Vorlesung-26-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Konsultation<br /> |Title=Repetitorium (2)<br /> |Room=BAR/SCHÖ<br /> |Date=2026-02-02<br /> |DS=DS3<br /> |Download=FS2025-Repetitorium-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Konsultation<br /> |Title=Besprechung der Probeklausur<br /> |Room=HSZ/0003<br /> |Date=2026-02-05<br /> |DS=DS4<br /> |Download=FS2025-Probeklausur.pdf, FS2025-Probeklausur-Slides.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2025-10-19<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 2<br /> |Room=--<br /> |Date=2025-10-26<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-02.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 3<br /> |Room=--<br /> |Date=2025-11-02<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-03.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 4<br /> |Room=--<br /> |Date=2025-11-09<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-04.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 5<br /> |Room=--<br /> |Date=2025-11-16<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-05.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 6<br /> |Room=--<br /> |Date=2025-11-23<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-06.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 7<br /> |Room=--<br /> |Date=2025-11-30<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-07.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 8<br /> |Room=--<br /> |Date=2025-12-07<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-08.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 9<br /> |Room=--<br /> |Date=2025-12-14<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-09.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 10<br /> |Room=--<br /> |Date=2026-01-04<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-10.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 11<br /> |Room=--<br /> |Date=2026-01-11<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-11.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 12<br /> |Room=--<br /> |Date=2026-01-18<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-12.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 13<br /> |Room=--<br /> |Date=2026-01-25<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-13.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 14<br /> |Room=--<br /> |Date=2026-02-01<br /> |DS=terminlos<br /> |Download=FS2025-Blatt-14.pdf<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-03-print.pdf&diff=44317 2026-04-20T13:57:11Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-03-print.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-03-overlay.pdf&diff=44316 2026-04-20T13:56:42Z

<p>Markus Krötzsch: Markus Krötzsch lud eine neue Version von Datei:TheoLog2026-Vorlesung-03-overlay.pdf hoch</p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44311 2026-04-20T08:38:05Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> &lt;!--<br /> == WHILE/LOOP Simulator ==<br /> <br /> Wir bieten einen [https://tools.iccl.inf.tu-dresden.de/while/ Online-Simulator für WHILE- und LOOP-Programme] an. Der Simulator unterstützt zusätzlich zu den Grundsprachen einige der Abkürzungen aus der Vorlesung. Im Menü unter ''Beispiele'' finden sich einige Beispielprogramme, die in das Programmfeld kopiert werden können.<br /> <br /> Der Simulator wurde von Simon Meusel entwickelt. Der Quellcode ist frei verfügbar unter https://github.com/knowsys/while-simulator . Pull-Requests sind Willkommen.<br /> --&gt;<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44310 2026-04-20T08:37:32Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> &lt;!--<br /> == WHILE/LOOP Simulator ==<br /> <br /> Wir bieten einen [https://tools.iccl.inf.tu-dresden.de/while/ Online-Simulator für WHILE- und LOOP-Programme] an. Der Simulator unterstützt zusätzlich zu den Grundsprachen einige der Abkürzungen aus der Vorlesung. Im Menü unter ''Beispiele'' finden sich einige Beispielprogramme, die in das Programmfeld kopiert werden können.<br /> <br /> Der Simulator wurde von Simon Meusel entwickelt. Der Quellcode ist frei verfügbar unter https://github.com/knowsys/while-simulator . Pull-Requests sind Willkommen.<br /> --&gt;<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum Logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=4. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-23<br /> |DS=DS4<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=5. Vorlesung<br /> |Room=HÜL/S386<br /> |Date=2026-04-27<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=6. Vorlesung<br /> |Room=HSZ/0002<br /> |Date=2026-04-30<br /> |DS=DS4<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44309 2026-04-20T08:33:46Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> &lt;!--<br /> == WHILE/LOOP Simulator ==<br /> <br /> Wir bieten einen [https://tools.iccl.inf.tu-dresden.de/while/ Online-Simulator für WHILE- und LOOP-Programme] an. Der Simulator unterstützt zusätzlich zu den Grundsprachen einige der Abkürzungen aus der Vorlesung. Im Menü unter ''Beispiele'' finden sich einige Beispielprogramme, die in das Programmfeld kopiert werden können.<br /> <br /> Der Simulator wurde von Simon Meusel entwickelt. Der Quellcode ist frei verfügbar unter https://github.com/knowsys/while-simulator . Pull-Requests sind Willkommen.<br /> --&gt;<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=3. Verfahren zum Logischen Schließen<br /> |Room=HÜL/S386<br /> |Date=2026-04-20<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-03-overlay.pdf, TheoLog2026-Vorlesung-03-print.pdf<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-03-print.pdf&diff=44308 2026-04-20T08:33:33Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-03-overlay.pdf&diff=44307 2026-04-20T08:33:26Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Vorlage:Publication_Report&diff=44297 2026-04-16T18:21:59Z

<p>Markus Krötzsch: </p> <hr /> <div>&lt;noinclude&gt;This template is used to generate an annual report for publications that match a given query criterion (parameter 1).<br /> <br /> &lt;/noinclude&gt;&lt;includeonly&gt;Overall statistics:<br /> &lt;ul class=&quot;link-list&quot;&gt;<br /> &lt;li&gt;&lt;span class=&quot;badge&quot;&gt;{{#ask: [[Kategorie:Publikation]] {{{1|}}} | format = count }}&lt;/span&gt;<br /> publications (including edited proceedings, technical reports, misc.)&lt;/li&gt;<br /> &lt;li&gt;&lt;span class=&quot;badge&quot;&gt;{{#ask: [[Kategorie:Publikation]] {{{1|}}} [[Bibtype::!Proceedings]] [[Bibtype::!Techreport]] [[Bibtype::!Deliverable]] [[Bibtype::!Misc]] [[Bibtype::!Phdthesis]]| format = count }}&lt;/span&gt; regular publications (excluding proceedings, technical reports, project reports, PhD theses, misc.; including books, book chapters, regular papers) <br /> &lt;li&gt;&lt;span class=&quot;badge&quot;&gt;{{#ask: [[Kategorie:Publikation]] {{{1|}}} [[Bibtype::!Proceedings]] [[Bibtype::!Techreport]] [[Bibtype::!Deliverable]] [[Bibtype::!Misc]] [[Bibtype::!Phdthesis]] [[Referiert::true]]| format = count }}&lt;/span&gt; regular publications that were reviewed<br /> &lt;/ul&gt;<br /> <br /> <br /> {{#maketabs:<br /> |2012={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2012]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2012}}|HIDETHISTAB}}<br /> |2013={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2013]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2013}}|HIDETHISTAB}}<br /> |2014={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2014]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2014}}|HIDETHISTAB}}<br /> |2015={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2015]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2015}}|HIDETHISTAB}}<br /> |2016={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2016]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2016}}|HIDETHISTAB}}<br /> |2017={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2017]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2017}}|HIDETHISTAB}}<br /> |2018={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2018]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2018}}|HIDETHISTAB}}<br /> |2019={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2019]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2019}}|HIDETHISTAB}}<br /> |2020={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2020]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2020}}|HIDETHISTAB}}<br /> |2021={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2021]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2021}}|HIDETHISTAB}}<br /> |2022={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2022]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2022}}|HIDETHISTAB}}<br /> |2023={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2023]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2023}}|HIDETHISTAB}}<br /> |2024={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2024]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2024}}|HIDETHISTAB}}<br /> |2025={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2025]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2025}}|HIDETHISTAB}}<br /> |2026={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2026]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2026}}|HIDETHISTAB}}<br /> |2027={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::2027]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|{{Annual Publication Query|{{{1|}}}|2027}}|HIDETHISTAB}}<br /> |TODO={{#ifeq:{{#ask: [[Kategorie:Publikation]] [[Year::&gt;2028]] {{{1|}}} | limit=1 |default=none|mainlabel=-|searchlabel=|intro=some}}|some|Too far into the future! Go to [[:Template:Publication Report]] and add more tabs by copying and modifying the ones that are there|HIDETHISTAB}}<br /> }}<br /> &lt;/includeonly&gt;</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Theoretische_Informatik_und_Logik_(SS2026)&diff=44289 2026-04-15T19:41:37Z

<p>Markus Krötzsch: </p> <hr /> <div>{{Vorlesung<br /> |Title=Theoretische Informatik und Logik<br /> |Research group=Wissensbasierte Systeme<br /> |Lecturers=Markus Krötzsch<br /> |Tutors=Stephan Mennicke; Maximilian Marx; Lukas Gerlach; Anna Dolma Hornschild; Florens Förster; Cornelius Lübke<br /> |Term=SS<br /> |Year=2026<br /> |Lecture series=Theoretische Informatik und Logik<br /> |Matrix=#theolog:tu-dresden.de<br /> |Module=INF-25-BA-LUK, INF-B-290, INF-D-330, INF-LE-EUI<br /> |SWSLecture=4<br /> |SWSExercise=2<br /> |SWSPractical=0<br /> |Exam type=Klausur<br /> |Description=== Beschreibung ==<br /> <br /> Die Lehrveranstaltung vermittelt eine vertiefende Einleitung in die theoretische Informatik, mit den Schwerpunkten Logik und Komplexitätstheorie. Themen sind unter anderem die Aussagen- und die Prädikatenlogik und deren Bezug zu Komplexität und Datenbanken, automatisches Schließen, Modallogiken und weiterführende Inhalte. <br /> <br /> Im Sommersemester 2026 wird die Lehrveranstaltung zum letzten Mal unter dem Titel ''Theoretische Informatik und Logik'' angeboten bevor sie mit dem Übergang zu den neuen Studienordnungen im Herbst 2026 durch die Lehrveranstaltung ''Logik und Komplexitätstheorie'' ersetzt wird. Die Inhalte werden bereits entsprechend angepasst und unterscheiden sich daher teilweise von denen der Vorjahre. Studierende der neuen Studienordnungen können die Veranstaltung bereits im neuen Modul prüfen.<br /> <br /> Die Vorlesung baut auf den Grundlagen aus der Veranstaltung [[Formale Systeme]] auf.<br /> <br /> === Nutzung von Z3 ===<br /> <br /> Wir nutzen in dieser Vorlesung und den dazugehörigen Übungen die SMT-Solver [https://www.microsoft.com/en-us/research/project/z3-3/ Z3], der sich über ein [https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#using-z3py-locally Python Binding] lokal nutzen lässt. Eine Beispielumgebung finden Sie unter [https://colab.research.google.com/drive/1H4Ek7uqI5qJzEzOMzfYxiuyMt21snUhk?usp=sharing Google Colab], die Sie sich herunterladen oder klonen können, um selbst damit weiterzuarbeiten.<br /> <br /> == Vorlesungen ==<br /> <br /> Die Vorlesungstermine sind<br /> * montags 3.DS (11:10&amp;ndash;12:40) in [[HÜL/S386]] sowie<br /> * donnerstags 4.DS (13:00&amp;ndash;14:30) in [[HSZ/0002]].<br /> <br /> Die erste Vorlesung findet am Montag, dem 13. April 2026 statt.<br /> <br /> == Übungen ==<br /> <br /> &lt;!--<br /> Die Einschreibung in die Übungsgruppen wird über [https://bildungsportal.sachsen.de/opal/url/RepositoryEntry/44106088449 OPAL] erfolgen.--&gt;<br /> <br /> Die Einschreibung ist ab Montag, dem 13. April 2026, 15:00 Uhr möglich. Für die Teilnahme an einer Übungsgruppe ist die Einschreibung in dieser Gruppe '''verpflichtend'''. Studierenden ohne Einschreibung kann die Teilnahme an einer selbst gewählten Übung nicht garantiert werden. Übungsleiter sind berechtigt, nicht eingeschriebene Studierende bei Überfüllung der Übung zu verweisen.<br /> <br /> &lt;!--<br /> Die folgenden Termine für Übungen werden von uns angeboten:<br /> * '''Gruppe A''': montags 5. DS (14:50-16:20) in [[APB E008]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe B''': dienstags 5. DS (14:50-16:20) in [[APB E006]] (Übungsleiter: [[Dörthe Arndt]])<br /> * '''Gruppe C''': mittwochs 3. DS (11:10-12:40) in [[APB E008]] (Übungsleiter: Anton Claußnitzer)<br /> * '''Gruppe D''': mittwochs 5. DS (14:50-16:20) in [[APB E010]] (Übungsleiter: Florens Förster)<br /> * '''Gruppe E''': donnerstags 3. DS (11:10-12:40) in [[APB E006]] (Übungsleiter: [[Marcos Cramer]])<br /> * '''Gruppe F''': donnerstags 5. DS (14:50-16:20) in [[POT 0106]] (Übungsleiter: Linus Wemmer)<br /> * '''Gruppe G''': freitags 2. DS (9:20-10:50) in [[APB E009]] (Übungsleiter: [[Stephan Mennicke]])<br /> --&gt;<br /> <br /> Die Einschreibungen in die Übungsgruppen erfolgt über '''[https://bildungsportal.sachsen.de/opal/auth/RepositoryEntry/53973614593/CourseNode/1775702163109381006 die OPAL-Seite der Lehrveranstaltung]'''.<br /> <br /> Der Übungsbetrieb startet '''am 20. April 2026''' zu Ihren jeweiligen Terminen in den angegebenen Räumen. Die Übungsblätter können in der Spalte der jeweiligen Übung unter ''Termine und Unterlagen'' heruntergeladen werden.<br /> <br /> &lt;!--<br /> == WHILE/LOOP Simulator ==<br /> <br /> Wir bieten einen [https://tools.iccl.inf.tu-dresden.de/while/ Online-Simulator für WHILE- und LOOP-Programme] an. Der Simulator unterstützt zusätzlich zu den Grundsprachen einige der Abkürzungen aus der Vorlesung. Im Menü unter ''Beispiele'' finden sich einige Beispielprogramme, die in das Programmfeld kopiert werden können.<br /> <br /> Der Simulator wurde von Simon Meusel entwickelt. Der Quellcode ist frei verfügbar unter https://github.com/knowsys/while-simulator . Pull-Requests sind Willkommen.<br /> --&gt;<br /> <br /> == Unterlagen ==<br /> <br /> Die vollständigen Foliensätze zur Vorlesung erscheinen bis zur Woche der Vorlesung online (siehe ''Termine und Unterlagen''). Weiterführende Literatur ist unter ''Literatur'' angegeben. Die Quellen der Vorlesungsfolien sind auf github verfügbar: https://github.com/knowsys/TheoLog<br /> <br /> (C) Markus Krötzsch, https://iccl.inf.tu-dresden.de/web/TheoLog2026, CC BY 3.0 DE<br /> <br /> Bildrechte können davon abweichen und sind gesondert in den LaTeX-Dateien angegeben. Die Foliensätze enthalten keinerlei Texte, die aus Werken entnommen sind, für welche die VG Wort Verwertungsrechte vertritt.<br /> <br /> Die Nutzung der Materialien in eigenen Lehrveranstaltungen ist willkommen, sofern der obige Lizenztext in allen abgeleiteten Foliensätzen angegeben wird. Rückmeldungen sind ebenfalls willkommen (z.B. als Issue zu diesem Repository); wir verlinken hier gern auf die Homepages der entsprechenden Kurse. Interessierte Lehrende können ihre abgewandelten Quellen auch mit in diesem Respository veröffentlichen -- kontaktieren Sie Prof. Krötzsch.<br /> <br /> Die Folien wurden erstellt von Markus Krötzsch. Eine vollständige Liste der Beitragenden ist unter https://github.com/mkroetzsch/TheoLog/graphs/contributors zu finden.<br /> <br /> == Kontakt ==<br /> <br /> Zur Kommunikation unter Vorlesungsteilnehmern der TU Dresden steht ein [https://matrix.tu-dresden.de/#/room/#theolog:tu-dresden.de Matrix-Kanal] zur Verfügung.<br /> <br /> Kommentare und Bug Reports können gern auch direkt über die entsprechenden Seiten auf github gepostet werden: https://github.com/mkroetzsch/TheoLog<br /> <br /> Persönliche Fragen können direkt an das Organisationsteam (siehe Links oben) gestellt werden, falls sie aus einem zwingenden Grund nicht über andere Kanäle gerichtet werden können. Allgemeine Fragen sollten Sie aber immer in geteilten Kanälen stellen, damit auch Ihre Kommilitoninnen und Kommilitonen davon profitieren (oder vielleicht sogar direkt helfen können).<br /> |Literature=Allgemein sind die Vorlesungsfolien und Übungsunterlagen ausreichend detailliert für das Studium. Weitere Lehrmaterialien können dennoch hilfreich sein, um Details nachzuschlagen oder sich weiter im Thema zu vertiefen.<br /> <br /> === Allgemeine Lehrbücher ===<br /> <br /> * Uwe Schöning: '''Theoretische Informatik -- kurz gefasst.''' Spektrum Akademischer Verlag.<br /> : ''(deutschsprachiger Standardtext; in der Tat ziemlich kurz gefasst)''<br /> * Michael Sipser: '''Introduction to the Theory of Computation.''' Cengage Learning.<br /> : ''(Standardtext zur Berechnung und Sprachen, speziell zum Thema Komplexität zu empfehlen; leider nur auf Englisch)''<br /> * Christopher Moore, Stephan Meterns: '''The Nature of Computation.''' Oxford University Press.<br /> : ''(sehr guter, moderner Text zu Komplexität und Berechnung, weniger formell; leider nur auf Englisch)''<br /> * John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: '''Einführung in Automatentheorie, Formale Sprachen und Berechenbarkeit.''' Pearson Studium.<br /> : ''(aus dem Englischen übertragenes Standardwerk; Original ev. besser)''<br /> <br /> === Unterhaltung ===<br /> <br /> Besonders spannende und interessante Themen aus der theoretischen Informatik und der Geschichte ihrer Protagonisten kann man auch in weniger formalen Texten nachlesen:<br /> <br /> * Apostolos Doxiadis, Christos Papadimitriou: '''Logicomix: An Epic Search for Truth.''' Bloomsbury<br /> : ''(Graphic Novel, inspiriert von Russels Leben und der Geschichte der Logik, wenn auch in Teilen frei erfunden)'' <br /> * Scott Aaronson: '''Quantum Computing Since Democritus.''' Cambridge<br /> : ''(informeller Text (eigentlich eine Sammlung von Blogeinträgen) mit interessanten Denkanstößen rund um Berechnung und Komplexität)''<br /> * Douglas Hofstadter: '''Gödel, Escher, Bach: An Eternal Golden Braid.''' Basic Books<br /> : ''(der Klassiker; in viele Sprachen übersetzt, aber im Original am besten)''<br /> <br /> === Berechnung und Komplexität ===<br /> <br /> Die Bücher von Sipser und Moore &amp; Mertens sind hier bereits sehr gute Referenzen. Wer darüber hinaus noch mehr Details sucht, der kann die folgenden Fachbücher konsultieren:<br /> <br /> * Christos H. Papadimitriou: '''Computational Complexity''' Academic Internet Publ., 2007.<br /> : ''(Standardwerk zu vielen Themen der Komplexitätstheorie)''<br /> * Sanjeev Arora, Boaz Barak: '''Computational Complexity: A Modern Approach''' Cambridge University Press.<br /> : ''(Detailllierter und umfangreicher Text zur Komplexitätstheorie)''<br /> <br /> === Prädikatenlogik ===<br /> <br /> Die Vorlesungsfolien sollten bei diesem Thema ausreichen. Die Darstellung des Themas in der Literatur ist ziemlich uneinheitlich, so dass verschiedene Bücher oft leicht unterschiedliche Definitionen verwenden. Wer dennoch weitere Details nachschlagen will, dem nützen eventuell die folgenden Bücher:<br /> <br /> * Uwe Schöning: '''Logik für Informatiker.''' Spektrum Akademischer Verlag.<br /> : ''(leichte Abweichungen in Notation und Darstellung)''<br /> * Martin Kreuzer, Stefan Kühling: '''Logik für Informatiker.''' Pearson Studium.<br /> : ''(sehr knapp und informell; eventuell interessant als Quelle für Übungsaufgaben)''<br /> * [[Steffen Hölldobler]]: '''[[Book3008|Logik und Logikprogrammierung]].''' Synchron Verlag.<br /> : ''(Schwerpunkt auf Logikprogrammierung und Prädikatenlogik)''<br /> * [[Steffen Hölldobler]], [[Sebastian Bader]], [[Bertram Fronhöfer]], [[Ursula Hans]], [[Pascal Hitzler]], [[Markus Krötzsch]], [[Tobias Pietzsch]]: '''[[Book3001|Logik und Logikprogrammierung, Band 2: Aufgaben und Lösungen]]''' Synchron Verlag<br /> : ''(Aufgabensammlung aus den Logikvorlesungen vergangener Jahre)''<br /> <br /> === Spezielle Themen ===<br /> <br /> * Torkel Franzén: ''''Gödel's Theorem: An Incomplete Guide to Its Use and Abuse.''' A K Peters.<br /> : ''(Gut verdaulicher Text zu Gödels Unvollständigkeitssätzen, einschl. deren Beziehungen zur Berechenbarkeitstheorie)''<br /> * Raymond M. Smullyan: '''A Beginner's Guide to Mathematical Logic.''' Dover Publications, 2014.<br /> : ''(Erster Teil: Einleitung und Logikrätsel. Zweiter Teil: Umfassende Entwicklung von Gödels Unvollständigkeitsbeweisen mit Gödel-Nummern und Gödel-Sätzen)''<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=1. Einleitung / Syntax und Semantik der Aussagenlogik<br /> |Room=HÜL/S386<br /> |Date=2026-04-13<br /> |DS=DS3<br /> |Download=TheoLog2026-Vorlesung-01-overlay.pdf, TheoLog2026-Vorlesung-01-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=2. Logische Schlussfolgerungen und Äquivalenzen<br /> |Room=HSZ/0002<br /> |Date=2026-04-16<br /> |DS=DS4<br /> |Download=TheoLog2026-Vorlesung-02-overlay.pdf, TheoLog2026-Vorlesung-02-print.pdf<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Übung<br /> |Title=Übungsblatt 1<br /> |Room=--<br /> |Date=2026-04-19<br /> |DS=terminlos<br /> |Download=TheoLog2026-Uebung-01.pdf<br /> }}</div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-02-print.pdf&diff=44288 2026-04-15T19:41:32Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:TheoLog2026-Vorlesung-02-overlay.pdf&diff=44287 2026-04-15T19:41:19Z

<p>Markus Krötzsch: </p> <hr /> <div></div>

Markus Krötzsch