Corso di laurea: Informatica Programmazione per l'A.A. 2012/2013

Programma del docente:
Introduzione alla statistica descrittiva per l'analisi dati. Cenni alla
esplorazione visuale dei dati. Test statistici per la verifica delle ipotesi.
Classificazione Bayesiana. Trasformazione dei dati: analisi componenti
principali, discriminante id Fisher, percettrone, SVM, kernel methods. Parzen
windows, k-nn, alberi decisionali e loro applicazioni. Modelli di Markov. Reti
Bayesiane e modelli grafici. Cenni alle reti neurali multilivello.

Appunti dattiloscritti diffusi dal docente.
Pattern Classification (2nd Edition) Duda, Hart, Stork, Wyley and Son

Introduzione al corso. Induzione sui numeri naturali. Definizione di insiemi per induzione. Principio di induzione strutturale. Dimostrazione per induzione con la teoria delle liste. Sintassi della logica proposizionale. Costruzione del linguaggio della logica proposizionale. Principio di induzione strutturale.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.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.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.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.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.Logica del I ordine: linguaggi, sostituzioni e unificazione. Algoritmo di unificazione, correttezza e terminazione.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.Sistema di dimostrazione di deduzione naturale per la logica del I ordine. Teoremi di sostituzione. Skolemizzazione. Teorema di Skolemizzazione. Forma skolemizzata e prenessa. Sistemi di dimostrazione dei tableaux e della risoluzione a variabili libere.Introduzione alle logiche descrittive. La logica ALCN (sintassi e semantica). TBox e ABox. Un algoritmo di decisione per ALCN basato sui tableaux.Il dimostratore per la logica del I ordine Prover9 e applicazioni.Introduzione alla semantica dei programmi. Sintassi e semantica operazionale dei linguaggi di programmazione flowchart e while.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.














































































































Priority="66"
Name="Medium

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

Altri testi consigliati:
o The Foundations of Program Verification. Second Edition. Jacques Loeckx, Kurt Sieber. John Wiley & Sons, Inc., 1987.
o The Calculus of Computation. Decision Procedures with Applications to Verification. Aaron R. Bradley, Zohar Manna. Springer-Verlag Berlin Heidelberg 2007.
o 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.

Come
da URL di cui sotto





























































































































Pr

Ross Anderson: Security Engineering: A Guide to Building Dependable Distributed Systems, Wiley