Logik

Wintersemester 2011/2012

im Vorlesungsverzeichnis

 

Aktuelles

• Wer der Bekanntgabe seiner Klausurergebnisse vom 13.2. zugestimmt hat und die
  Klausur bestanden hat, findet seine Ergebnisse hier. Alle anderen Klausurteilnehmer
  erhalten in Kürze eine Mail (sofern die Email-Adresse bekannt ist).
  Herzlichen Glückwunsch an alle, die bestanden haben!
  
• Auf Folie 136 zur Aussagenlogik ("Sequenzenregeln") gab es einen Tippfehler in der
  Sequenzenregel für →-rechts. Bitte laden Sie die neue Version herunter und korrigieren
  Sie gegebenenfalls Ihre Unterlagen.
  
• Die Klausureinsicht findet statt am Freitag, den 17.2. von 10:15 - 11:30 Uhr in SR V.
  
• Die Nachklausur findet statt am Mittwoch, den 28.3. von 10-13 Uhr in HS C in der Chemie.
  

Hinweise auf Veranstaltungen im Sommersemester

• Für das kommende Semester suchen wir noch Tutoren für die Vorlesung Theoretische
  Informatik. Interessenten melden sich bitte bei Herrn Gumm.
• Außerdem möchten wir die mathematisch interessierten Hörer auf das Seminar
  "Kohomologie von Mannigfaltigkeiten und Gruppen" hinweisen. Informationen
  finden Sie hier, erste Vorbesprechung ist am Montag, den 6.2., 16:15 im Hörsaal V.
  Fragen richten Sie bitte an Herrn Lochmann.
  

Übungsblätter

• Blatt 1 (Version 3)
• Blatt 2 (Version 3)
• Blatt 3 (Version 3)
• Blatt 4 (Version 3)
• Blatt 5 (Version 3)
  (Benötigt dpll.pl und tuProlog)
• Blatt 6 (Version 3)
• Blatt 7 (Version 3)
  (Benötigt JAPE: die aktuellen Versionen finden Sie hier. Verwenden
  Sie zur Installation keinen Pfadnamen mit Leerzeichen!)
• Blatt 8 (Version 5)
• Blatt 9 (Version 3)
• Blatt 10 (Version 2)
• Blatt 11 (Version 3)
• Blatt 12 (Version 2)
• Blatt 13 (Version 3)
• Blatt 14 (Version 2)
  

In JAPE ist die Syntax für den Sequenzenkalkül so definiert, dass "∨"
stärker bindet als "∧". Das kann man leicht korrigieren, indem man die
Datei "../Jape/examples/sequent_calculus/sequent_syntax.j" öffnet. Dort
steht:
   INFIX 150L ∧
   INFIX 160L ∨
Das ändert man einfach in:
   INFIX 160L ∧
   INFIX 150L ∨
Dann sind die Präzedenzen so wie in der Vorlesung. Eine bereits
korrigierte Fassung der Datei finden Sie hier.

Folien und Dateien aus der Vorlesung

• Folien zur Aussagenlogik (komplett)
  (Tippfehler auf Folie 136 zur Sequenzenregel für →-rechts korrigiert.)
• Folien zur Prädikatenlogik (komplett)
  
• tuProlog und Prolog-Programme zum Download
• Installationsprogramm für Jape (Windows/Java)
• Installationsprogramm für Jape (Linux/Java)
  

Lösungsskizzen zu ausgesuchten Aufgaben

• Beispiele zu DPLL und Resolutionen
  
• Lösungsskizzen zu Blatt 5 (ver. 2)
• Lösungen zu zwei Aufgaben von Blatt 6
• Lösungsskizze zu Aufgabe 3.c auf Blatt 7
• Lösungsskizzen zu Blatt 8, Aufgaben 2,3,4
• Musterlösung zum Test vom 22.12.
• Lösung zu Blatt 12, Aufgabe 1 (Grundresolventenmethode)
  

Termine

• Vorlesung: Mo 10-12, HG 004 und Do 12-14, HG 007
• Klausur: Mo, 13.2.2012, 16:00 (s.t.) in HG 114
• Klausureinsicht: Fr, 17.2.2012, 10:15-11:30 in SR V
• Nachklausur: Mi, 28.3.2012, 10:00-13:00 in HS C (Chemie)
  

Bedingungen zur Klausurteilnahme

• Mindestens 50% der Punkte aus den Übungsblättern in der Summe.
• Aktive Mitarbeit in den Übungsgruppen, insbesondere also auch Anwesenheit.
  

Sprechzeiten

Prof. Dr. H. Peter Gumm	05D13      siehe Homepage
Dr. Andreas Lochmann	06D25      nach Vereinbarung

Literatur

• Logik für Informatiker, M. Kreuzer / S. Kühling, Pearson 2006
  
• Mathematical Logic for Computer Science, M. Ben-Ari, 2nd. ed., Springer Verlag 2001
  
• Logik für Informatiker, U. Schöning, 5. Aufl., Spektrum Akademischer Verlag 2000
• Logic in Computer Science - Modelling and Reasoning About Systems, M. Huth / M. Ryan, 2nd. ed., Cambridge Univ. Press. 2004
• Grenzen der Mathematik, D. Hoffmann, Spektrum Akademischer Verlag 2011
  

Wir erwarten, dass Sie das erstgenannte Buch (Kreuzer/Kühling) zur Vorlesung lesen.
Die folgenden vier Bücher sind zur Ergänzung empfohlen.