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).
| 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 |
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.
© 2024 | Verona University
******** CSS e script comuni siti DOL - frase 9957 ********p>
