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

A.A. 2024/2025 A.A. 2023/2024 A.A. 2022/2023 A.A. 2021/2022 A.A. 2020/2021 A.A. 2019/2020 A.A. 2018/2019 A.A. 2017/2018 A.A. 2016/2017 A.A. 2015/2016 A.A. 2014/2015 A.A. 2013/2014 A.A. 2012/2013 A.A. 2011/2012 A.A. 2010/2011 A.A. 2009/2010

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/2026

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

CURRICULUM TIPO:

1° Anno 

InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
C
INF/01

2° Anno   Attivato nell'A.A. 2020/2021

InsegnamentiCreditiTAFSSD
6
B
ING-INF/05
6
B
INF/01
Altre attività formative
4
F
-
Prova finale
24
E
-
InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
C
INF/01
Attivato nell'A.A. 2020/2021
InsegnamentiCreditiTAFSSD
6
B
ING-INF/05
6
B
INF/01
Altre attività formative
4
F
-
Prova finale
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
Due insegnamenti a scelta
6
C
INF/01
6
C
INF/01
6
C
FIS/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
SECS-P/10
6
C
INF/01
6
C
INF/01
6
C
INF/01
Tra gli anni: 1°- 2°
8
D
-

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.

A Attività di base
B Attività caratterizzanti
C Attività formative affini o integrative
D Attività a scelta dello studente
E Prova finale
F Altre attività formative
S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Ragionamento automatico  (2019/2020)

Codice insegnamento

4S02796

Docente

Maria Paola Bonacina

Coordinatore

Maria Paola Bonacina

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

I semestre dal 1 ott 2019 al 31 gen 2020.

Orario Lezioni MoodleMoodle Seminari 0

Obiettivi formativi

Il corso si propone di fornire le seguenti conoscenze: a) metodi per la dimostrazione di teoremi e costruzione di modelli; b) sistemi di inferenza basati su ordinamenti (risoluzione), per generazione di istanze, basati su riduzione di sotto-goal (tableaux); c) piani di ricerca; d) procedure di decisione per la soddisfacibilità proposizionale (SAT) e modulo teorie (SMT). Al termine del corso la studentessa dovrà dimostrare di saper comprendere sistemi di inferenza, piani di ricerca, procedure di decisione, valutarne proprietà di correttezza, completezza ed efficienza, anche tramite implementazione di un prototipo. Queste conoscenze le consentiranno di usare ragionatori esistenti, svilupparne di nuovi, e sceglierne uno appropriato per un problema o applicazione. Alla fine del corso la studentessa sarà in grado di proseguire gli studi o sviluppare una tesi magistrale nell’ambito del ragionamento automatico e dell’intelligenza artificiale.

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 ed assegnamenti (SMT/SMA). Combinazione di teorie. Implementazione di un dimostratore o risolutore come progetto individuale.

Testi di riferimento
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
John Harrison Handbook of Practical Logic and Automated Reasoning (Edizione 1) Cambridge University Press 2009 9780521899574
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% PI + 25% PF + 50% P, dove PI è la Prova Intermedia, PF è 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.
Non è previsto il "rifiuto" del voto e tutti i voti saranno registrati. E' possibile ritirarsi informando la docente.

Le/gli studentesse/studenti con disabilità o disturbi specifici di apprendimento (DSA), che intendano richiedere l'adattamento della prova d'esame, devono seguire le indicazioni riportate QUI