Praktikum Mathematische Logik (P2A1), also P4A1
Lecturer
- Prof. Dr. Peter Koepke
Time and place
- Lecture: Thursday 16:15 - 18:00, N 0.008. Start: 04. April.
Contents
This practical module uses the proof assistant Naproche-SAD
which is currently being developed at Bonn (https://github.com/Naproche/Naproche-SAD).
Naproche-SAD is based on first-order logic and set theory. It is
distinguished by accepting natural mathematical language
with LaTeX-style symbolic terms as its input language, and by allowing
natural structurings of proofs and documents.
The module aims at completing a formalization of the Set Theory scriptum 2018/19
in Naproche-SAD. We shall also study the Naproche-SAD software which is written
in the functional programming language Haskell. This will allow us to make small
extensions to the system.
We assume that participants acquire a basic knowledge of Haskell by themselves.
Advanced concepts like inductive data types, monads, or proving algorithms
will be presented in seminar-style presentations by participants. Participants should
have a reasonably powerful laptop, ideally to be able to run the current version
of the Isabelle proof assistant (https://isabelle.in.tum.de/) since we shall
use the Isabelle infrastructure to run Naproche-SAD. It is also possible to
run Naproche-SAD in a terminal, with more modest hardware requirements.
The practical course will meet weekly at the above time and location.
Individual projects will be fixed in May. There will be some longer meetings,
possibly whole days, for practical work and coordination, possibly also
in July or the first half of August, with dates to be arranged.
It will be advantageous to attend my 2 SWS course
Type Theory and the Formalization of Mathematics that
I shall offer on Thursdays 2-4.
I will be able to admit about 6 participants. Please send your applications
to koepke@math.uni-bonn.de until 1 March 2019, stating:
- Name
- Matriculation number
- Email address
- Course of studies (Bachelor/Master/...)
- Semester of studies
- Attendance of Einführung in die Mathematische Logik and/or Set Theory and/or the Type Theory course in SS 19?
- Programming experience; which languages?
- Further information if you wish