Automated Deduction (2008/2009)

Course partially running

Course code
Name of lecturer
Maria Paola Bonacina
Number of ECTS credits allocated
Other available courses
Academic sector
Language of instruction
2° Q dal Jan 26, 2009 al Mar 27, 2009.
Web page

Lesson timetable

2° Q
Day Time Type Place Note
Tuesday 12:30 PM - 1:30 PM lesson Lecture Hall D  
Wednesday 2:30 PM - 4:30 PM lesson Lecture Hall F from Feb 11, 2009  to Mar 27, 2009
Friday 11:30 AM - 1:30 PM lesson Lecture Hall D  

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.


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.

Reference books
Author Title Publisher Year ISBN Note
Ricardo Caferra, Alexander Leitsch, Nicolas Peltier Automated Model Building (Edizione 1) Kluwer Academic Publishers 2004 1-4020-265 Testo supplementare
Rolf Socher-Ambrosius, Patricia Johann Deduction Systems (Edizione 1) Springer Verlag 1997 0387948473 Testo adottato
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509 Testo adottato
Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741 Testo adottato
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821 Testo supplementare

Assessment methods and criteria

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.

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

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.