Bonn Mathematical Logic Group

Arbeitsgruppe 1 - Formale Mathematik

Natur- und Ingenieurwissenschaftliches Kolleg VI - Erste Kollegphase

Dozenten

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:

  1. Einführung (Koepke)
    Besprechung des Ablaufs der Kollegwoche, Installation, OCaml made light of.
    Einleitung (slides); Zusammenfassung für "OCaml made light of".
  2. Aussagenlogik, PLAR 2.1 - 2.4 [IPT S. 3 - 4];
    Slides
  3. Normalformen, PLAR 2.5, 2.6, 2.8 [IPT 1.3.1]
    Slides
  4. Aufgaben zu:
    OCaml
    Aussagenlogik und Normalformen: Teil 1, Teil 2
Dienstag:
  1. Davis-Putnam-Verfahren, PLAR 2.9, [IPT 1.3.4, Completeness Theorem]
    Slides
    Weitere Erklärungen zu DPLL.
  2. Logik erster Stufe, PLAR 3.1 - 3.4 [IPT 2.1]
    Slides
  3. Übungen zu 5. und 6.
Mittwoch:
  1. Normalformen, PLAR 3.5 und 3.6
  2. Satz von Herbrand, PLAR 3.7, 2.12, Theorem 3.25 [IPT 2.5.1]
  3. Anwendungen des Satzes von Herbrand, PLAR 3.8, 3.9
  4. Übungen zu Normalformen, und Herbrands Satz und Unification.
Donnerstag:
  1. Resolution, PLAR 3.11 - 3.13
  2. Prolog, PLAR 3.14 - 3.15
    Slides
  3. Übungen zu Resolution und Prolog (Lösungen).
  4. Vorbereitung der Gruppenpräsentation

Vortragsgruppen:

Literatur:

Installation von Software

Linux (Debian/Ubuntu):

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