AnnoAcc0607 < TD

----
----

---+!! Teoria della Dimostrazione

---++++!! Corso di Laurea Specialistica in Informatica

---++++!! [[Users.StefanoGuerrini][Stefano Guerrini]]

----

---++++!! Anno Accademico 2006/07

----
----

%TOC%

----
----

---+++ Obiettivi e contenuti

Il corso ha lo scopo di fornire le nozioni di base della teoria della dimostrazione e le principali
connessioni tra questa e l'informatica. In particolare, le basi logiche per lo studio dei linguaggi
di programmazione e della teoria dei tipi.

Dopo un richiamo delle principali nozioni di logica di base, si studieranno le relazioni tra i sistemi
alla Hilbert del primo ordine, la deduzione naturale e il calcolo dei sequenti e le principali propriet&agrave;
di questi sistemi.

Si passer&agrave; poi allo studio della logica intuizionistica e della sua interpretazione
Brouwer-Heyting-Kolmogorov.

Prima di passare allo studio dei sistemi del secondo ordine (sistema F),
si dimostreranno i teoremi di incompletezza di G&ouml;del (preceduti da un 
un richiamo delle nozioni base di calcolabit&agrave;).

Si mostrer&agrave; quindi il teorema di normalizzazione forte per il sistema F e la
rappresentabilit&agrave; di funzioni e tipi di dato in F. Infine, si vedr&agrave;
la rappresentabilit&agrave; dell'aritmetica al secondo ordine (aritmetica di Heyting)
per mezzo della corrispondenza con il sistema F. 

Il corso si concluder&agrave; con una parte seminariale composta da brevi presentazioni
(una o due ore) tenute dagli studenti su argomenti proposti dal docente.

---++++ Programma di massima

   * Calcolo dei predicati
      * Richiami su linguaggi e teorie del prim'ordine, validit&agrave; logica e modelli
      * Sistemi deduttivi:
         * Sistemi assiomatici alla Hilbert
         * Deduzione naturale
         * Calcolo dei sequenti
         * Corrispondenze tra i sistemi deduttivi
      * Corretteza e completezza.
   * Riduzioni ed eliminazione del taglio
      * Riduzione di dimostrazioni in deduzione naturale
      * Teorema di eliminazione del taglio
   * Richiami di teoria della calcolabilit&agrave;
   * Aritmetica di Peano e teoremi di incompletezza di G&ouml;del
   * Logica Intuizionistica
      * Differenze e relazioni con la logica classica
      * Interpretazione Brouwer-Heyting-Kolmogorov e isomorfismo Curry-Howard
      * Modelli della logica intuizionistica
   * Sistemi di ordine superiore
      * Polimorfismo e sistema F
      * Teorema di forte normalizzazione
      * Funzioni e tipi di dato rappresentabili nel sistema F
      * Aritmetica di Heyting
   * Parte seminariale su temi di approfondimento proposti dal docente e scelti dagli studenti

---+++ Esercizi

   * [[%ATTACHURL%/LogComb.pdf][Logica Combinatoria]]: Trovare la corrispondenza tra Logica Combinatoria e un sistema assiomatico alla Hilbert per l'implicazione.

   * [[%ATTACHURL%/Formule.pdf][Logica Intuizionista]]: Dimostrare se alcune fomule sono derivabili o meno in NJ, per via sintattica (ragionando sulle regole di NJ) e per via semantica (usando la semantica di Kripke).

   * [[%ATTACHURL%/NJintoLL.pdf][Traduzione NJ in LL]]: Trovare come tradurre le dimostrazioni di NJ nella Logica Lineare.

-- Users.StefanoGuerrini - 22 Sep 2006

Attachments

Topic attachments
I	Attachment	History	Action	Size	Date	Who	Comment
pdf	Formule.pdf	r1	manage	27.7 K	2007-10-12 - 11:58	StefanoGuerrini	Logica Intuizionista
pdf	LogComb.pdf	r1	manage	70.0 K	2007-10-12 - 11:57	StefanoGuerrini	Logica Combinatoria
pdf	NJintoLL.pdf	r1	manage	51.3 K	2007-10-12 - 11:59	StefanoGuerrini	Traduzione NJ in LL

This topic: TD > WebHome > AnnoAcc0607
Topic revision: r3 - 2007-10-12 - StefanoGuerrini