Arbeitsgruppe 1 - Formale Mathematik
Natur- und Ingenieurwissenschaftliches Kolleg VI - Erste Kollegphase
Dozenten
- Prof. Dr. Peter Koepke
- Dr. Ioanna Dimitriou
- Regula Krapf
Inhalt
Die formale Mathematik ist ein interdisziplinäres Gebiet zwischen Mathematik, Logik und Informatik Ihr Ziel ist die praktische Realisierung von vollständig formalen Beweisen mathematischer Sätze. Das ist auf Grund des Gödel'schen Vollständigkeitssatzes prinzipiell möglich, jedoch mit grossen Komplexitätsproblemen verbunden. Erst vor wenigen Jahren gelang es durch massiven Einsatz von Computern und durch die Entwicklung geeigneter Beweissprachen und Beweisalgorithmen, formale Beweise prominenter Theoreme wie des Vier-Farben-Satzes oder des Primzahlsatzes zu konstruieren Inwieweit die formale Mathematik die mathematische Praxis beeinflussen kann, ist eine offene Frage. In der Arbeitsgruppe "Formale Mathematik" werden wir theoretische Grundlagen erarbeiten, etablierte Systeme studieren und eigene Programmier- und Formalisierungsprojekte verfolgen. Dabei interessieren wir uns auch für die Einbeziehung von Methoden der Computerlinguistik zu einer natürlichen formalen Mathematik, deren Eingabesprache und Schlussweisen üblichen mathematischen Texten nahekommen.
Vorträge
Montag:
- Einführung (Koepke) Besprechung des Ablaufs der Kollegwoche, Installation, OCaml made light of. Einleitung (slides); Zusammenfassung für "OCaml made light of".
- Aussagenlogik, PLAR 2.1 - 2.4 [IPT S. 3 - 4];
Slides - Normalformen, PLAR 2.5, 2.6, 2.8 [IPT 1.3.1]
Slides - Aufgaben zu:
OCaml
Aussagenlogik und Normalformen: Teil 1, Teil 2
- Davis-Putnam-Verfahren, PLAR 2.9, [IPT 1.3.4, Completeness Theorem]
Slides
Weitere Erklärungen zu DPLL. - Logik erster Stufe, PLAR 3.1 - 3.4 [IPT 2.1]
Slides - Übungen zu 5. und 6.
- Normalformen, PLAR 3.5 und 3.6
- Satz von Herbrand, PLAR 3.7, 2.12, Theorem 3.25 [IPT 2.5.1]
- Anwendungen des Satzes von Herbrand, PLAR 3.8, 3.9
- Übungen zu Normalformen, und Herbrands Satz und Unification.
- Resolution, PLAR 3.11 - 3.13
- Prolog, PLAR 3.14 - 3.15
Slides - Übungen zu Resolution und Prolog (Lösungen).
- Vorbereitung der Gruppenpräsentation
Vortragsgruppen:
- Vorträge 2 und 3: Dorothee Henke, Leonie Mädje, Christian Schneider
- Vorträge 5 und 6: Amelie Flatt, Christian Offen, Carl Wanninger
- Vorträge 8 und 12: Paul Leon Götz, Felix Schremmer, Eike Maximilian Schulte
- Vorträge 9 und 10: Fabian Maximilian Kunze, Matthias Naaf, Felix Rech
- Vortrag 13: Maximilian Dore, Regula Krapf
Literatur:
- [PLAR] John Harrison, Handbook of Practical Logic and Automated Reasoning, CUP 2009 (www.cl.cam.ac.uk/~jrh13/atp/)
- [IPT] Samuel R. Buss, An introduction to proof theory, in: Samuel R. Buss (ed.), Handbook of Proof Theory, Elsevier 1998; auch auf der Homepage von Sam Buss, http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf
- Zusätzliche Aufgaben (und Lösungen) zu Harrison's Buch finden Sie hier.
- Gute Notizen, Aufgaben und Slides kann man auch auf Uwe Waldmanns Webseite fü die Vorlesung "Automated Reasoning" finden.
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.
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).