Materiali Didattici Disponibili

Inserisco una guida ai materiali didattici sviluppati da me insieme ad alcuni collaboratori. Avverto che gli appunti scaricabili qui sono sempre in fase di rielaborazione, manutenzione ed aggiornamento (talvolta intere parti non sono ancora state scritte o sono solo in prima stesura). Si ringraziano in anticipo quanti faranno pervenire osservazioni e segnalazioni atte a migliorare la qualità del materiale messo a disposizione.

• Introduzione alla logica proposizionale e alla procedura DPLL(file.pdf): questa dispensa è utilizzata nei corsi di base di tutti i tipi e contiene i rudimenti della logica proposizionale classica, una introduzione ad alto livello della procedura di Davis-Putnam-Logemann-Loveland, la descrizione della sintassi standard utilizzata negli attuali SAT-solvers, nonchè puntatori a risorse di rete per le implementazioni e per approfondimenti. La dispensa è piuttosto datata; una nuova versione che include aspetti più attuali (CDCL, ecc.) è disponibile (contattare il docente).
• Introduzione alla logica elementare(file.pdf): questa dispensa è utilizzata nel corso di base della laurea triennale, sviluppa sintassi e semantica della logica del primo ordine e introduce il calcolo dei tableaux semantici.
• Risoluzione e sovrapposizione(file.pdf): questa dispensa è utilizzata nei corsi di base per le lauree specialistiche, contiene, oltre alla semantica dei linguaggi elementari, i fondamenti della dimostrazione automatica basata su metodi di saturazione (ossia del Superposition Calculus); lo studente viene introdotto all'uso del dimostratore automatico SPASS e viene stimolato con esempi a formalizzare problemi nella logica del primo ordine con identità e a risolverli col calcolatore. Per una trattazione completa da un punto di vista matematico dei fondamenti del Superposition Calculus si rimanda al mio testo Sfidare l'Indecidibile, Milano, Polimetrica 2004.
• Introduzione alle logiche descrittive(file.pdf): questa dispensa viene utilizzata nelle lauree specialistiche (pur essendo adatta anche alla didattica delle lauree triennali), introduce le logiche descrittive ALC e ALCQ, le nozioni di TBox e ABox e spiega in dettaglio un algoritmo standard per la soddisfacibilità locale.
• Introduzione al model-checking simbolico (file.pdf): questa dispensa viene utilizzata nelle lauree specialistiche, spiega in modo facile i principi del model-checking simbolico in CTL ed introduce all'utilizzo del model-checker NuSMV mediante esempi tratti dalla verifica di proprietà di semplici protocolli per sistemi distribuiti.
• Logica temporale lineare(file.pdf): questa dispensa è utilizzata in corsi complementari per le lauree specialistiche, sviluppa le problematiche relative alla soddisfacibilità e al model-checking per la logica del tempo lineare LTL, utilizzando strumenti basati sia su tableaux che su automi.
• Introduzione alla semantica dei linguaggi naturali(file.pdf): questa dispensa sviluppa argomenti di derivazione linguistica, affrontando da un punto di vista logico alcuni temi classici della semantica modellistica ispirata a Montague.
• A first introduction to the algebra of sentences(file.pdf): questa dispensa ha carattere prettamente matematico ed è stata utilizzata in un corso tenuto alla scuola italiana di logica nell'anno 2000.
• Il teorema di Goedel: questi appunti (parzialmente in formato elettronico) sono utilizzati solo nel corso complementare di Logica 2 e costituiscono semplicemente un ausilio al lettore che voglia affrontare lo studio di capitoli impegnativi di manuali standard di logica matematica.
• Appunti di teoria dei modelli: questi appunti (disponibili solo in forma manoscritta) hanno carattere prettamente matematico e sono stati utilizzati in un corso per la laurea in Matematica nell'a.a. 98-99.

Metto anche a disposizione le slides del corso di dottorato tenuto nella primavera 2010 da L. De Moura (Microsoft Research) sulla soddisfacibilità modulo teorie (SMT): I lezione, II lezione, III lezione, IV lezione.