Theoretical Computer Science

Vorlesung: Einführung in die Logik

Sommersemester 2018 in Braunschweig

Neuigkeiten

• Raumaufteilung für die Klausur (2018-08-23, 08:30-10:30): gerade Matrikelnummern in PK 15.01, ungerade Matrikelnummern in SN 19.01. Die Klausureinsicht findet am Donnerstag, 2018-08-30, von 13:00 bis 15:00 vermutlich im PK 358 statt.
• Die Übungsklausur wird am Montag, 2018-08-13 ab 11:00 Uhr in PK 2.2 besprochen.
• Die Übungsklausur mit Lösungen findet sich hier.
• Die Einführung in das Beweisen findet sich hier.
• Die erste Vorlesung findet Mittwoch, 2018/04/04 von 09:45 - 11:15 in Raum PK 2.2 statt. Damit wir realistische Teilnehmerzahlen bekommen und sinnvolle Übunstermine auswählen können, ist es wichtig, dass Sie (mindestens) zur ersten Vorlesung erscheinen.
• Der Übungsbetrieb beginnt in der zweiten Vorlesungswoche. Nähere Informationen erhalten Sie in der ersten Vorlesung.
• Zettel zur (unverbindlichen) Anmeldung für die Übungsgruppen werden ab Donnerstag, 2018/04/05, 11:00 neben Raum IZ 343 verfügbar sein.

Vorlesung

• Die Vorlesung wird von Dr. Jürgen Koslowski und Prof. Dr. Roland Meyer gehalten.
• Ein Skript wird parallel zur Vorlesung bereitgestellt (s.u).
• Eintrag im Vorlesungsverzeichnis: Vorlesung, Übung.
• Vorlesungstermine:
  • Mittwoch, 09:45 - 11:15 in PK 2.2

Übungsbetrieb

• Die Übungen beginnen in der Woche 2018/04/09-13.
• Alle Übungen finden im Gebäude des Instituts für Theoretische Informatik statt. Die Übungstermine sind wie folgt:
  
  
  • Gruppe 0: Mo, 13:15 - 14:45 in 358, Herr Harz
  • Gruppe 1: Di, 13:15 - 14:45 in 305, Frau Tonn
  • Gruppe 2: Di, 15:00 - 16:30 in 305, Herr Lampe
  • Gruppe 3: Do, 11:30 - 13:00 in 358, Herr Holzhüter
  • Gruppe 4: Do, 11:30 - 13:00 in 305, Herr Koslowski
  • Gruppe 5: Do, 15:00 - 16:30 in 358, Herr Palm
  • Gruppe 6: Fr, 08:00 - 09:30 in 358, Herr Köcher
  • Gruppe 7: Fr, 11:30 - 13:90 in 358, Frau Bolle
  Die Übungstermine, die in den Gruppen 1 und 2 am 1. Mai ausfallen werden am 8 Mai nachgeholt. Dafür entfallen in der Woche vom 7. bis 11. Mai die Termine in allen übrigen Gruppen.
  
• Es gibt jede Wochen ein Übungsblatt zur Abgabe. Ihre Lösungen reichen Sie bitte in Gruppen von 2 Personen ein, Einzelabgaben bitte nur in begründeten Ausnahmefällen. Dazu dient eine Box im Institut für Theoretische Informatik, neben Büro 343. Die Lösungen werden in den Übungsstunden besprochen.

Präsenzsblätter

• 2018-04-09: Blatt 0 (in Aufgabe 4 müssen Sie die Rolle des SAT-Solvers übernehmen!), mit Lösungen der Präsenzaufgaben
• 2018-04-16: Blatt 1 mit Lösungen der Präsenzaufgaben
• 2018-04-23: Blatt 2 mit Lösungen der Präsenzaufgaben und der optionalen HA
• 2018-04-30: Blatt 3 mit Lösungen der Präsenzaufgaben und Aufgabe 4, verbesserte Formulierung und Lösung von Aufgabe 2
• 2018-05-14: Blatt 4 mit Lösungen aller Aufgaben (ausnahmsweise)
• 2018-05-28: Blatt 5; mit Lösungen der Präsenzaufgaben
• 2018-06-04: Blatt 6; mit Lösungen der Präsenzaufgaben
• 2018-06-11: Blatt 7; mit Lösungen der Präsenzaufgaben
• 2018-06-19: Blatt 8; mit Lösungen der Präsenzaufgaben
• 2018-06-26: Blatt 9; mit Lösungen der Präsenzaufgaben
• 2018-07-02: Blatt A; mit Lösungen der Präsenzaufgaben

