Contact
Teaching
 |
 |
|
| Algorithms for the Undecided SS2015 | ||
 |
 |
| News | Content | Grading | Time schedule | Material |
Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
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!
Examples of interesting Theories include:
- Propositional Logic + extensions (SAT-solving, QBF)
- Existential Real Arithmetic
- Presburger Arithmetic (via a technique using automata)
- Combinations of theories (nice theoretical results with direct practical applications)
We will also offer some problems related to verification that are most naturally expressed outside the language of first-order logic. For example
- Finding the winner of a so-called 'Parity Game' (a problem to which a number of extremely powerful temporal logics can be reduced)
- Deciding a fragment of Separation Logic (a formalism designed for specifying properties of the heap)
Picture by Ilya Yodovsky Jr. (taken from "Decision Procedures" by D. Kroening and O. Strichman)
Requirements
- Discrete Structures
- Logic
- Introduction to Theoretical Computer Science
- Enjoying Theoretical Computer Science, Algebra, and seeing the beauty in their many applications :)