Bonn Mathematical Logic Group

Praktikum Mathematische Logik (P2A1), also P4A1


Lecturer

Time and place

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:

Admission to the course will be announced by email one week later.

Last changed: 20. Januar 2019