Anno di corso: 1

Anno di corso: 2

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

FONDAMENTI LOGICO MATEMATICI DELL'INFORMATICA

Scheda dell'insegnamento

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

Conoscenza della logica classica

Moduli

Metodi di valutazione

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

Esame scritto con 2 compitini intermedi che comprendono esercizi e domande di teoria aperte

Orale sui 2 compitini

Chi non affronta i 2 compitini dovrà sostenere l'esame scritto che verterà su tutto il programma del corso che comprende esercizi e domande di teoria aperte

Orale sui compito scritto

Valutazione: 
Voto Finale

Obiettivi formativi

Il corso si propone di fornire agli studenti conoscenze relative a logiche non classiche costruttive (intuizionismo e sue estensioni) e modali con implementazione di relativi theorem prover e fornire strumenti per la sintesi logica di algoritmi

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

Il corso si propone di analizzare alcuni argomenti di logica matematica legati alla teoria della dimostrazione in logiche non classiche (intuizionismo e sue estensioni) e alla dimostrazione automatica di teoremi in tali logiche. Verranno presentati sistemi deduttivi diretti (deduzione naturale) e indiretti (tableaux) e vari theorem prover. Per arrivare a questi argomenti si partirà dalla logica classica e si riprenderanno in modo più approfondito gli argomenti abbozzati nel corso di Fondamenti dell’informatica (corso obbligatorio della LT) presentando il calcolo della deduzione naturale e introducendo la forma clausale, il principio di risoluzione, la skolemizzazione e l’algoritmo di unificazione.

Si tratterà poi la sintesi logica degli algoritmi e si farà vedere come non sempre le dimostrazioni in logica classica permettono la sintesi diretta. Per questo si comincerà ad introdurre la logica intuizionista con sintassi a tableaux, semantica con modelli di Kripke e relativi teoremi di validità e completezza con cenni a estensioni dell'intuizionismo. Verranno analizzati i rapporti sintattici e semantici fra logica classica e logica intuizionista. Verranno poi presentati i theorem prover proposizionali PITP, PITPINV, IPTP sviluppati in C con le relative valutazioni delle strategie dimostrative, della complessità computazionale e dell’efficienza rispetto alla libreria di benchmark ILTP. Verranno infine valutati possibili sviluppi a livello predicativo.

Bibliografia consigliata

M. Fittng, Intuitionistic logic, model theory and forcing, North Holland 1965

M. J. Cresswell, G. E. Hughes A New Introduction to Modal Logic, Taylor & Francis Ltd, 1996

G. Boolos, ,The Unprovability of Consistency: An Essay in Modal Logic, CUP, 1969
Slides del titolare del corso nel sito del corso

Metodi didattici

Lezioni in aula