Seminar on Automated Reasoning
Schedule: Fridays from 10:15am in INF 213, see official page
First course: Friday, September 24, at 10:15.
Related course: Synthesis, Analysis, and Verification
- Background: decision problems, constraint solving, synthesis, overview of applications
- Algorithms for constraints on numerical domains, sets, multisets, algebraic data types
- Local theory extensions
- Combination problem for decision procedures
- Superposition-based reasoning for first-order logic with equality
- Understand theoretical foundations and recent results behind in automated reasoning tools such as theorem provers, decision procedures, constraints solvers, and synthesis procedures.
- The course will include lectures, exercises, and presentations by students.
- Lecture 01, 24 Sept: Propositional Logic, DPLL
- Lecture 02- 04, 01,08,15, 22 Oct: First-Order Logic, Resolution, Model Construction
- Lecture 05, 22 Oct: Reasoning Modulo Theories, Abstract Congruence Closure
- Lecture 06, 29 Oct (by Andrej Spielmann): Alternation, Space, Complexity, and QFPAbit
- Lecture 07, 5 November (Swen Jacobs, Ruzica Piskac, Viktor Kuncak)
- Lecture 08, 12 November (Giuliano Losa, Swen Jacobs, Viktor Kuncak, all with native-language introductions by Ruzica Piskac)
- Lecture 09, 19 November (Hossein Hojjat, Alen Stojanov, Andrei Giurgiu)
- Lecture 10, 26 November (Eva Darulova, Hossein Hojjat)
- Lecture 11, 03 December (Ali Sinan Köksal, Victor Bushkov)
- First-Order Logic, syntax and semantics - due 08.10.2010.
- Herbrand Interpretation, Orderings, Model Construction - due 15.10.2010.
- Most General Unifier, Non-ground resolution - due 27.10.2010.
- Homeworks on QFPAbit - due 4.11.2010
- Homework on Second-Order Logic - due 8.12.2010
- 10/12/2010 - Etienne and Robin