Automated reasoning (2019/2020)

Course code
4S02796
Name of lecturer
Maria Paola Bonacina
Coordinator
Maria Paola Bonacina
Number of ECTS credits allocated
6
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Period
I semestre dal Oct 1, 2019 al Jan 31, 2020.

Lesson timetable

Go to lesson schedule

Learning outcomes

The class aims at providing knowledge about the following topics: a) methods for theorem proving and model building; b) inference systems based on orderings (resolution), instance generation, sub-goal reduction (tableaux); c) search plans; d) decision procedures for propositional satisfiability (SAT) and satisfiability modulo theories (SMT). At class' end the student will have to show her capacity to understand inference systems, search plans, and decision procedures, and evaluate them in terms of soundness, completeness and efficiencly, also via the implementation of a prototype. These skills will allow her to use existing resoners, develop new ones, and choose one appropriate for a problem or application. At class' end the student will be prepared to continue her studies or develop a master thesis in automated reasoning or artificial intelligence.

Syllabus

Foundations of automated reasoning: theorem proving and model building. The problem of propositional satisfiability (SAT): the DPLL and CDCL procedures. The problem of validity in first-order logic: inference systems and search plans. The Herbrand theorem. Instance-based inference systems: hyper-linking. Ordering-based inference systems: resolution and paramodulation/superposition. Subgoal-reduction based inference systems: model elimination, tableaux. Search plans: the given-clause algorithm; depth-first search with iterative deepening. Decision procedures for satisfiability modulo theories and assignments (SMT/SMA). Combination of theories. Implementation of a prover or solver as individual project.

Reference books
Author Title Publisher Year ISBN Note
Daniel Kroening, Ofer Strichman Decision Procedures. An algorithmic point of view Springer 2008 978-3-540-74104-6
John Harrison Handbook of Practical Logic and Automated Reasoning (Edizione 1) Cambridge University Press 2009 9780521899574
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509
Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821
Martin Davis The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. Taylor and Francis Group 2012 978-1-4665-0519-3

Assessment methods and criteria

First round: the grade is given by 25% PI + 25% PF + 50% P, where PI is the midterm exam, PF is the final exam, and P is a project.
Later rounds: the grade is given by 100% E, where E is a written exam, as hard as midterm, final, and project combined.
Attending all classes is crucial, however the exam rules are the same regardless of whether one attends or not.
All grades will be registered; it is possible to withdraw by informing the instructor.