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

Die Vorlesung findet montags um 16:15 – 17:45 im H7 (Erwin-Rommel-Straße 60) statt. Die Tutorien beginnen in der dritten Semesterwoche (26.10-30.10). Anmeldung zu den Tutorien über MeinCampus, voraussichtlich Mo. 12.10, 18:00 bis Mi. 14.10, 24:00.

Klausur

Zur Klausur sind sämtliche papierbasierten Hilfsmittel zugelassen. Zur Vorbereitung empfiehlt sich ein Blick auf die Probeklausur.
Information zu Bonuspunkten (aktualisiert 11.03).

Übungsblätter

Ü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.

Termin	Zeit	Raum	Tutor
Montag	10:15 – 11:45	01.150-128	Tobias Wilhelm
Mittwoch	12:15 – 13:45	R4.15	Christoph Rauch
Mittwoch	12:15 – 13:45	01.150-128	Lukas Braun
Mittwoch	12:15 – 13:45	01.153-113	Johannes Kern
Donnerstag	14:15 – 15:45	0.154-115	Daniel Hausmann
Donnerstag	14:15 – 15:45	HF-Technik: SR5.14	Dominik Paulus
Donnerstag	14:15 – 15:45	K2-119	Ludwig Dietel
Donnerstag	14:15 – 15:45	0.151-115	Hans-Peter Deifel
Freitag	08:15 – 09:45	H3 Egerlandstr.3	Tobias Polzer
Freitag	08:15 – 09:45	K1-119	Judith Bauer
Freitag	08:15 – 09:45	H15	Paul Wild
Freitag	14:15 – 15:45	02.134-113	Daniel Hausmann

Intensivübungen

Intensivübungen finden Donnerstags von 16:15 bis 17:45 in Raum 02.133-113 statt. Tutor: Sergey Goncharov.

Video-Aufzeichnung

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

Hilfsmaterial

Es existiert ein inoffizielles Skript, das wohl nicht mehr sinnvollerweise inoffiziell genannt werden kann. Dennoch ist der Inhalt des Skripts während des Vorlesungszeit stets als vorläufig anzusehen, insbesondere hinsichtlich des Umfangs des Materials; will sagen, es kann ggf. Material dazukommen. Eine Version, die dem tatsächlichen Ablauf der Veranstaltung entspricht, wir 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
Coq-Beispiele aus der Vorlesung in und
Coq-Beispiele aus Übung 4: zu und

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: Natürliches Schliessen, Coq)
- Übung 9 (Prädikatenlogik: Substitution, Unifikation)
- Übung 10 (Prädikatenlogik: Normalformen, Resolution)
- Übung 11 (Prädikatenlogik: Modelle, Fitch/Coq mit Induktion)