Ragionamento automatico/Automated Reasoning

Insegnamento del corso di Laurea Magistrale in "Ingegneria e Scienze Informatiche" e del Dottorato in "Informatica".
Graduate course for the MS program in Computer Science and Engineering and the PhD program in Computer Science.

Docente/Instructor: Maria Paola Bonacina Ricevimento: mercoledì, 12:00 - 13:30, Stanza 1.73
Office hours: Wednesday, 12:00 - 13:30, Room 1.73

Obbiettivi/Objectives: Il corso introduce problemi, metodi e sistemi del ragionamento automatico. La presentazione combina fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, con enfasi sulla meccanizzazione. Obbiettivo del corso è dare allo studente strumenti per progettare, applicare e valutare metodi e sistemi di ragionamento automatico, per applicazioni in campi quali analisi, verifica, sintesi di sistemi, intelligenza artificiale, matematica, robotica.
The class presents problems, methods and systems in automated reasoning. The treatment combines theoretical foundations with algorithmic and practical issues, emphasizing mechanization throughout. The student learns how to design, apply, and evaluate methods and systems for automated reasoning, with attention to applications in fields such as analysis, verification, synthesis of systems, artificial intelligence, mathematics, robotics.

Programma/Programme: Fondamenti del ragionamento automatico: dimostrazione di teoremi e costruzione di modelli. Sistemi di inferenza, e.g.: per generazione di istanze (e.g., hyper-linking), basati su ordinamenti (e.g., risoluzione), basati su riduzione di sotto-goal (e.g., eliminazione di modelli). Piani di ricerca. Ragionamento algoritmico in ambiti specifici, e.g.: procedure di decisione per soddisfacibilità (SAT) e soddisfacibilità modulo teorie (SMT); ragionamento su vincoli. Progetto e uso di ragionatori generici o specifici.
Foundations of automated reasoning: theorem proving and model building. Inference systems, e.g.: instance-based (e.g., hyper-linking), ordering-based (e.g., resolution), subgoal-reduction based (e.g., model elimination). Search plans. Algorithmic reasoning in specific fields, e.g.: decision procedures for satisfiability (SAT) and satisfiability modulo theories (SMT); reasoning about constraints. Design and use of general-purpose or special-purpose reasoners.

Registro/Journal

Libri (in ordine alfabetico)/Books (in alphabetical order):

Articoli/Papers:

Esami (I appello)/Exams (First take):
Il voto è dato da 25% C1 + 25% C2 + 50% P, dove C1 è la prova intermedia (29 novembre 2017), C2 è la prova finale (il giorno del I appello nella sessione di febbraio 2018), e P è un progetto.
The grade is given by 25% C1 + 25% C2 + 50% P, where C1 is the midterm exam (29th November 2017), C2 is the final exam, and P is a project.

Prove intermedie: AA2011-12, AA2012-13, AA2013-14, AA2014-15, AA2016-17;
e loro soluzioni: AA2011-12, AA2012-13, AA2013-14, AA2014-15, AA2016-17.

Progetto/Project

Esami (appelli successivi)/Exams (Later takes):
Il voto è dato da 100% E, dove E è un unico compito scritto, di difficoltà tale da uguagliare l'unione delle prove parziali.
The grade is given by 100% E, where E is a written exam, as hard as midterm, final, and project combined.

Registrazione/Registration: non è previsto il rifiuto del voto e tutti i voti saranno registrati. Ci si può ritirare informando la docente. Tutti gli elaborati sono individuali. È vietato copiare o condividere codice o testo e le copiature determineranno abbassamenti di voti.
All grades will be registered. It is possible to withdraw by informing the instructor. All tests and projects are individual work. Cheating is strictly forbidden and will determine penalties on grades.



Maria Paola Bonacina