Teoria della Dimostrazione

Corso di Laurea Specialistica in Informatica

Stefano Guerrini


Vai alla pagina dell'A.A. 2007-08 hand.gif



Obiettivi

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Ó di questi sistemi.

Si passerÓ 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÷del (preceduti da un un richiamo delle nozioni base di calcolabitÓ).

Si mostrerÓ quindi il teorema di normalizzazione forte per il sistema F e la rappresentabilitÓ di funzioni e tipi di dato in F. Infine, si vedrÓ la rappresentabilitÓ dell'aritmetica al secondo ordine (aritmetica di Heyting) per mezzo della corrispondenza con il sistema F. Il corso si concluderÓ con una parte seminariale composta da brevi presentazioni (una o due ore) tenute dagli studenti su argomenti proposti dal docente.

Contenuti

  • Calcolo proposizionale
    • Deduzione naturale
    • Relazioni con i sistemi assiomatici alla Hilbert
    • Correttezza e completezza
    • Calcolo dei sequenti
  • Calcolo dei predicati
    • Richiami su linguaggi e teorie del prim'ordine, validitÓ logica e modelli
    • Deduzione naturale e calcolo dei sequenti
    • Correttezza e completezza
    • Compattezza
  • Eliminazione del taglio
    • Teorema di eliminazione del taglio
    • Riduzione di dimostrazioni in deduzione naturale
  • Logica Intuizionistica
    • Differenze e relazioni con la logica classica
    • Interpretazione Brouwer-Heyting-Kolmogorov
    • Modelli della logica intuizionistica
  • Corrispondenza tra dimostrazioni e programmi
    • lambda-calcolo tipato semplice
    • Isomorfismo Curry-Howard
    • Normalizzazione debole e forte
  • Teorema di Godel
    • Richiami di teoria della calcolabilitÓ
    • Aritmetica di Peano e teoremi di incompletezza di G÷del

Approfondimenti

  • 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 proposti dal docente o dagli studenti

Pagine del Corso

Anni Precedenti


-- StefanoGuerrini - 22 Sep 2006

Edit | Attach | Watch | Print version | History: r15 < r14 < r13 < r12 < r11 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r15 - 2007-10-12 - StefanoGuerrini






 
Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback