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.
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.
|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|
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.