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.