Praktikum Mathematische Logik (P2A1, also P4A1)
Lecturer
- Prof. Dr. Peter Koepke
Times
- Tuesday 14:15 - 16:00, N 0.003. Start: Early November 2019
Contents
This practical module employs 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 a natural mathematical language
with LaTeX-style symbolic terms as its input language, and by allowing
natural structurings of proofs and documents.
Practical projects will aim at formalizations of parts of basic mathematical theories. We shall also study the Naproche-SAD software which is written
in the functional programming language Haskell. This will allow us to improve the system.
We assume that participants acquire a basic knowledge of Haskell by themselves.
Advanced concepts like 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 times.
Individual projects will be fixed in November/December. There will be
some longer meetings,
possibly whole days, for practical work and coordination
with dates to be arranged. For the logical foundations we shall assume the
material developed in parallel in the lecture course
Einführung in die Mathematische Logik.
I will be able to admit about 10 participants. Please send your applications
to koepke@math.uni-bonn.de until 25 October 2019, stating:
- Name
- Matriculation number
- Email address
- Course of studies (Bachelor/Master/...)
- Semester of studies
- Previous or current attendance of logic courses
- Programming experience; which languages?
- Further information if you wish