Decision Procedures
Lecturers
Schedule
Preparatory Meeting: Tuesday, April 14, 2015: 10 - 12h, room 630 (Building E1 5)
Talks: Friday, June 19, 2015: 08:30 h, room 630 (Building E1 5)
Sample Topics
Congruence Closure, CDCL, Quantifier Elimination, Fourier-Motzkin, Simplex, Virtual Subsitution, SMT, Superposition, IC3
There are currently more applications than slots. Therefore, please have a look at the following paper which is one of the slots and which is a representative paper. The task is to turn it into to a talk that Presburger for the existential fragment is decidable and NP-complete. We expect you to be able to extract and understand the necessary information from the paper on your own. Please only register if you feel comfortable with such a task. If you already registered and don't feel comfortable with such a task, please ask Jennifer Müller (jmueller@mpi-inf.mpg.de) to remove you from the list.
Representative Paper: ScarpelliniComplexityPresburger84.pdf