Logica Computazionale 2008/2009

 

Lezioni

1. Lunedì 13 e Mercoledì 15 ottobre 2008
Introduzione al corso. Induzione sui numeri naturali. Definizione di insiemi per induzione. Principio di induzione strutturale. Definizione di funzioni per induzione.   

2. Lunedì 20 e Mercoledì 22 ottobre 2008
Sintassi della logica proposizionale. Costruzione del linguaggio della logica proposizionale. Principio di induzione strutturale e di ricorsione strutturale. Nozione di sottoformula. Semantica della logica proposizionale. Connettivi, valutazioni booleane. Tautologie, formule soddisfacibili e soddisfacibilità di insiemi di formule. Teorema di deduzione semantica. Nozione di dualità per i connettivi binari.   

3. Lunedì 27 e Mercoledì 29 ottobre 2008
Teoremi di sostituzione. Forma normale negativa. Notazione uniforme di Smullyan e nuove formulazioni di principio di induzione strutturale e di ricorsione strutturale. Congiunzioni e disgiunzioni generalizzate. Letterali, clausole, clausole duali, CNF, DNF. Algoritmo per trasformare una formula in CNF (correttezza e terminazione - Lemma di Koenig). Introduzione al metodo di dimostrazione dei tableaux semantici.   

4. Lunedì 3 e Mercoledì 5 novembre 2008
Il metodo dei tableaux semantici: regole di espansione e costruzione. Correttezza del sistema dei tableaux. Il metodo di risoluzione: regole di espansione e regola di risoluzione. Correttezza del sistema di risoluzione.   

5. Lunedì 10 e Mercoledì 12 novembre 2008
Insiemi di Hintikka e lemma di Hintikka. Proprietà di consistenza proposizionale e teorema di esistenza di un modello (caso finito e infinito). Dimostrazione di completezza per il sistema dei tableaux e della risoluzione proposizionale.   

6. Lunedì 17 e Mercoledì 19 novembre 2008
Albero semantico. Dimostrazione alternativa del teorema di compattezza. Insiemi di clausole saturi. Insiemi di Robinson. Completezza del sistema di risoluzione in ipotesi di strettezza. Regola di S-introduzione per tableaux e risoluzione. Sistemi di Hilbert. Teorema di Deduzione di Tarski-Herbrand. Correttezza e completezza di un sistema di Hilbert.   

7. Lunedì 24 e Mercoledì 26 novembre 2008
Sistema di deduzione naturale. Correttezza e completezza forte del sistema. Procedura di Davis Putnam. Correttezza e completezza della procedura. I SAT solver.   

8. Lunedì 1 dicembre 2008
I SAT solver: Chaff.   

9. Mercoledì 3 dicembre 2008
Logica del I ordine: linguaggi, sostituzioni e unificazione. Esercitazione sulla logica proposizionale.   

10. Mercoledì 10 dicembre 2008
Logica del I ordine: algoritmo di unificazione, semantica. Esercitazione sulla logica proposizionale.  

11. Lunedì 15 dicembre 2008
Prova in itinere sulla logica proposizionale.

12. Lunedì 12 gennaio 2009
Modelli di Herbrand. Notazione uniforme per il I ordine. Principio di induzione e di ricorsione strutturale.   

13. Mercoledì 14 gennaio 2009
Sistema dei tableaux, di risoluzione, di Hilbert e di deduzione naturale per la logica del I ordine.   

Home
Corso di Progetto Software 2007/2008
Corso di Progetto Software 2008/2009

Corso di Logica Computazionale 2008/2009
Corso di Logica Computazionale 2009/2010
Corso di Logica Computazionale 2010/2011
Corso di Logica Computazionale 2011/2012
Corso di Logica Computazionale 2012/2013
Corso di Logica Computazionale 2013/2014
Corso di Basi Teoriche dell'Informatica 2009/2010