Praktikum Mathematische Logik (P2A1 / P4A1)
Dozent
- Prof. Dr.
Peter Koepke
Zeit
- Dienstags 14:15 - 16:00. Beginn: nach Vereinbarung
Automatisches 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 mathematische Aussagen formalisiert werden können, einfache Beweise automatisch gefunden werden können und umfangreiche Theorien 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-SAD können und sollen 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 das Naproche-Webinterface.
Im Praktikum soll im Rahmen der Weiterentwng von Naproche das Verhalten des automatischen Beweisers Theorem Proving in a Russian Room and in Haskell von S. Panitz. Die anschließende Projekte betreffen z.B. Erweiterungen der natürlichen Beweissprache, Restrukturierungen der Beweis-Überprüfung oder die Anbindung externer Beweiser.
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.
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
- Thursdays 16:15 - 18:00. Start: by appointment
Formal Mathematics
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 mathematical theories can be completely formalized and checked for logical correctness.
The Naproche (Natural Proof Checking) group is developing the interactive theorem prover Naproche-SAD which accepts proofs in a (controlled) natural language which is similar to the ordinary language of mathematics. Naproche-SAD texts can be and should be formulated so that they are immediately readable by mathematicians.
In the practical module we shall work on programming projects for the further development of Naproche-SAD. The system is written in the functional programming language Haskell. An introduction to Haskell and automatic proving is given in the module, e.g., using the text Theorem Proving in a Russian Room and in Haskell by S. Panitz. The programming assignments deal with extensions of the natural proof language, restructuring of proof checking or interfacing with external automatic provers.
Participants are supposed to have reasonably powerful laptops which can run the present version of Naproche-SAD. Naproche-SAD can also be started from the command line.
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