Algorithms for the (decidedly) Undecided WS2013/2014

News | Content | Grading | Time schedule | Material

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)
• Arrays (compiler optimization, verification)
• Strings (software-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!

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

Requirements

• Discrete Structures
• Introduction to Theoretical Computer Science
• Enjoying Theoretical Computer Science, Mathematics, and seeing the beauty in their many applications :)