Prüfungsmodalitäten

• Prüfungsleistung: Schriftliche Abschlussklausur: Donnertag, 2018-08-23, 08:30-10:30, PK 15.01 und SN 19.01. . Raumaufteilung: gerade Matrikelnummern in PK 15.01, ungerade Matrikelnummern in SN 19.01. Zur Klausur darf ein beidseitig (handschriftlich!) beschriebenes DIN A4-Blatt mitgebracht werden.
• Studienleistung: Sie müssen auf den Übungsblättern mindestens 50 Prozent der Punkte erreichen.

Material

1. Iteratives Bounded-Model-Checking. (Woche 1)
2. Einführung in das Beweisen. (Woche 2)
3. Syntax und Semantik der Aussagenlogik, Kompaktheitssatz. (Woche 2, 3)
4. Deduktionstheorem, Beweise. (Woche 4)
5. Vollständigkeit, Sequenzen, Tableaus. (Woche 5)
6. Beispiele Davis-Putnam und Resolution, Widerlegungsvollständigkeit der Resolution. (Woche 6)
7. Syntax und Semantik der Prädikatenlogik erster Stufe. (Woche 7)
8. Substitution und Normalformen. (Woche 8)
9. Herbrand-Theorie. (Woche 9)
10. Allgemeingültigkeit. (Woche 10)
11. Kompaktheitssatz. (Woche 11)
12. Theorien. (Woche 12)
13. Tableaus und Unifikation. (Woche 13)
14. Prädikatenlogische Resolution. (Woche 14)
15. Zusätzliche Notizen zu Nichtstandardmodellen.

Information in English

Literatur

• Enderton: A Mathematical Introduction to Logic, Academic Press.
• Schöning, Logik für Informatiker, Spektrum Akademischer Verlag.
• Ebbinghaus et. al., Einführung in die mathematische Logik, Spektrum Akademischer Verlag.
• Huth and Ryan, Logic in Computer Science, Cambridge University Press.
• Ben-Ari: Mathematical Logic for Computer Science, Springer-Verlag.
• Kreuzer, Kühling: Logik für Informatiker, Pearson.
• Nissanke: Introductory Logic and Sets for Computer Scientists, Pearson.
• Yosuhara: Recursive Function Theory and Logic, Academic Press.

• The Davis-Putnam algorithm is described here (Slides 1 to 8) and here. Note that we use the rules pure, unit, subsumption reduce, and splitting. You have to use them in this order, as is defined in pseudo code on our Slide 120. The examples on Slides 117 and 118 of our lecture will be helpful. There is quite some material on the web, search for Davis-Putnam or DPLL algorithm.
• Resolution is explained here (Slides 1 to 6 on Page 1) and here. Please also check the examples on our Slides 125 to 127. Alternatively, you can google for resolution rule and propositional logic.
• The tableau method is described here and here (we decompose conjunctions). Also check the examples on our Slides 77, 87 to 90. Again, Google may provide more information.
• Our system F0 is precisely what is described in Gaifman's notes. Up to the third axiom, it coincides with system H2 that Anita Wasilewska discusses in Chapter 8 (starting from Page 10) and Chapter 9 of her book.
• The sequent calculus is introduced (in slightly different notation) under the name Gentzen Style Proof System in Anita Wasilewska's Chapter 11.
• A good overview of topics on predicate logics can be found here.
• An introduction to predicate logic together with a description of Herbrand theory, unification, and resolution can be found in this course on artificial intelligence. Concerning the syntax of predicate logic, you may prefer to use our notation on Slides 144 to 147 (syntax) and 155 to 158 (semantics).
• The tableaux method for predicate logic is explained in these notes.
• A proof of undecidability of validity via a reduction of PCP can be found here. You may compare the development with Slides 190 to 194.
• Quantifier elimination in QBF is described here (cf. Slides 171 and 172).
• Gödel's System F is explained in Enderton's book as well as Slides 199 to 212.
• First-order theories are introduced here, the relationship between axiomatizability and decidability is discussed here. More information is given on Slides 213 to 225.
• Lecture notes in English by Haim Gaifman can be found here.
• This course by Anita Wasilewska comes with slides as well as lecture notes in English.