Grundlagen der Logik in der Informatik (WS 16/17)

Die Vorlesung findet montags um 16:15 – 17:45 im H7 (Erwin-Rommel-Straße 60) statt.

Erste Vorlesung: Montag 17.10.
Erstes Tutorium: Montag 24.10.

Anmeldung zu den Tutorien über MeinCampus (genaues Zeitintervall siehe im Univis).

Klausur

• Zur Klausur sind sämtliche papierbasierten Hilfsmittel zugelassen.
• Zur Vorbereitung empfiehlt sich ein Blick auf die Probeklausur.
• Eine Fragestunde zur Vorbereitung auf die anstehende Klausur findet am Dienstag, 28.03.2017 um 14:00 Uhr (s.t.) im Raum 01.150-128, Cauerstraße 11, 1. Stock statt.
• Bonuspunkte (Aktualisiert! Achtung: es sind nur Einträge von Studierenden gelistet, die Bonuspunkte erreicht haben; auf eine bestandene Klausur wird entsprechend den gelisteten Punkten ein Bonus von maximal 15% angerechnet).

Übungsblätter

• Übungsblatt 1 (rev.13716); Abgabe: 31.10.-04.11.
• Übungsblatt 2 (rev.13822); Abgabe: 07.11.-11.11.
• Übungsblatt 3 (rev.13875); Abgabe: 14.11.-18.11.
• Übungsblatt 4; Abgabe: 21.11.-25.11. – Coq-Beispiele (Präsenzaufgaben): ; Musterlösung zu den Fitch-Beweisen.
• Übungsblatt 5; Abgabe: 28.11.-02.12. – Coq-Beispiele (Präsenzaufgaben):
• Übungsblatt 6; Abgabe: 12.12.-16.12. 05.12.-09.12.
• Übungsblatt 7; Abgabe: 12.12.-16.12.
• Übungsblatt 8; Abgabe: 19.12.-23.12.
• Übungsblatt 9; Abgabe: 09.01.-13.01. – Coq-Beispiele (Präsenzaufgaben):
• Übungsblatt 10; Abgabe: 16.01.-20.01.
• Übungsblatt 11; Abgabe: 23.01.-27.01.
• Übungsblatt 12; Abgabe: 30.01.-03.02.

<!–

• Übungsblatt 1 (rev. 9993 10065); Abgabe: 2.11.-6.11.
• Übungsblatt 2 (rev. 10211); Abgabe: 9.11.-13.11.
• Übungsblatt 3; Abgabe: 16.11.-20.11.
• Übungsblatt 4 (rev. 10279); Abgabe: 23.11.-27.11.
• Übungsblatt 5; Abgabe: 30.11.-4.12. (Coq Beispiel: )
• Übungsblatt 6; Abgabe: 7.12.-11.12.
• Übungsblatt 7; Abgabe: 14.12.-18.12.
• Übungsblatt 8; Abgabe: 11.01.-15.01. (Das Trinkerparadoxon in Coq: )
• Übungsblatt 9; Abgabe: 18.01.-22.01. ()
• Übungsblatt 10; Abgabe: 25.01.-29.01.
• Übungsblatt 11 (rev. 10874); Abgabe: 1.02.-5.02. (, )

–>

Tutorien

Tutorien werden in Gruppen abgehalten, entsprechend dem folgenden Plan.

Intensivübungen

Intensivübungen finden Dienstags von 12:15 bis 13:45 in Raum 02.133-113 statt und werden von Dr. Sergey Goncharov abgehalten.

Video-Aufzeichnung

Die Vorlesung wird vom RRZE aufgezeichnet und ist auf der RRZE-Seite zu finden.

Hilfsmaterial

• Es existiert ein Skript (Rev. 15406), das wohl nicht mehr sinnvollerweise inoffiziell genannt werden kann. Dennoch ist der Inhalt des Skripts während der Vorlesungszeit stets als vorläufig anzusehen, insbesondere hinsichtlich des Umfangs des Materials; will sagen, es kann ggf. Material hinzukommen. Eine Version, die dem tatsächlichen Ablauf der Veranstaltung entspricht, wird erst nach Abschluss der Vorlesungen zur Verfügung gestellt.
• Notation.pdf — eine Kurzzusammenfassung relevanter mathematischer Begriffe und Schreibweisen.
• induktion.pdf — Hilfsblatt für Induktionsbeweise (von Thomas Voß).
• Coq Cheat Sheets von Amy Felty und Andrej Bauer und von uns.
• Folien zu den Tutorien (ohne Gewähr)
  • Übung 1 (Induktion)
  • Übung 2 (Aussagenlogik)
  • Übung 3 (Induktion für aussagenlogische Formeln)
  • Übung 4 (Aussagenlogik: Natürliches Schliessen)
  • Übung 5 (Aussagenlogik: Natürliches Schliessen, Coq)
  • Übung 6 (Aussagenlogik: Normalformen, Resolution)
  • Übung 7 (Aussagenlogik: optimierte Resolution)
  • Übung 8 (Prädikatenlogik: Syntax, freie Variablen, Substitution)
  • Übung 9 (Prädikatenlogik: Natürliches Schliessen, Coq)
  • Übung 10 (Prädikatenlogik: Unifikation)
  • Übung 11 (Prädikatenlogik: Modelle, Fitch mit Induktion)
  • Übung 12 (Prädikatenlogik: Normalformen, Resolution)

Vorläufiger Plan der Vorlesung