Schedule: Fridays from 10:15am in INF 213, see official page

First course: Friday, September 24, at 10:15.

Credits: 4

Teaching Staff:

• Swen Jacobs
• Viktor Kuncak
• Ruzica Piskac

Related course: Synthesis, Analysis, and Verification

Topics:

• 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

Objectives:

• Understand theoretical foundations and recent results behind in automated reasoning tools such as theorem provers, decision procedures, constraints solvers, and synthesis procedures.

Format:

• The course will include lectures, exercises, and presentations by students.

Slides:

• 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)

Homeworks:

• Propositional Logic
• 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
• Homeworks on Parikh's Theorem - due 22.11.2010. (Solution to problem 4)
• Homework on Second-Order Logic - due 8.12.2010

Student Presentation:

• 10/12/2010 - Etienne and Robin