Docente: Ugo Moscato
Crediti: 4 cfu
CONOSCENZE
Il corso si propone di analizzare alcuni argomenti di logica matematica legati alla teoria della dimostrazione in logiche non classiche (intuizionismo e logiche modali) e alla dimostrazione automatica di teoremi in tali logiche. Verranno presentati per tali logiche sistemi deduttivi a tableaux.
CAPACITA’
Si prevede che lo studente acquisisca capacità nel sintetizzare algoritmi, nella formalizzazione e costruzione di dimostrazioni e loro verifica.
PROGRAMMA
Riepilogo dei principali risultati del corso di Fondamenti logico-matematici dell'informatica (elementi).
Sintesi logica degli algoritmi
Introduzione alla logica intuizionista; sintassi a tableaux e semantica con modelli di Kripke.
Teoremi di validità e completezza.
Introduzione alla logica modale S4; sintassi a tableaux e semantica con modelli di Kripke.
Teoremi di validità e completezza.
Rapporti fra S4 e la logica intuizionista Cenni a estensioni dell'intuizionismo e di S4.
I theorem prover PITP, PITPINV, IPTP e Isabelle.