Teoria della Dimostrazione

Anno Accademico 2004/05

Prof. Stefano Guerrini

guerrini at di.uniroma1.it



Domande/Esercizi orale

Ecco una prima lista di domande/esercizi per l'orale di Teoria della dimostrazione

Domande/Esercizi Orale

Si deve rispondere ad almeno due domande/esercizi a scelta in forma scritta o orale.


Discussione Tesine 8-9 Febbraio

La discussione delle tesine avverrà in aula alfa, martedì 8 e mercoledì 9 febbraio, dalle 9.00 alle 14.00.

Tenendo conto di uno slot di 20 minuti a persona più 5-10 minuti di domande e altri tempi morti, in ciascuno dei due giorni potranno tenere la loro presentazione al massimo 10 studenti. Per questo motivo sono attive due pagine di prenotazione

* martedì 8

* mercoledì 9

Tutti gli studenti sono invitati a indicare una preferenza sul giorno della propria presentazione, prenotandosi per mezzo del corrispondente modulo elettronico.

ATTENZIONE! La tesina scritta dovrà essere consegnata entro lunedì alle 9.00 del mattino (meglio se entro venerdì) e preferibilmente in forma elettronica (via email).


Orario delle lezioni

Mercoledì e Giovedì dalle 12.00 alle 13.45 in aula alfa.

Ricevimento

Il giovedì dalle 14.15 alle 15.15, previo appuntamento con il docente durante la lezione o via email.

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

Programma di massima

  • Calcolo dei predicati
    • Richiami su linguaggi e teorie del prim'ordine, validità 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à
  • Aritmetica di Peano e teoremi di incompletezza di Gö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

-- StefanoGuerrini - 22 Sep 2006

Edit | Attach | Watch | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r2 - 2007-10-12 - StefanoGuerrini






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