Page begin -
Logo DISCO
|
Go to the Highly accessible area
|
Go to the Content page
|
Go to the End of content
|
Go to the Main menu
|
Go to the Navigation Bar (location)
|
Go to the Navigation menu (tree)
|
Go to the Commands list
|
Go to the Further readings
|
Go to the Bottom Menu
|
Logo Ateneo
   
Education
Fondamenti logico-matematici dell'informatica (elementi)

Docente: F. Cardone

Crediti: 6

Conoscenze: Nella parte istituzionale del corso verranno esaminati i concetti fondamentali della logica proposizionale e del prim'ordine, sia sul piano sintattico che su quello semantico. Nella parte monografica, verranno sviluppate le corrispondenze tra dimostrazioni formalizzate in sistemi di logica costruttiva e programmi funzionali con tipi da un lato, e tra tipi o formule ed oggetti in opportune categorie. Questa parte del corso si propone di servire come prima introduzione ad un insieme di problematiche che sono alla base di molte ricerche nell'ambito della sintassi e della semantica dei linguaggi di programmazione funzionali con tipi.

Abilità: Lo studente acquisterà familiarità con le principali tecniche di formalizzazione della deduzione, e con alcuni comuni metodi di dimostrazione (in particolare, il principio di induzione matematica). La parte monografica del corso introdurrà lo studente alla teoria delle categorie, un linguaggio usato largamente nella ricerca teorica recente.

Testi consigliati:

Per la parte istituzionale: Gabriele Lolli: Introduzione alla Logica Formale, il Mulino, Bologna, 1991.

Si vedano anche:

Per la parte monografica:

  • Andrea Asperti e Giuseppe Longo: Categories, Types and Structures, MIT Press, Foundations of Computing Series, 1991, capitolo 8. http://www.di.ens.fr/users/longo/download.html
  • Magnan, F. & Reyes, G. E.: Category Theory as a Conceptual Tool in the Study of Cognition. In J. Macnamara & G. E. Reyes (Eds) The Logical Foundations of Cognition. Oxford University Press, New York, pagg. 57-90

Modalità di esame: due compiti scritti durante il corso e una eventuale prova orale con la possibilità di approfondire argomenti particolari attraverso pubblicazioni di ricerca concordate con il docente.

Per ulteriori informazioni sul corso rivolgersi direttamente al docente.

Programma:

  • Logica proposizionale classica: linguaggio e calcolo della deduzione naturale.
  • Semantica mediante tavole di verità e tableaux.
  • Teorema di completezza.
  • Logica dei predicati: linguaggio e calcolo della deduzione naturale.
  • Cenni sui tableaux e la nozione di interpretazione di un linguaggio predicativo.
  • Parte monografica: Il frammento positivo del calcolo proposizionale intuizionista. Calcolo dei sequenti e teorema di eliminazione del taglio. Relazioni con le categorie cartesiane chiuse e il lambda-calcolo con tipi semplici.
Further readings
(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - last update of this page 25/03/2011