Anno di corso: 1

Anno di corso: 2

Crediti: 6
Crediti: 6
Crediti: 6
Crediti: 6
Crediti: 6
Crediti: 6
Crediti: 12
Tipo: A scelta dello studente
Crediti: 3
Tipo: Lingua/Prova Finale
Crediti: 33
Tipo: Lingua/Prova Finale

FONDAMENTI LOGICO MATEMATICI DELL'INFORMATICA

Scheda dell'insegnamento

Anno accademico di regolamento: 
2015/2016
Anno di corso: 
2
Anno accademico di erogazione: 
2016/2017
Tipo di attività: 
Obbligatorio a scelta
Crediti: 
6
Ciclo: 
Secondo Semestre
Ore di attivita' didattica: 
48
Prerequisiti: 

Nozioni di base di logica matematica classica.

Moduli

Metodi di valutazione

Tipo di esame: 
Orale
Modalita' di verifica dell'apprendimento: 

Esame scritto e colloquio

Valutazione: 
Voto Finale

Obiettivi formativi

Si prevede che lo studente acquisisca capacità nel sintetizzare algoritmi, nella formalizzazione e costruzione di dimostrazioni e loro verifica.

Contenuti

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 e vari theorem prover.

Programma esteso

1 Sintesi logica degli algoritmi

2 Introduzione alla logica intuizionista; sintassi a tableaux/deduzione naturale e semantica con modelli di Kripke

3 Teoremi di validità e completezza

4 Introduzione alla logica modale S4; sintassi a tableaux e semantica con modelli di Kripke

5 Teoremi di validità e completezza

6 Rapporti fra S4 e la logica intuizionista Cenni a estensioni dell'intuizionismo e di S4

7 I theorem prover PITP, PITPINV, IPTP e Isabelle.

Bibliografia consigliata

D. Prawitz Natural deduction Dover,. 2006
Calcoli a tableaux (manoscritto del docente)

Metodi didattici

Lezioni frontali