Practical Project in Mathematical Logic - Foundations and Implementations of Automated and Interactive Theorem Proving (P4A1), and Praktikum Mathematische Logik P2A1

Lecturer

• Prof. Dr. Peter Koepke

Times

• Mondays and Wednesdays 14:15-16:00, Endenicher Allee 60 - PC-Pool, N 0.004/5
  Exercise classes: Tuesdays 12:15-14:00 or 16:15-18:00, Endenicher Allee 60 - PC-Pool, N 0.004/5
  Begin: 11 April

Contents

The Gödel completeness theorem shows that a formula holds in all models of an axiom system if and only if there is a formal proof of the formula from the axioms. The completeness theorem thus reduces the highly infinite problem of checking all structures to the search for a finitary object which obeys some simple syntactical rules. Automated theorem provers (ATP) are built around practical implementations of this proof search and are able to verify simple lemmas automatically. ATPs are the basis for interactive theorem proving (ITP) of sophisticated mathematical theorems: a human user supplies a "formalization" of the proof in the form of a series of intermediate proof steps which are successively proved by the ATP.

The Practical Project in Mathematical Logic is intended to augment the common view of mathematical logic as a theoretical subject with a practical side which has the future potential of wide applicability within mathematics. The lecture part of the course roughly corresponds to Sections I and II of my logic scriptum. We shall, however, quickly summarize Section I and then vastly expand Section II by detailed working implementations in the programming language Haskell. Participants should already be acquainted with some theoretical logic and/or self-study Section I before the summer term.

We shall use code from the interactive theorem prover Naproche which is being developed in the Bonn logic group. Naproche is distinguished from other ITPs by accepting and checking formalizations which are formulated in (a subset of) the usual language of mathematics; Naproche is available and usable as part of the Isabelle prover environment. After the introduction to automated and interactive theorem proving, students will work on individual projects which may be formalizations in Naproche or other ITPs or programming work in the Naproche context.

The course consists of

4 hours (4 SWS) per week of lectures, tutorials, or plenary exercises, probably Monday 14-16 und Wednesday 14-16;

2 hours (2 SWS) per week of problem sessions, times to be announced.

Until about mid-June there will be weekly homework exercises consisting of theoretical, programming, or formalization tasks. Successful participation in exercises and homework problems is a prerequisite for individual projects which will be assigned in June. The format of the course may change once students begin working on their project. Completed projects with a written project report will have to be submitted in August and presented at a plenary meeting.

Students are expected to bring and use their own laptop capable of running Haskell and the Isabelle prover environment (see minimum requirements), preferably under Linux. Visual Studio Code is recommended for development of code.

To facilitate our planning please state your interest in this module in a short informal email to koepke@math.uni-bonn.de. Alternatively you can simply turn up for the first lecture on 11 April.