Learning outcomes

The class, taught in English, presents the main problems of and methods and systems for automated reasoning. The treatment combines theoretical foundations with algorithmic and practical issues, stressing mechanization throughout. The student learns how to design, apply and evaluate methods and systems for automated reasoning, with emphasis on the applications to the verification of SW or HW, either automated or semi-automated. Pre-requisites: undergraduate-level knowledge of logic and algorithms.

Program

Automated reasoning: proof procedures as semi-decision procedures for validity or theorem-proving strategies. Inference system + search plan = theorem-proving strategy. The Herbrand theorem. Ordering-based strategies. Expansion inference rules: resolution, paramodulation, superposition. Contraction inference rules: subsumption, simplification by rewriting. Search plans. Algorithmic reasoning: proof procedures as decision procedures for satisfiability. First-order theories and decidable problems in first-order theories. Decision procedures and their combination. When theorem-proving strategies are decision procedures. Design and use of automated reasoners.

Examination Methods

Partial tests mode:
it applies only to the exam right at the end of the class, that is for the exam session of March-April, since the class is offered in the Winter. The exam consists of a written test (C) and an individual project (P) to be developed either at home or in the lab during the term. The final grade is given by 50% C + 50% P. After the first exam session since the end of the class, P and C are no longer valid.

Single-test mode:
the exam consists of a single written test E, whose difficulty is equivalent to that of C + P, and whose grade determines alone the final grade. This mode applies to all sessions.

Notes:
the partial test C is administered on the same date, time and place as test E of the March-April session (of course contents and duration of C and E will be different).

Registration:
for each session the date of the exam is given by the date of the written test E and it is sufficient to register for that date. All grades will be registered. Students dissatisfied with their performance may withdraw by not handing-in either C or E.