Studiare
In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.
Piano Didattico
Queste informazioni sono destinate esclusivamente agli studenti e alle studentesse già iscritti a questo corso.Se sei un nuovo studente interessato all'immatricolazione, trovi le informazioni sul percorso di studi alla pagina del corso:
Laurea magistrale in Ingegneria e scienze informatiche - Immatricolazione dal 2025/2026Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.
1° Anno
Insegnamenti | Crediti | TAF | SSD |
---|
2° Anno Attivato nell'A.A. 2018/2019
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Due insegnamenti a scelta
Legenda | Tipo Attività Formativa (TAF)
TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.
Ragionamento automatico (2017/2018)
Codice insegnamento
4S02796
Docente
Coordinatore
Crediti
6
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
INF/01 - INFORMATICA
Periodo
I sem. dal 2 ott 2017 al 31 gen 2018.
Obiettivi formativi
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.
Programma
Fondamenti del ragionamento automatico: dimostrazione di teoremi e costruzione di modelli. Il problema della soddisfacibilità proposizionale (SAT): le procedure DPLL e CDCL. Il problema della validità in logica del primo ordine: sistemi di inferenza e piani di ricerca. Il teorema di Herbrand. Sistemi di inferenza per generazione di istanze: iper-nessi. Sistemi di inferenza basati su ordinamenti: risoluzione e paramodulazione/sovrapposizione. Sistemi di inferenza basati su riduzione di sotto-goal: eliminazione di modelli, tableaux. Piani di ricerca: algoritmo della clausola data; ricerca per profondità con approfondimento iterativo. Procedure di decisione per soddisfacibilità modulo teorie (SMT). Ragionamento su vincoli. Progetto e uso di ragionatori generici o specifici.
Autore | Titolo | Casa editrice | Anno | ISBN | Note |
---|---|---|---|---|---|
Daniel Kroening, Ofer Strichman | Decision Procedures. An algorithmic point of view | Springer | 2008 | 978-3-540-74104-6 | |
Rolf Socher-Ambrosius, Patricia Johann | Deduction Systems (Edizione 1) | Springer Verlag | 1997 | 0387948473 | |
Raymond M. Smullyan | First-order logic | Dover Publications | 1995 | 0486683702 | |
Chin-Liang Chang, Richard Char-Tung Lee | Symbolic Logic and Mechanical Theorem Proving (Edizione 1) | Academic Press | 1973 | 0121703509 | |
Aaron R. Bradley, Zohar Manna | The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) | Springer | 2007 | 9783540741 | |
Alexander Leitsch | The Resolution Calculus (Edizione 1) | Springer | 1997 | 3540618821 | |
Martin Davis | The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. | Taylor and Francis Group | 2012 | 978-1-4665-0519-3 |
Modalità d'esame
I appello (mediante prove parziali) : il voto è dato da 25% C1 + 25% C2 + 50% P, dove C1 è la prova intermedia, C2 è la prova finale, e P è un progetto.
Appelli successivi: il voto è dato da 100% E, dove E è un unico compito scritto, di difficoltà tale da uguagliare l'unione delle prove parziali.
Frequentare il corso è fondamentale, tuttavia le modalità d'esame sono le stesse per chi frequenta e chi non frequenta.