Description

Computer systems are becoming more complex every day. This has led to the conception that we need automated reasoning techniques to efficiently and soundly reason about them. Here automated reasoning is understood in the broad sense of the use of computers to perform logical inference, potentially including user interaction.

As an example, we mention the use of automated reasoning techniques in formal specifications of computer systems, in particular the deepspec initiative an NSF funded "Expedition in Computing" that brings together several major research groups in the US. The aim of this project is to guarantee the correct behaviour of various parts of a computer system, like software-systems infrastructure such as operating systems, programming-language compilers or computer chips, according to their fully formalised specification. That is, it is formally proven that these parts works according to their specification. These proofs do rely on the use of interactive theorem provers, that is automated reasoning techniques.

In this seminar we will study one relatively easily accessible testbook, which emphasises the practical use of logic in this context:

John Harrison
Handbook of Practical Logic and Automated Reasoning
Cambridge University Press

We will look at 15 different (sub)-chapters of the book, spanning propositional logic, SAT solving, binary decision diagrams, first-order logic, resolution and tableau provers and decicable fragments. Each student will be given a specific chapter to present each week. Code and resources from the book can be found here.

Guidelines

The final grade will be based on the presentation and the written report. Active participation during the presentations will also be taken into account. In particular, attendance each week is mandatory.

Language and Typesetting

Theses must be written in LaTeX2e. In order to ensure a uniform layout, the Computational Logic LaTeX class must be used. Before producing the final version of the seminar report, make sure you use the latest version. Reports have to be written in English. The report must be between 10 and 15 pages long.