Conoscenza e capacità di comprensione. Acquisire la conoscenza dei concetti di calcolabilità, di computabilità e le nozioni elementari dei formalismi della logica proposizionale e dei predicati. Conoscenza e capacità di comprensione applicate. Acquisire la capacità di definire in modo formale i problemi utilizzando il formalismo degli automi o il linguaggio della logica e in particolare di specificare formalmente un problema o il comportamento di un sistema in uno dei modelli computazionali studiati. Autonomia di giudizio. Comprendere i limiti intrinseci della computabilità o la complessità connaturata ai problemi per ragionare sulle limitazioni nella progettazione di soluzioni algoritmiche efficaci ed efficienti. Abilità comunicativa. Capacità di definire e comunicare in modo rigoroso e formale concetti e problemi. Capacità di apprendere. Capacità di leggere in autonomia la letteratura che propone metodi formali per l’intelligenza artificiale (con particolare riferimento agli approcci simbolici dell'intelligenza artificiale e della rappresentazione della conoscenza) e l’informatica in generale.

Le nozioni elementari dell'insiemistica. Consuetudine con la notazione formale della matematica

Il corso consiste di tre parti principali ciascuna quantificabile in tre CFU: - Computabilità. Si esamineranno i principali modelli di computazione ragionando sulla loro espressività. In particolare, in ordine crescente di espressività si introdurranno prima gli automi regolari, poi gli automi a pila e le grammatiche libere dal contesto. Per definire la nozione di calcolabilità si studierà infine la macchina di Turing e la nozione di decidibilità. Si studieranno le relazioni di espressività tra i modelli di computazione, le loro proprietà rispetto alle operazioni di composizione e si dimostrerà che esistono problemi per cui non esistono soluzioni algoritmiche (non decidibili). - Complessità. Si illustreranno le nozioni di base della complessità spaziale e temporale. In particolare, si studieranno le più conosciute classi di complessità: P, NP, NP-Complete, coNP, EXP e PSPACE. Per ciascuna classe si studieranno dei problemi rappresentativi appartenenti alla classe. Si darà particolare attenzione alla classe NP-complete introducendo la nozione di problema completo e si esemplificherà la tecnica di riduzione tra problemi (utile per determinare la complessità di un problema) in alcuni casi significativi (e.g. SAT, 3SAT, Cammino Hamiltoniano, k-Clique, etc). - Logica. Si introdurranno sintassi e semantica della logica proposizionale e della logica dei predicati (al primo ordine). Si studieranno i problemi di soddisfacibilità per entrambe le logiche. Si introdurranno le tecniche di tableaux, risoluzione e di refutazione introducendo gli algoritmi più noti per SAT nel caso della logica proposizionale. Si studieranno forme normali per la logica dei predicati (forma prenessa, forma di clausola) e il teorema di Goedel per la refutazione per formule della logica dei predicati in forma di clausola. Si introdurrà la programmazione logica e il linguaggio Prolog. Si farà una breve introduzione all'ambiente di specifica Z3

Per la parte di calcolabilità e complessità: [1] Michael Sipser, Introduzione alla teoria della computazione, Apogeo. Per la parte di Logica: [2] Mordechai Ben-Ari: Mathematical Logic for Computer Science (3rd ed.), Springer, 2013. (per un testo in italiano si veda anche) [3] Daniele Mundici, Logica-Metodo breve, Springer, 2011.

- Nozioni introduttive: Alfabeti, parole e linguaggi - Gli automi regolari - Automi deterministici e non deterministici: sintassi e semantica. - Determinizzazione di automi regolari - Linguaggi regolari e loro chiusura per unione, intersezione, complemento, concatenazione e *. - Espresioni regolari: sintassi e semantica - Equiespressività di automi regolari ed espressioni regolari - Pumping lemma per linguaggi regolari - Uso del Pumping lemma per provare la non regolarità di linguaggi - Gli automi a pila (non deterministici): sintassi e semantica - Linguaggi liberi dal contesto - Grammatiche libere dal contesto per la generazione di linguaggi liberi dal contesto - Pumping lemma per i linguaggi liberi dal contesto - Non chiusura per intersezione e complemento degli automi a pila - Macchine di Turing (MdT) deterministiche e non deterministiche: sintassi e semantica. - Linguaggi riconosciuti e decisi da MdT - Equivalenza delle Mdt multinastro - Determinazzione della MdT - Caratterizzazione dei linguaggi decidibili - Numerabilità delle macchine di Turing e non numerabilità dei linguaggi - Esempi di linguaggi non decidibili. - Complessità spaziale e temporale per linguaggi - Classe P e problemi decidibili in tempo polinomiale da MdT deterministiche - Classe NP e problemi decidibili in tempo polinomiale da MdT non deterministiche - Classe NP-complete: Problemi completi e il concetto di riduzione - Teorema di Cook-Levin (NP-completezza di SAT) - Altri problemi NP-completi: 3SAT, k-Clique, Cammino Hamiltoniano. - La classe coNP ed esempi di problemi coNP-completi - Classi di complessità spaziale: PSPACE e NPSPACE - Teorema di Savitch (PSPACE = NPSPACE) - Problemi PSPACE-completi: la logica booleana quantificata. - Logica - Calcolo proposizionale: sintassi e semantica. - Implicazione logica, equivalenza, tautologie, soddisfacibilità. - Metodo del tableaux. - Forma normale congiuntiva e disgiuntiva. - Algoritmo di Davis-Putnam - Correttezza e completezza dell'algoritmo di Davis-Putnam. - Altri algoritmi di SAT solving. - Refutazione - Clausole di Krom e clausole di Horn - Calcolo dei predicati: sintassi e semantica - Soddisfacibilità - Il metodo dei Tableaux. - Forma normale prenessa - Skolemizzazione - Riduzione in forma di clausola - Universo di herbrand - Teorema di Goedel per la refutazione - Algoritmo di unificazione - Programmazione logica e risoluzione SDL - Introduzione a Prolog - Risoluzione SAT in Z3.

Lezioni frontali ed esercitazioni in classe. Assegnazione di esercizi da svolgere autonomamente e loro correzione in classe.

I materiali del corso (Slides, esercizi, testi degli esami precedenti) sono recuperabili nella cartella condivisa del canale TEAM del corso.

La verifica prevede una prova scritta e una successiva prova orale. La prova scritta consiste nello svolgimento di esercizi sulla parte di Calcolabilità e quella di Logica e di domande di carattere generale sulla parte di complessità. La prova scritta è composta 6 esercizi a risposta libera. A ciascun esercizio è assegnato un punteggio e la somma complessiva dei punti assegnati agli esercizi è 32. Il punteggio massimo per un esercizio è assegnato allo svolgimento corretto dell'esercizio. In presenza di errori il punteggio massimo viene ridotto in ragione della loro gravità. Il voto dello scritto è pari alla somma dei voti conseguiti nei singoli esercizi. Lo studente è ammesso all'esame orale se ha ottenuto allo scritto almeno il punteggio minimo di 18. L'esame scritto può essere sostenuto anche in due parti: 1) Calcolabilità e complessità; 2) Logica. In questo caso i voti sulle due parti saranno mediati. L'esame orale è focalizzato prevalentemente (ma non esclusivamente) sulla parte di complessità e di logica. Le domande vertono sulla definizione dei concetti di base, sulle prove dei teoremi presentati nel corso, sulla comprensione ragionata dei concetti studiati. Verranno valutati il grado di conoscenza, la precisione dell'esposizione, la capacità di articolare riflessioni autonome. All'esame orale viene assegnato un punteggio in trentesimi (indipendente dal punteggio conseguito nell'esame scritto). Il voto finale media il voto conseguito alla scritto con la valutazione riportata nell'esame orale (che deve essere almeno di 18/30). La distinzione della lode è assegnata a chi abbia conseguito il voto massimo sia allo scritto sia all'esame orale. L'esame orale può essere alternativamente sostituito con lo sviluppo di un progetto nell'ambiente di specifica Z3 da concordare con il docente.

Questo insegnamento approfondisce argomenti strettamente connessi a uno o più obiettivi dell’Agenda 2030 per lo Sviluppo Sostenibile delle Nazioni Unite