Theoretical Computer Science

Vorlesung: Einführung in die Logik

Sommersemester 2020

Neuigkeiten

03. Sept

Aufgrund aktueller Lage kann die Einsicht nicht wie üblich stattfinden. Falls Sie die Klausur einsehen wollen, melden Sie sich bitte per E-Mail bei unserer Sekretärin Frau Soleinsky (a.soleinsky@tu-bs.de) zur Terminfindung. Die Ergebnisse finden Sie (nun wieder) hier (Statistik).

03. August

Raumaufteilung für die Klausur: Beginnt Ihr Nachname mit A-K: Sporthalle Beethovenstraße. Beginnt Ihr Nachname mit L-Z: Mensa 1.

03. August

Es gibt eine Korrektur auf den Folien 74 und 75, die blau hervorgehoben ist. Vielen Dank für den Hinweis!

29. Juli

Die Klausur findet am 04. August 14:30 statt. Der Prüfungsbeginn ist um 15:15. Die Räumlichkeiten sind Mensa 1, Sporthalle Beethovenstraße, Tentomax und Zi-24.1 (Grotrian). Am Montag, dem 03. August, wird hier bekannt gegeben, in welchem Raum Sie geprüft werden. Bitte lesen Sie sich die Bestimmungen der TU für Prüfungen während der Corona-Zeit durch. Zugelassen zur Klausur ist ein beidseitig handschriftlich beschriebenes DIN-A4 Cheat-Sheet.

10. Juli

Die Vorlesung in Woche 9 erscheint aufgrund von Terminkonflikten verspätet. Wir bitten um Entschuldigung.

01. Juli

Es gibt nun einen TU Rocket.Chat(link expires 15. Juli) für die Vorlesung. Neue Informationen bezüglich der Vorlesung werden auch dort vermittelt (sowie natürlich weiterhin auf dieser Website). Zudem können Sie sich mit anderen Studenten austauschen, Fragen stellen und beantworten. Desweiteren werde ich (Sören van der Wall) freitags (03. Juli, 10. Juli, 17. Juli) um 10:00 für eine Stunde im Chat sein und kann dort Fragen beantworten.

01. Juli

Der Klausurtermin steht nun fest: 04.08.2020 14:30-18:45 15:15-17:15. Es wird eine schriftliche Klausur geben. Weiter Informationen später.

7. Mai

Die Vorlesung wird von Prof. Dr. Meyer übernommen. Die ersten Vorlesungsvideos erscheinen in der nächsten Woche.

17. April

Zu den Übungen melden Sie sich bitte in Gruppen mit bis zu vier Personen per Mail an Sören van der Wall( s.van-der-wall@tu-bs.de) an. Bitte achten Sie darauf, in der Mail folgende Information anzugeben:

• Matrikelnummer,
• Nachname,
• Vorname,
• E-Mail-Adresse.

11. April

Die Vorlesungen und kleinen Übungen werden aufgrund der momentanen Situation nur online angeboten. Dazu werden hier auf dieser Seite die jeweiligen Veranstaltungen in Videoform hochgeladen. Hausaufgabenabgabe und -korrektur werden ebenfalls online stattfinden. Dazu sind die Hausaufgaben einzuscannen oder direkt als .pdf zu erstellen.

Vorlesung

• Der Dozent ist Prof. Dr. Roland Meyer (roland.meyer@tu-braunschweig.de).
• Eintrag im Vorlesungsverzeichnis: Vorlesung.
• Vorlesungstermine: Die Vorlesungen werden im Videoformat mittwochabends hochgeladen.

• Woche 1: Einführung und Kompaktheit

  Folien, Beispiel zur Semantik, Beweis des Lemmas zur Fortsetzung von Belegungen, Beweis der aufbauenden Folgerung, Beweis des Deduktionstheorems (semantische Version), Beweis des Kompaktheitssatzes.

• Woche 2: Deduktive Systeme

  Folien, Beispielbeweis zur Vollständigkeit einer Operatorenmenge, Beweis des Deduktionstheorems (syntaktische Version).

• Woche 3: F0

  Beweise in F0, Beweis mittels Inkonsistenz, Vollständigkeit von F0.

• Woche 4: Sequenzen, Typsysteme und Tableaus

  Folien zum Sequenzenkalkül, Beispielbeweis im Sequenzenkalkül, Typsysteme, Beispiele zu Tableaus. Folien zu Tableaus.

• Woche 5: Normalformen, Davis-Putnam

  Folien zu Normalformen, Beispiel zu Tseitin mit Syntaxbaum, Beispiele zu Davis-Putnam, Folien zu Davis-Putnam.

