| TU München | Informatik | Software & Systems Engineering | Theorem Proving Group | Lehre |
The course will be an introduction to logic, the basic language of all sciences. You will learn about the precise syntax and meaning of the standard logical language, first-order logic. What is more, you will also learn about automatic procedures for deciding logical formulae: from surprisingly efficient decision procedures for propositional logic to semidecision procedures for full first-order logic. These algorithms will be presented as actual code in OCaml, both in the lectures and the exercises. An understanding of OCaml is essential to follow the course.
Syllabus:
Practical exercises in OCaml will complement the lectures and theory exercises. You will need some very basic knowledge of OCaml (for example from earlier lectures), or you should be prepared to learn this in the first weeks (here is some help).
We will make use of the code that comes with John Harrison's book. Download it here. Before using it, you need to build it using make. If you are running Windows and don't have the make tool, just download atp_interactive.ml (the result of the build process) and place it in the code directory.
The exercises will include three small projects where you will program small logic-related tools. You can gain a bonus of one level (0.3) on your final grade if you complete one of the projects and a second bonus of two levels (0.6) if you complete at least two of them.
For the exercise sessions, please bring your laptop if you have one, and make sure that you have OCaml running and the code downloaded.