Fondamenti - LOGICA COMPUTAZIONALE (2009/2010)

Codice insegnamento
4S02789
Docente
Gianluigi Bellin
crediti
4
Altri corsi di studio in cui è offerto
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Sede
VERONA
Periodo
I semestre dal 1-ott-2009 al 31-gen-2010.

Per visualizzare la struttura dell'insegnamento a cui questo modulo appartiene, consultare * organizzazione dell'insegnamento

Orario lezioni

I semestre
Giorno Ora Tipo Luogo Note
martedì 14.30 - 16.30 lezione Aula I dal 1-ott-2009  al 21-nov-2009
mercoledì 10.30 - 12.30 lezione Aula I dal 1-ott-2009  al 21-nov-2009
giovedì 14.30 - 16.30 lezione Aula I dal 1-ott-2009  al 21-nov-2009

Obiettivi formativi

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.

Programma

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).

Modalità d'esame

Esame scritto.