Corso di studi offerto per:
Orario Lezioni
Date (Dates): Martedì 16.30 - 18.30, Venerdì 11:30 - 13:30 (Tuesday 16.30 - 18.30, Friday 11:30 - 13:30)
Luogo(Place): Strada Le grazie 15, Ca' Vignal 1, Aula C
Obiettivi
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. Obiettivo del corso è dare allo studente strumenti per progettare, applicare e valutare metodi e sistemi di ragionamento automatico, per applicazioni in campi quali verifica di HW e SW, intelligenza artificiale, robotica.
Educational Objectives
The class presents problems, methods and systems for automated reasoning. The class 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, focusing on applications such as HW and SW verification, artificial intelligence and robotics. Syllabus
Programma
Ragionamento automatico generale: strategie di dimostrazione di
teoremi. Sistemi di inferenza a scelta: generazione di istanze,
generazione di conseguenze (risoluzione, sovrapposizione, riscrittura),
riduzione di goal (eliminazione di modelli). Piani di ricerca.
Ragionamento algoritmico in ambiti specifici a scelta: ragionamento con
incertezza; ragionamento in sistemi multi-agente; procedure di
decisione per soddisfacibilità modulo teorie. Progetto e uso di
ragionatori generici o specifici.
Syllabus
Automated Reasoning: theorem-proving strategies. Inference Systems,
choosing among: instance-based, ordering-based (e.g., resolution,
superposition, rewriting), subgoal-reduction (e.g., model elimination).
Search Plans. Algorithmic Reasoning in specific domains, choosing
among: reasoning under uncertainty; reasoning in multi-agent systems;
reasoning procedures for satisfiability modulo theories. Design and use
of general-purpose or specific automated reasoners.
Modalità d'esame
Esame mediante prove parziali: vale solo per gli appelli subito dopo la
fine delle lezioni, ovvero per la sessione. L'esame consta di un
compito scritto (prova parziale) e di un progetto individuale da
realizzare a casa o in laboratorio.
Il voto d'esame è dato da: 50% prova parziale + 50% progetto.
Esame senza prove parziali: l'esame consta di un unico compito scritto
(compito d'esame), di difficoltà tale da uguagliare la prova parziale
ed il progetto, il cui voto determina da solo il voto d'esame. Questa
modalità vale per tutti gli appelli.
Note: la prova parziale si tiene nella stessa data, ora e luogo del
compito d'esame . (contenuto e durata della prova parziale e del
compito d'esame saranno diversi).
Exam Modalities
Partial tests mode: it applies only to the exam sessions right at the
end of the class. The exam consists of a written test (partial test)and
an individual project to be developed either at home or in the lab. The
final grade is given by 50% partial test + 50% project.
Single-test mode: the exam consists of a single written test (exam
test), whose difficulty is equivalent to that of the partial test and
the project, and whose grade determines alone the final grade. This
mode applies to all sessions.
Notes: the partial test is administered on the same date, time and
place as the exam test (contents and duration of the partial test and
of the exam test will be different).
Docente/Teacher: Alessandro Farinelli