Automated Deduction (2006/2007)

Course partially running

Course code
Name of lecturer
Maria Paola Bonacina
Number of ECTS credits allocated
Other available courses
Academic sector
Language of instruction
2nd quadrimester dal Jan 8, 2007 al Mar 9, 2007.
Web page

Lesson timetable

2nd quadrimester
Day Time Type Place Note
Tuesday 10:30 AM - 11:30 AM lesson Lecture Hall I from Feb 7, 2007  to Mar 5, 2007
Wednesday 10:30 AM - 12:30 PM lesson Lecture Hall C  
Thursday 11:30 AM - 1:30 PM lesson Lecture Hall C  

Learning outcomes

The class assumes undergraduate-level knowledge of logic and algorithms. It presents the central problems in automated reasoning and a selection of the most important theoretical methods and state-of-the-art systems to approach them. The student learns how to design, apply and evaluate methods and systems for automated reasoning.


Inference system + search plan = proof procedure; the Herbrand theorem; instance-based strategies from Gilmore's method to the combination of hyperlinking with the Davis-Putnam-Logemann-Loveland algorithm for SAT; ordering-based strategies: expansion inferences (resolution, paramodulation, superposition), contraction inferences (subsumption, simplification by rewriting) and search plans for forward reasoning; subgoal-reduction strategies: linear resolution, tableaux, model elimination and search plans for backward reasoning; design and use of theorem provers; decision procedures; model building (hints); applications of automated reasoning to verification (hints).

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 Altro testo di riferimento
Rolf Socher-Ambrosius, Patricia Johann Deduction Systems (Edizione 1) Springer Verlag 1997 0387948473 Testo adottato
Klaus Truemper Design of Logic-based Intelligent Systems (Edizione 1) John Wiley and Sons 2004 0471484032 Altro testo di riferimento
Raymond M. Smullyan First-order logic Dover Publications 1995 0486683702 Altro testo di riferimento
Allan Ramsay Formal Methods in Artificial Intelligence (Edizione 1) Cambridge University Press 1989 0521424216 Altro testo di riferimento
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509 Testo adottato
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821 Altro testo di riferimento

Assessment methods and criteria

First mode:
this mode applies only to the exam right at the end of the class, that is for the exam session of March-April 2007, since the class is scheduled in the II term. In this mode, the exam consists of a written 2h test (C) and an individual programming project (P) to be developed either at home or in the lab during the course. The project comprises writing a short project report (max 4 pages). The final grade is given by 50% C + 50% P. After the first exam session since the end of classes, P and C are no longer valid. Those who choose to take the exam in this mode are supposed to register for the exam session of March-April 2007.
Second mode:
in this mode, the exam consists of a single written test, whose difficulty is equivalent to that of C + P, and whose grade determines alone the final grade. This mode applies to all exam sessions. However, if a student takes test E, the grade given by 50% C + 50% P is lost.