Praktikum Mathematische Logik (P2A1 / P4A1)
Dozent
- Prof. Dr.
Peter Koepke
Zeit
- nach Vereinbarung
Programming Naproche in Haskell
In der Bonner Logikgruppe wird der interaktive Beweisprüfer Naproche (für: Natural Proof Checking) entwickelt, 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 ist Teil der Beweiser-Plattform Isabelle und kann nach Installation von Isabelle sofort benutzt werden. Einen ersten Eindruck bietet auch das Naproche-Webinterface.
Im Praktikum soll - nach einer kurzen Einführung in Naproche - das Verhalten und die Leistungsfähigkeit von Naproche durch Änderungen am Programm verbessert werden. Das betrifft die Erweiterung der Eingabesprache, die Verwaltung von Notationen und Annahmen im Verlauf von mathematischen Texten, die effiziente Ankoppelung des automatischen Beweisers Eprover usw. Ein weiteres mögliches Teilprojekt wäre die Übersetzung von freier mathematischer Sprache in die Eingabesprache von Naproche mit Hilfe von ChatGPT.
Voraussetzungen sind ein gutes Verständnis mathematischen Beweisens und eine sehr gute allgemeine Computerbeherrschung, praktische Programmiererfahrungen und LaTeX. Naproche benutzt die funktionale Programmiersprache Haskell, in die wir uns einarbeiten werden. 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 kleine Anzahl von Plätzen zur Verfügung, die individuell vergeben werden. Sie können sich jederzeit 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
- by appointment
Programming Naproche in Haskell
At Bonn we are developing the interactive theorem prover Naproche (Natural Proof Checking), 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 is part of the prover-platform Isabelle and it can be used right after installation of Isabelle. A first impression is also available via the Naproche-Webinterface.
After a brief introduction to Naproche we shall improve the behaviour and efficiency of the Naproche program. This concerns extensions of the input language, managing notations and assumptions in mathematical texts, efficiently interfacing with the automatic theorem prover Eprover, etc. Another possible project could be the translation of free mathematical language into the input language of Naproche using ChatGPT.
Prerequisites are a good understanding of mathematical proving and very good general mastering of computers, practical programming experience, and LaTeX.Naproche employs the functional programming language Haskell, which will be introduced in the course. Participants are supposed to have reasonably powerful laptops which can run the present version of Isalle/Naproche under Linux.
There is a small number of practical slots which will be allocated individually. Please 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