Logica Computazionale 2011/2012

La logica computazionale è un'area dell'informatica che si occupa del problema di formalizzare la realtà, di studiarne le proprietà principali e, basandosi su queste ultime, di inferirne di nuove. Essa fornisce strumenti fondamentali in ambiti quali la verifica hardware/software, la definizione di linguaggi di programmazione, la gestione di database.





Contenuti del corso


• Logica proposizionale e del primo ordine. Introduzione ad alcune teorie di strutture dati quali liste e array;
• Verifica dei programmi: semantica, tecniche di base e strategie;
• Web semantico: logiche descrittive;






Modalità di esame

L'esame consta di tre parti:
• un esame scritto in cui vengono assegnati degli esercizi riguardanti la logica proposizionale e del primo ordine;
• un esame orale sugli argomenti spiegati a lezione (due domande in tutto);
• l'elaborazione di un progetto di programmazione o di un seminario;
Il voto finale è dato dalla media dei voti che il candidato avrà riportato in ciascuna delle tre prove. Il candidato può sostenere le diverse parti dell'esame in appelli differenti.





Orario di ricevimento

Venerdì dalle 11:00 alle 13:00, stanza 343 blocco I.





Libro di testo (logica proposizionale e del primo ordine)

First-order logic and automated theorem proving. Second Edition. Melvin Fitting. Springer, 1996.





Altri testi


• Sulla semantica e sulla verifica dei programmi, su teorie di strutture dati
  
  
  • The Foundations of Program Verification. Second Edition. Jacques Loeckx, Kurt Sieber. John Wiley & Sons, Inc., 1987.
  • The Calculus of Computation. Decision Procedures with Applications to Verification. Aaron R. Bradley, Zohar Manna. Springer-Verlag Berlin Heidelberg 2007.
  
  
  
• Sulle logiche descrittive
  
  
  • The Description Logic Handbook. Theory, implementation, and applications. Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, Peter F. Patel-Schneider. Cambridge University Press 2007.






Lezioni



1. Giovedì 20 e mercoledì 26 ottobre 2011
Introduzione al corso. Induzione sui numeri naturali. Definizione di insiemi per induzione. Principio di induzione strutturale. Dimostrazione di induzione con la teoria delle liste. Sintassi della logica proposizionale. Costruzione del linguaggio della logica proposizionale. Principio di induzione strutturale. (.pdf)  

2. Venerdì 28 ottobre e venerdì 4 novembre 2011
Nozione di sottoformula. Semantica della logica proposizionale. Connettivi, valutazioni booleane. Nozione di dualità per i connettivi binari. Tautologie, formule soddisfacibili e soddisfacibilità di insiemi di formule. Teorema di deduzione semantica. Teoremi di sostituzione. Forma normale negativa. Notazione uniforme di Smullyan. Formulazioni dei principi di induzione strutturale e di ricorsione strutturale in notazione uniforme. Congiunzioni e disgiunzioni generalizzate. Letterali, clausole, clausole duali, CNF, DNF. (.pdf)  

3. Mercoledì 9 e venerdì 11 novembre 2011
Algoritmo per trasformare una formula in CNF (correttezza e terminazione - Lemma di Koenig). Esempio di computazione di una CNF. Il metodo dei tableaux semantici: introduzione, regole di espansione e costruzione. Correttezza del sistema dei tableaux. Il metodo di risoluzione: regole di espansione e regola di risoluzione. Esempi. (.pdf)  

3. Mercoledì 16 e venerdì 18 novembre 2011
Anomalie del sistema dei tableaux. Il calcolo dei tableaux KE. Ottimizzazioni dei tableaux: tableaux con merging e con lemmi. Insiemi di Hintikka e lemma di Hintikka. Proprietà di consistenza proposizionale e teorema di esistenza di un modello (no dimostrazione). (.pdf)  

4. Mercoledì 23, venerdì 25 e mercoledì 30 novembre 2011
Dimostrazione di completezza per il sistema dei tableaux. Procedura di Davis Putnam. Correttezza e completezza della procedura. I SAT solver. Sistemi di Hilbert. Teorema di Deduzione di Tarski-Herbrand. Correttezza di un sistema di Hilbert. Introduzione al sistema di dimostrazione di Deduzione Naturale. (.pdf)  

5. Venerdì 2 e mercoledì 7 dicembre 2011
Dimostrazione di completezza per un sistema di Hilbert. Sistema di dimostrazione di Deduzione Naturale e sua correttezza. Esempi ed esercizi di logica proposizionale riguardanti tutti i metodi di dimostrazione studiati.

6. Mercoledì 14 dicembre 2011
Logica del I ordine: linguaggi, sostituzioni e unificazione. Algoritmo di unificazione, correttezza e terminazione. (.pdf)  

7. Venerdì 16 e mercoledì 21 dicembre 2011
Logica del I ordine: Semantica. Sostituzioni e assegnamenti. Modelli di Herbrand. Notazione uniforme per le formule quantificate. Insiemi di Hintikka al I ordine, proprietà di consistenza del I ordine e alcuni risultati. Sistema di dimostrazione dei tableaux, della risoluzione e di Hilbert per la logica del I ordine (.pdf)  

8. Venerdì 23 dicembre 2011
Sistema di dimostrazione di deduzione naturale per la logica del I ordine. Teoremi di sostituzione. Skolemizzazione. Teorema di Skolemizzazione. Forma skolemizzata e prenessa. (.pdf)  

9. Martedì 10 gennaio 2012
Versione costruttiva del teorema di Herbrand. Esercitazione logica del I ordine.  

10. Mercoledì 11 gennaio 2012
Introduzione alle logiche descrittive. La logica ALCN (sintassi e semantica). TBox e ABox. Un algoritmo di decisione per ALCN basato sui tableaux.(.pdf)   

11. Venerdì 13 gennaio 2012
Sistemi di dimostrazione dei tableaux e della risoluzione a variabili libere. Esercitazione.  

12. Mercoledì 18 e venerdì 20 gennaio 2012
Il dimostratore per la logica del I ordine PROVER9 . Funzionamento ed esempi di applicazione.  

13. Mercoledì 25 gennaio 2012
Introduzione alla semantica dei programmi. Sintassi e semantica operazionale dei linguaggi di programmazione flowchart e while.(.pdf)  

14.venerdì 27 gennaio 2012
Introduzione alla verifica dei programmi. Nozioni di correttezza parziale, terminazione, correttezza totale. Precondizioni, postcondizioni e invarianti. Definizione del metodo delle asserzioni induttive. Definizione del metodo degli insiemi ben fondati (funzione di ranking). Annotazioni di programma, loop invariant e asserzioni. Esempi di dimostrazioni di correttezza parziale e totale di programmi iterativi e ricorsivi. (.pdf)



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 Basi Teoriche dell'Informatica 2009/2010