Praktikum Mathematische Logik (P2A1, also P4A1)
Lecturer
- Prof. Dr. Peter Koepke
Times
- Dienstags 14:15 - 16:00, N 0.003. Beginn: Erste Novemberhälfte 2019
Contents
Der Gödelsche Vollständigkeitssatz besagt, dass (alle) mathematische(n) Beweise im Prinzip in formalen Beweiskalkülen geführt werden können. Die tatsächliche Durchführung ist allerdings mit großen Komplexitätsproblemen verbunden, die nur durch Einsatz von Computern beherrscht werden können. In der Formalen Mathematik werden Kalküle praktisch implementiert, so dass mathematische Theorien tatsächlich vollkommen formalisiert und auf logische Korrektheit überprüft werden können.
In dem Praktikum Mathematische Logik benutzen wir die Beweis-Systeme LEAN und Naproche-SAD. LEAN ist ein aktueller Beweis-Assistent, der auf Typentheorie basiert. Wir stellen das System zu Beginn des Praktikums in eingeteilten Vorträgen aus dem Skript "Theorem Proving in LEAN" vor.
Die anschließenden Praktikumsprojekte werden sich damit befassen, Formalisierungen aus der LEAN Bibliothek in das System Naproche-SAD zu übertragen. Naproche-SAD ist ein Beweisprüfer, den wir zur Zeit in Bonn entwickeln und der auf Logik erster Stufe und Mengenlehre beruht. Besonderheit ist die Eingabe von Beweisen in einer (kontrollierten) natürlichen Sprache, die der gewöhnlichen mathematischen Sprache nahe kommt. Texte in Naproche-SAD können und sollen so formuliert werden, dass sie für Mathematiker unmittelbar lesbar sind.
Ziel der Projekte ist eine kleine Bibliothek "natürlicher" und korrekter mathematischer Texte für Naproche-SAD. Dabei können kleine Erweiterungen und Änderungen des Systems nötig sein, das in der funktionalen Programmiersprache Haskell geschrieben ist.
Die Teilnehmer sollten einigermaßen leistungsfähige Laptops haben, auf denen z.B. die augenblickliche Version von Naproche-SAD laufen kann. Man kann Naproche-SAD aber auch auf der Kommandozeile starten. Das Praktikum kommt zunächst wöchentlich zur angegebenen Zeit zusammen; der Beginn wird in der ersten Novemberhälfte liegen. Individuelle Projekte werde im Dezember festgelegt.
Es stehen ca. 10 Plätze zur Verfügung. Bitte bewerben Sie sich bis zum 1. November per Email an koepke@math.uni-bonn.de mit
- Ihrem Namen
- Matrikelnummer
- Email Adresse
- Studiengang
- Fachsemester
- Bisher oder augenblicklich besuchte Logikmodule
- Programmiererfahrungen
- Mögliche weitere Informationen