# Seminar ‘Decision Procedures’, Summer Semester 2016

## Overview

 Title Seminar Decision Procedures Semester SS 2016 Module Master-Seminar (IN2107) Prerequisites Specialization in the area Formal Methods and its Applications, e. g. some of the following courses: IN2041: Automata and Formal Languages IN2048: Equational Logic IN2049: Logic IN2050: Model Checking IN2055: Semantics Enjoying Theoretical Computer Science, Mathematics, and seeing the beauty in their many applications ☺ SWS 2 ECTS 4 Organisation Fabian Immler, Manuel Eberl, Tobias Nipkow

Picture by Ilya Yodovsky Jr. (taken from Decision Procedures by D. Kroening and O. Strichman)

## Content

In 1928, David Hilbert and Wilhelm Ackermann posed the fundamental question commonly known as the Entscheidungsproblem (‘decision problem’): ‘Is there a finite procedure (= algorithm) that decides the validity of any given formula in first-order logic?’ Hilbert called it the ‘main problem of mathematical logic’ at that time. The question was answered negatively by Church and Turing (independently) only several years later. Thus the quest for the holy grail of logic – an automated procedure to decide the validity of any given first-order formula – was doomed to fail!

But not all hope is lost – there are many theories and fragments of first-order logic which

• are powerful enough to talk about interesting statements
• and at the same time admit an algorithm that decides the validity of these statements!
Many of these theories are of utmost importance for both mathematicians and computer scientists. Important applications include automatic theorem proving and automatic verification of hard- and software.

Examples of interesting Theories include:

• Propositional Logic & extensions (SAT solving, QBF)
• Real closed Fields (seminal result by Tarski)
• Linear Arithmetic (any boolean combination of linear inequalities, ⇒ more than just linear programming)
• Presburger Arithmetic (e. g. via automata, Cooper's algorithm, or Omega)
• Equality logic and uninterpreted functions (Congruence Closure)
• Arrays (compiler optimization, verification)
• Combinations of theories (nice theoretical results with direct practical applications)
In this seminar, we will study several of these theories (and others) and their decision problems – there will be beautiful results, algorithms and applications!

Primary book:

## Important Dates

### First Meeting

Date: 28.1.2016
Time: 14:30 – 15:30
Room: MI 00.09.038 (Turing)

### Homework

Please hand in your solution attempts to Fabian Immler until 31.8.2016

## First meeting

Overview of topics, information on organization, …  If you want to participate in the seminar but cannot attend the first meeting, please write an email to Fabian Immler

## Registration

Students are assigned to the course via the Matching platform.

## Grading

Grading will be based on:
• Preparation phase.
• Presentation.
• Creation of the exercise sheet.
• Active participation during the discussion.
• Seriously attempting to solve at least 80 % of the exercises.

## Presentation & Exercise Sheets

All participants are expected to give a decent lecture of 45 minutes. During and after every lecture there will be discussions.

Everyone is expected to prepare an exercise sheet with 3-4 exercises (of varying difficulty). Every participant should make a serious attempt at a solution for at least 80% of the exercises and hand in solution attempts to Fabian Immler.

Please prepare enjoyable slides! Use a clean layout and font and include appropriate figures. Feel free to use the blackboard or projector e. g. for highlighting important facts or developing examples. Before you start working on your presentation, please read the Guidelines for Creating Presentations from the LaTeX-beamer userguide. Please also prepare enjoyable exercise sheets – you can use the template provided.

## Supervision

We will provide some basic literature – additionally, we expect every participant to search for further literature! Every presentation will be supervised by one member of the chair who will always be happy to answer questions and provide guidance on how to give a good presentation.

## Assignment of Topics

TopicIDStudentAdvisor Literature Date and Time Room Material
Certification of (un)SAT proofs 1 Wolfgang Nicka Dr. Peter Lammich link Tue 28 June, 14:00–15:00 MI 00.11.038 (John v. Neumann) Slides Exercises Solutions
Equality Logic and Uninterpreted Functions 2 Michaela Tiessler Dr. Johannes Hölzl link Tue 28 June, 15:00–16:00 MI 00.11.038 (John v. Neumann) Slides Exercises Solutions
Linear Arithmetic 3 Matthias Kohler Prof. Tobias Nipkow link Tue 5 July, 14:00–15:00 MI 00.09.038 (Turing) Slides Exercises Solutions
Presburger Arithmetic 4 Fabio Madge Pimentel Julian Brunner link, link Tue 5 July, 15:00–16:00 MI 00.09.038 (Turing) Slides Exercises Solutions
Real Arithmetic 6 Max Haslbeck Manuel Eberl link Fri 8 July, 10:00–11:00 MI 00.11.038 (John v. Neumann) Slides Exercises Handout Solutions
Combination of Theories 5 Dennis Schmidt Fabian Immler link Fri 8 July, 11:00–12:00 MI 00.11.038 (John v. Neumann) Slides Exercises Solutions