Hauptseminar mathematische Logik (S2A2)

Dozenten

• Prof. Dr. Peter Koepke
• Dr. Ioanna Dimitriou

Zeit und Ort

• Dienstags 14:00 - 16:00, N0.008 - Neubau

Inhalt

Dieses Seminar ist eine Einführung in das automatische Theorembeweisen. Wir werden sehen wie mathematische Beweise formell beschrieben werden können, und wie ein Computeprogram diese Beweise auf korrektheit überprüfen kann. Wir folgen John Harrisons Buch ''Handbook of Practical Logic and Automated Reasoning''. Voraussetzung für das Seminar sind Grundlagen der mathematischen Logik, z.B. die Vorlesung ''Einführung in die mathematische Logik''.

Vorträge

• 27. Oktober ; Dimitriou ; OCaml made light of, 1. Teil (Appendix 2).
  • Handout
  • Aufgaben und Lösungen (wird mir eure Lösungen geupdated werden).
• 03. November ; Dimitriou ; OCaml made light of, 2. Teil (Appendix 2).
  • Aufgaben und Code für die Aufgaben des ersten Kapitels..
  • Liste mit die Funktionen und die Beispiele des 2. Treffens.
• 10. November ; Höfer ; Aussagenlogik (§2.1-2.3) und die Davis-Putnam Procedure (§2.9)
• 17. November ; Höfer ; Die Davis-Putnam Procedure in OCaml
  Dazu werden wir ausgewälte Übungen anschauen. Schicken Sie gewünschte Übungen hier.
• 24. November ; Broll ; Logik erster Stufe und Skolemizerung (§3.1-3.6)
• 01. Dezember ; Broll ; Skolemizierung #2 ; und Aufgaben (Tröbst)
• 08. Dezember Termin fällt aus
• 15. Dezember Termin fällt aus
• 22. Dezember ; Stehr ; Unifikation, Tableaux und Resolution.
• 12. Januar ; Tröbst ; LCF
  [mölicherweise auch am 19. Januar]
• 26. Januar ; Hamm ; Stile für interaktive Beweisüberprüfungen
  [möglicherweise auch am 02. Februar]

Installation von Software

Linux (Debian/Ubuntu):

• OCaml und Camlp5 installieren: Geben Sie im Terminal (Str+Alt+T) folgendes ein
  (sudo) apt-get install ocaml camlp5
• Harrisons Program herunterladen: www.cl.cam.ac.uk/~jrh13/atp/OCaml.tar.gz und auspacken.

Windows:
Leider funktioniert camlp5 unter Windows nicht. Man kann aber Linux von ein USB-Stick wie folgt ausführen.

• Einen leeren USB-Stick mit mindestens 3GB Speicherplatz bereit haben.
• Ubuntu .iso herunterladen: www.ubuntu.com/download/
• Pendrivelinux herunterladen: www.pendrivelinux.com
• Das letzte heruntergeladene Program ausführen und folgendes auswählen:
  • Step 1: Ubuntu
  • Step 2: Die von Ihnen heruntergeladene .iso Datei auswählen
  • Step 3: Den dafür behaltenen USB-Stick einstecken und auswählen.
  • Step 4: So viel MBs wie möglich auswählen
  • ,,Create`` clicken, damit USB-Stick formattieren und Ubuntu darauf installieren.
• Den Computer neustarten, und bevor es im Windows reingeht, mit F2 (normalerweise) den BIOS aufrufen. Da wechseln Sie die Bootreihenfolge, sodass der Ubuntu-USB-Stick zuerst hochfährt.
• Warten bis Ubutu aufgeladen ist, in einer Internetverbindung sich verbinden, und obige Anweisungen für Linux folgen (mit sudo ohne Klammern).