Instructor: Simone Martini
Prerequisites: Formal systems, completeness.
Aims: presentare alcuni concetti di base della teoria della dimostrazione (deduzione naturale, sequenti, eliminazione del taglio e sue conseguenze), cercando di enucleare alcune tecniche dimostrative di particolare rilievo. Il corso introdurra' anche ad alcune aree di ricerca. Si assumer\`a una conoscenza preliminare dei concetti e risultati preliminari relativi alle logiche del primo ordine (gli studenti che non ne siano in possesso possono parlare con Martini per alcuni riferimenti bibliografici).
Programma
1. Fondamenti Di Teoria Della Dimostrazione
1.1 Sistemi di deduzione naturale per la logica classica e intuizionista
1.2 Sistemi a sequenti per la logica classica e intuizionista.
1.3 Relazioni tra i due sistemi.
1.4 Equivalenza con i sistemi alla Hilbert
1.5 Eliminazione del taglio e sue conseguenze.
2. Lambda calcolo tipizzato
2.1 Lambda termini come notazione per deduzioni.
2.2 Propriet\`a sintattiche: normalizzazione forte;Confluenza.
2.3 Calcoli di ordine superiore (cenni).
3. Logica Lineare.
3.1 Presentazione a sequenti.
3.2 Reti di dimostrazione. Cenni ai criteri di correttezza.
Teoremi di normalizzazione.
3.3 Semantica. Semantica delle fasi. Semantica delle dimostrazioni
(cenni alla semantica categoriale). Semantica ``a giochi'' (Blass,
Abramsky-Jagadeesan).
Bibliografia (di base).