• Woche 6: Resolution, BMC

  Beispiel zur Resolution, Folien zur Resolution, Widerlegungsvollständigkeit der Resolution, Bounded-Model-Checking.

• Woche 7: Syntax und Semantik der Prädikatenlogik

  Folien, Lassie und Nemo.

• Woche 8: Substitution und Normalformen

  Folien, Beispiel zur Substitution, Anwendung des Substitutionslemmas, Pränexnormalform, Beispiel zur Skolemisierung, Beweis des Satzes von Skolem.

• Woche 9: Herbrand-Theorie

  Folien, Beispiel zu Herbrand-Strukturen, Beweis des Satzes von Herbrand.

• Woche 10: Algorithmus von Gilmore und Kompaktheit

  Folien, Beispiel zur Herbrand-Expansion, Diskussion zur Auffassung von E(A) als Menge aussagenlogischer Formeln, Beweis des Satzes von Gödel, Herbrand und Skolem, Beweis des Kompaktheitssatzes, Existenz von Nicht-Standardmodellen der Arithmetik.

• Woche 11: System F

  Folien.

Die Präsentation ist hier in Form von Videos zu finden. Ausführlichere Darstellungen des Inhalts finden Sie in den folgenden handschriftliche Notizen:

• Iteratives Bounded-Model-Checking
• Einführung in das Beweisen
• Syntax und Semantik der Aussagenlogik, Kompaktheitssatz
• Deduktionstheorem, Beweise
• Vollständigkeit, Sequenzen, Tableaus
• Beispiel zur Tseitin-Transformation
• Beispiele Davis-Putnam und Resolution, Widerlegungsvollständigkeit der Resolution
• Syntax und Semantik der Prädikatenlogik erster Stufe
• Substitution und Normalformen
• Herbrand-Theorie
• Allgemeingültigkeit
• Kompaktheitssatz der Prädikatenlogik
• Theorien
• Tableaus und Unifikation
• Prädikatenlogische Resolution
• Zusätzliche Notizen zu Nichtstandardmodellen.

• ausführliche Folien (mit allen Zwischenschritten) von 2019
• kompakte Folien (ohne Zwischenschritte) von 2019
• Folien von 2018
• Skript von 2017
• sehr lückenhaftes Skript von 2019

Übungsbetrieb

• Große Übungen werden in Form von Videos hochgeladen.
• Die kleinen Übungen werden von Tutoren gehalten. Die Tutoren werden abwechselnd ein Tutorium aufnehmen und auf dieser Seite zugänglich machen.
• Die E-Mail Adresse Ihres Gruppenleiters sollte Ihnen bereits bekannt sein. Sollte das nicht der Fall sein, melden Sie sich bitte bei Sören van der Wall (s.van-der-wall@tu-bs.de).

• Woche 1: Einführung in das Beweisen
• Woche 2/3: Deduktives Beweisen in F0 und Anwenden des Kompaktheitssatzes
• Woche 4/5: Satisfiability Checking - Algorithmen
• Woche 6/7: Prädikatenlogik - Syntax, Semantik und Bedeutsamkeit
• Woche 8/9/10: Herbrand-Theorie: Elimination der Gleichheit - Anwendung des Kompaktheitssatzes für Prädikatenlogik

Übungsblätter

• Übungsblatt 1 - Bis Do, 28.05.2020 23:59 - Lösungen
• Übungsblatt 2 - Bis Do, 11.06.2020 23:59 - Lösungen
• Übungsblatt 3 - Bis Do, 18.06.2020 23:59 - Lösungen
• Übungsblatt 4 - Bis Do, 25.06.2020 23:59 - Lösungen
• Übungsblatt 5 - Bis Do, 02.07.2020 23:59 - Lösungen - Fehler in 5.4: Datendomäne ist als nicht-leer definiert (Def. 4.7).
• Übungsblatt 6 - Bis Do, 09.07.2020 23:59 - Lösungen
• Übungsblatt 7 - Bis Do, 16.07.2020 23:59 - Lösungen
• Übungsblatt 8 - Bis Do, 23.07.2020 23:59 - Lösungen

Modul

• Prüfungsleistung: Zu erbringen durch Bestehen einer schriftliche Abschlussklausur zu Beginn des vorlesungsfreien Zeitraums.
• Studienleistung: Zu erbringen durch das erfolgreiche Bearbeiten von mindestens 50% der Übungsaufgaben.

Abschlussklausur

• Prüfungsleistung: Schriftliche Abschlussklausur: Dienstag, 2020-08-04, 14:30-18:45 Weitere Informationen zur Abschlussklausur werden wir Ihnen rechtzeitig zur Verfügung stellen.