Title  Seminar Decision Procedures 
Semester  SS 2016 
Module  MasterSeminar (IN2107) 
Prerequisites 
Specialization in the area Formal Methods and its Applications,
e. g. some of the following courses:

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)
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 firstorder 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 firstorder formula – was doomed to fail!
But not all hope is lost – there are many theories and fragments of firstorder logic which
Examples of interesting Theories include:
Date: 28.1.2016
Time: 14:30 – 15:30
Room: MI 00.09.038 (Turing)
Please hand in your solution attempts to
Fabian Immler until
31.8.2016
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
Students are assigned to the course via the Matching platform.
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 34 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 LaTeXbeamer userguide. Please also prepare enjoyable exercise sheets – you can use the template provided.
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.
Topic  ID  Student  Advisor  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 