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 geht es um die Pflege und Weiterentwicklung des Codes von Naproche.
Voraussetzungen sind ein gutes Verständnis mathematischen Beweisens, sehr gute allgemeine Computerbeherrschung, praktische Programmiererfahrungen und wenn möglich Erfahrungen mit der funktionalen Programmiersprache Haskell.
Es stehen maximal 3 Plätze 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.
The practical project will be concerned with maintaining and developing the code of Naproche.
Prerequisites are a good understanding of mathematical proving, very good general mastering of computers, practical programming experience, and - if possible - experience with the functional programming language Haskell.
There are maximally 3 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