Laurea specialistica - II semestre - I ciclo
Inizio del corso : martedi' 15 febbraio 2004
Durata : 5 settimane

Orario
LUN 13-15 aula Mondolfo, via Zamboni 38
MAR 13-15 aula Mondolfo, via Zamboni 38
GIO 13-15 aula Mondolfo, via Zamboni 38

Crediti : 5 cfu

Programma:

Teoria della dimostrazione

Problemi e temi della odierna teoria della dimostrazione. La dimostrazione automatica. Procedure e calcoli per la ricerca di dimostrazioni.

Calcoli di sequenti per la logica intuizionista ed alcune logiche intermedie

Tecniche di eliminazione delle cesure usando "riscrittura di termini"

Tecniche di eliminazione delle cesure usando argomenti di riducibilità

Calcoli per la sostituzione esplicita

Calcoli per la ricerca di dimostrazioni basati sul calcolo LJT di Herbelin

Corrispondenza tra deduzione naturale e calcoli di sequenti

Calcoli di sequenti con etichette per logiche modali proposizionali

Calcoli di sequenti con etichette per logiche intermedie proposizionali

Bibliografia

Dispense


Per questo corso prevede la collaborazione del Dr Roy Dyckhoff dell'Universita' di St Andrews e le lezioni saranno accompagnate da
costante "supervisione".

L'esame consiste essenzialmente nelle esercitazioni svolte durante il corso.