Praktikum Mathematische Logik (P2A1 / P4A1)
Dozent
- Prof. Dr.
Peter Koepke
Zeit
- Dienstags 14:15 - 16:00. Beginn: nach Vereinbarung
Automatisiertes Beweisen
Der Gödelsche Vollständigkeitssatz besagt, dass alle mathematischen 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, in denen einfache Beweise automatisch gefunden werden können und in denen umfangreiche Theorien formalisiert und auf logische Korrektheit überprüft werden können.
Die Bonner Arbeitsgruppe Naproche (Natural Proof Checking) entwickelt den interaktiven Beweisprüfer Naproche, der Beweise in einer (kontrollierten) natürlichen Sprache akzeptiert, die der gewöhnlichen mathematischen Sprache nahe kommt. Texte in Naproche können und sollten so formuliert werden, dass sie für Mathematiker/innen unmittelbar lesbar sind. Naproche kann als Teil der Beweiser-Plattform Isabelle benutzt werden. Einen ersten Eindruck bietet auch das Naproche-Webinterface.
Im Praktikum soll das Verhalten des automatischen Beweisers Eprover studiert werden, der innerhalb von Naproche für komplexe Beweisaufgaben benutzt wird. Dabei soll die Beweissuche für Naproche-typische Aufgaben nachverfolgt und verbessert werden.
Voraussetzungen sind die mathematische Logik etwa bis zum Vollständigkeitssatz und eine gute allgemeine Computerbeherrschung. Die Teilnehmer sollten einigermaßen leistungsfähige Laptops haben, auf denen z.B. die augenblickliche Version von Isabelle/Naproche unter Linux laufen kann.
Es steht eine begrenzte Anzahl von Plätzen zur Verfügung. Sie können sich ab sofort per Email an koepke@math.uni-bonn.de bewerben mit
- Ihrem Namen
- Matrikelnummer
- Emailadresse
- Studiengang
- Fachsemester
- Bisher besuchte Logikmodule
- Programmiererfahrungen
- Mögliche weitere Informationen
Practical Project in Mathematical Logic (P4A1 / P2A1)
Lecturer
- Prof. Dr. Peter Koepke
Time
- Tuesdays 14:15 - 16:00. Start: by appointment
Automated Proving
By the Gödel completeness theorem every mathematical proof can in principle be carried out in a formal proof calculus. The actual realization leads to high complexities that can only be handled with the help of computers. Formal mathematics practically implements calculi, in which simple proofs can be found automatically and in which mathematical theories can be formalized and checked for logical correctness.
The Naproche (Natural Proof Checking) group is developing the interactive theorem prover Naproche, which accepts proofs in a (controlled) natural language which is similar to the ordinary language of mathematics. Naproche texts can be and should be formulated so that they are immediately readable by mathematicians. Naproche can be run as part of the prover-platform Isabelle. A first impression is also available via the Naproche-Webinterface.
In the practical module we shall study the behaviour of the automated theorem prover Eprover that Naproche uses for complex proof tasks. We want to trace and improve Eprover's proof search for tasks generated by Naproche.
Prerequisites are mathematical logic up to the completeness theorem and a good general computer knowledge. Participants are supposed to have reasonably powerful laptops which can run the present version of Isalle/Naproche under Linux.
There is a limited number of practical slots. As of now you can apply by email to koepke@math.uni-bonn.de stating
- your name
- matriculation number
- email address
- subject
- study semester
- completed logic modules
- programming experience
- optional further information