Logica in informatica (2020/2021)

Codice insegnamento
4S008914
Docente
Andrea Masini
Coordinatore
Andrea Masini
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Sede
VERONA
Periodo
II semestre dal 1-mar-2021 al 11-giu-2021.

Orario lezioni

Vai all'orario delle lezioni

Obiettivi formativi

Il corso mira a fornire la conoscenza della logica classica e intuizionista (proposizionale e del primo ordine) e del lamba calcolo e della teoria dei tipi. Alla fine del corso gli studenti dovranno dimostrare di possedere le conoscenze necessarie per ragionare all'interno di un sistema logico formale, sia in un ambiente classico che intuizionista. Questa conoscenza consentirà allo studente di: i) eseguire prove formali con un sistema deduttivo; ii) ragionare con sistemi assiomatici. Inoltre gli studenti dovranno sapere come trasferire le nozioni teoriche apprese in contesti logici tipici dell'informatica, come i sistemi di tipo per i linguaggi funzionali. Gli studenti saranno in grado di continuare i loro studi nel campo della logica per l’informatica.

Programma

1. la logica proposizionale:
-proposizioni e connettivi
-semantica
-deduzione naturale
-correttezza e completezza
2. logiche dei predicati:
-quantificatori
-strutture
-tipi di similarità
-semantica
- identità
-deduzione tipi
-correttezza e completezza
3. la normalizzazione in deduzione naturale.
4. confluenza.
5. elementi di teoria dei modelli
-equivalenza, isomorfismo,
6. lambda calcolo senza tipi e con i tipi.
7. il calcolo dei seguenti ed il teorema di cut elimination.
8. Aritmetica di Peano
-primo e secondo teorema di incompletezza

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Jean Louis Krivine, Rene Cori Lambda-calculus, Types and Models Ellis Horwood 1993 978-0130624079
van Dalen, Dirk Logic and Structure. (Edizione 5) Springer 2013 978-1-4471-4557-8

Modalità d'esame

Esame scritto