Fondamenti (2009/2010)

Codice insegnamento
4S02789
Crediti
12
Coordinatore
Andrea Masini
Altri corsi di studio in cui è offerto
L'insegnamento è organizzato come segue:
Modulo Crediti Settore disciplinare Periodo Docenti
BASI DI DATI 4 INF/01-INFORMATICA I semestre Carlo Combi
LOGICA COMPUTAZIONALE 4 INF/01-INFORMATICA I semestre Gianluigi Bellin
LINGUAGGI 4 INF/01-INFORMATICA I semestre Andrea Masini

Obiettivi formativi

Modulo: BASI DI DATI
-------
modulo si propone di fornire allo studente i concetti fondazionali delle basi di dati rispetto al modello relazionale dei dati, ai modelli dei dati semistrutturati, ed ai relativi linguaggi di interrogazione.


Modulo: LOGICA COMPUTAZIONALE
-------
Il tema principale di questo modulo e` la computazione logica intesa come "proof-search/search for a counterexample" per le logiche classica, intuizionistica, modali e temporali: per ciascuna di queste logiche, data una formula A trovare una prova di A oppure un modello che rende A falsa. Il metodo preferito, ove possibile, e` quello dei sistemi di Gentzen, in particolare il calcolo dei sequenti che fornisce non solo un sistema di prova elegante (top-down derivation) - in un rapporto non-banale con i calcoli di deduzione naturale - ma anche una procedura di ricerca del controesempio ("semantic tableaux", bottom-up search).

Dopo una ricapitolazione del teorema di completezza per il calcolo dei sequenti classica proposizionale e predicativo rispetto alla semantica Tarskiana (I ordine) si estende la procedura a vari sistemi modali (K, KD, K4, S4) dimostrando il teorema di completezza e la proprieta` del modello finito per la semantica di Kripke.

Una estensione dei metodi di Gentzen alle logiche temporali PLTL e CTL e` tema di ricerca attuale; dopo una presentazione delle semantiche rispettive, si forniscono materiali per l'approfondimento del tema.

Il tema dei rapporti tra la deduzione naturale intuizionistica NJ ed il calcolo dei sequenti LJ e` affrontato mostrando la corrispondenza tra prove cut-free in LJ e deduzioni normali in NJ, con una introduzione al teorema sulla permutabilita` delle inferenze; inoltre si presentano gli algoritmi dei teoremi di eliminazione del cut e della normalizzazione debole e si illustrano esempi di confluenza e non-conluenza per la logica classica intuizionistica e lineare.


Modulo: LINGUAGGI
-------
L'obiettivo del corso è quello di presentare agli studenti le basi teoriche dei linguaggi di programmazione. A tale scopo verranno introdotti vari linguaggi tipati paradigmatici di ordine superiore (lambda calcoli). Tutto il corso sarà incentrato sui concetti di sistema di tipo e di semantica operazionale. Il corso affronterà anche problematiche relative alla definizione di tipi di dato.

Programma

Modulo: BASI DI DATI
-------
- Il modello relazionale: dipendenze funzionali, forme normali, decomposizioni e calcolo relazionale.
- Basi di dati relazionali ad oggetti: modellazione ed interrogazione.
- Basi di dati semistrutturate: XML, XML Schema, DTD, Xquery.
- Basi di dati temporali: modelli, linguaggi di interrogazione e aspetti tecnologici.


Modulo: LOGICA COMPUTAZIONALE
-------
PARTE 1 - (a) Semantic Tableaux per la logica proposizionale classica e modale.
Logica classica come logica della verita`. Semantic tableaux per la logica proposizionale classica; teorema di completezza. Semantica di Kripke delle logiche proposizionali modali K, KD K4, S4. Logica temporale, tempo lineare, branching time: nozioni semantiche fondamentali.

(b) Calcolo dei predicati del primo ordine.
Richiami di semantica. Procedura semantic tableaux e teorema di completezza del calcolo dei predicati del primo ordine.

PARTE 2 - Calcolo dei Sequenti
Nozioni fondamentali, proprieta` della sottoformula, regola del taglio. Permutazione delle inferenze. Eliminazione del taglio e normalizzazione delle prove. Normalizzazione forte e debole. Esempi. Cenni sulla logica lineare ed alle reti di prova.

PARTE 3 - Logica intuizionistica.
Logica intuizionistica come logica della asseribilita` e interpretazione di Heyting-Kolmogorov. Deduzione naturale intuizionista (frammento implicativo con prodotti). Corrispondenza di Curry-Howard (cenni). Corrispondenze fra deduzione naturale e calcolo dei sequenti. Interpretazioni modali della logica intuizionistica (cenni).


Modulo: LINGUAGGI
-------
Definizioni induttive; sistemi di transizione; sistemi di tipo; semantica operazionale strutturale;
Linguaggi di ordine superiore: lambda calcolo tipato: isomorfismo di Curry-Howard; calcoli di ordine superiore; il sistema T: sintassi e semantica; definibilità e tipi di dato; PCF: sintassi e semantica; definibilità e tipi di dato; il sistema F: sintassi e semantica, definibilità e tipi di dato.

Modalità d'esame

Modulo: BASI DI DATI
-------
L'esame consiste in una unica prova, non divisibile, della durata di circa 3 ore su tutto il programma dei tre moduli.


Modulo: LOGICA COMPUTAZIONALE
-------
Esame scritto.


Modulo: LINGUAGGI
-------
L'esame consiste in una prova scritta.

Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

Statistiche esiti
Esiti Esami Esiti Percentuali Media voti Deviazione Standard
Positivi 38.37% 25 3
Respinti 22.09%
Assenti 34.88%
Ritirati 4.65%
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
3.0% 9.0% 6.0% 6.0% 9.0% 9.0% 3.0% 9.0% 12.1% 6.0% 0.0% 15.1% 6.0% 6.0%

Valori relativi all'AA 2009/2010 calcolati su un totale di 86 iscritti. I valori in percentuale sono arrotondati al numero intero più vicino.