- Docente: Claudio Sacerdoti Coen
- Crediti formativi: 6
- SSD: MAT/01
- Lingua di insegnamento: Italiano
- Modalità didattica: Convenzionale - Lezioni in presenza
- Campus: Bologna
-
Corso:
Laurea Magistrale in
Scienze filosofiche (cod. 8773)
Valido anche per Laurea Magistrale in Informatica (cod. 5898)
-
dal 20/09/2023 al 02/11/2023
Conoscenze e abilità da conseguire
Al termine del corso, lo studente conosce le basi logico formali dell'informatica, in particolare, il lamb da calcolo e la sua teoria, corrispondenza tra programmi e dimostrazioni, il lamb da calcolo tipato semplice, i sistemi T ed F. È in grado di descrivere semplici funzioni numeriche in lamb da calcolo e di derivarne i tipi.
Contenuti
Primo modulo:
1. Richiami di Logica Proposizionale e al Prim'Ordine.
Sintassi, Semantica, Correttezza e Completezza, Indecidibilità della
Logica al Prim'Ordine
2. Lambda Calcolo non tipato.
Sintassi e Semantica Operazionale. Il Lambda Calcolo come linguaggio di
programmazione: stategie di valutazione e rappresentazione dei dati;
Turing completezza (cenni).
3. Meta-teoria del Lambda Calcolo non tipato.
Confluenza.
4. Lambda Calcolo Tipato Semplice e Isomorfismo di Curry-Howard
Sintassi alla Curry e alla Church. Isomorfismo con la logica
proposizionale minimale. Algoritmi per il type-checking e la type-
inference.
5. Meta-teoria del Lambda Calcolo tipato semplice.
Teoremi di normalizzazione debole e forte.
6. Isomorfismo di Curry-Howard ed estensioni del sistema di tipi.
Tipi prodotto, coprodotto, vuoto e singleton. Polimorfismo parametrico
(cenni al System F). Cenni ai sistemi di tipi dipendenti e al tipaggio
alla Hindley-Milner.
Secondo modulo:
1. Logica e Basi di Dati
Algebra Relazionale, FO come Linguaggio di Query, Algebre
Cilindriche, Aspetti Implementativi
2. Logica e Complessità Computazionale
Strutture Finite e Problemi Decisionali, Caratterizzazione di NP e
PSPACE tramite logiche al Prim'Ordine. SAT Solving.
3. Logica e Metodi Formali
LTL e CTL: sintassi e semantica. Sistemi Reattivi e Loro Verifica.
Model Checking.
4. Logica e Intelligenza ArtificialeLogica epistemica: sintassi, semantica, Esempi di Applicazione
Testi/Bibliografia
Per il primo modulo:
- H.P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Available on-line at http://www.cs.unibo.it/~sacerdot/fli1718/barendregt.pdf
- J.Y. Girard, Y. Lafont, P. Taylor: Proof and Types. Available on-line at http://www.paultaylor.eu/stable/Proofs+Types.html
Gli argomenti del libro di Barendregt che saranno presentati a lezione sono già contenuti nella seguente dispensa dello stesso autore:
http://www.cs.unibo.it/~sacerdot/fli1718/IntroductionToLambdaCalculus.pdf
Per il secondo modulo:
- N. Immerman. Descriptive Complexity. Springer, 1999. http://people.cs.umass.edu/~immerman/book/descriptiveComplexity.html
- J. Ullman. Principles of database and knowledge-base systems, Volume I. Computer Science Press, 1990.
- E. Clarke and O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.
Metodi didattici
Il corso si svolge al primo semestre e prevede in lezioni frontali in aula e on-line o, nel caso le condizioni sanitarie lo richiedessero, solamente on-line. Durante le lezioni frontali vengono trattati esaustivamente tutti gli argomenti del corso, fornendo dimostrazioni dettagliate della maggior parte dei teoremi.
A seconda dell'argomento trattato si utilizzeranno lucidi oppure la lezione verrà svolta alla lavagna.
Modalità di verifica e valutazione dell'apprendimento
Esame orale.
Persone con disabilità e DSA
Le persone con disabilità o disturbi specifici dell’apprendimento hanno diritto a speciali adattamenti in relazione alla loro condizione, previa valutazione del Servizio d’ateneo per le studentesse e gli studenti con disabilità e DSA. Si prega di non rivolgersi al/la docente, ma di contattare il Servizio per un appuntamento. Sarà cura del Servizio stabilire quali adattamenti si rendono opportuni. Maggiori informazioni alla pagina site.unibo.it/studenti-con-disabilita-e-dsa/it/per-studenti.
Strumenti a supporto della didattica
Verranno forniti i lucidi presentati a lezione. Si daranno inoltre puntatori ad articoli scientifici e testi divulgativi scaricabili liberamente dal Web.
Orario di ricevimento
Consulta il sito web di Claudio Sacerdoti Coen