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