Syllabus del corso
Obiettivi
L'obiettivo dell'insegnamento è quello di introdurre i concetti fondamentali che legano la logica alla scienza dei calcolatori così che lo studente possa comprendere gli sviluppi moderni della logica computazionale.
Contenuti sintetici
- Inquadramento storico e connessione con i contenuti degli insegnamenti Linguaggi di Programmazione e Linguaggi e Computabilità;
- Introduzione all'Isomorfismo Curry-Howard;
- Fondamenti di Logica Classica e Logica Intuizionista;
- Logiche Modali e Logiche Descrittive.
Programma esteso
- Illustremo come logica e computazione sono connessi partendo dai concetti di programmazione funzionale e teoria della ricorsività illustrati al secondo anno della Laurea Triennale. Questo ci permetterà di introdurre il linguaggio funzionale noto come Lambda Calcolo ed il concetto di Tipo i quali hanno un ruolo chiave nella correttezza dei programmi;
- dal punto precedente arriveremo ad introdurre il concetto di Isomorfismo Curry-Howard noto anche come paradigma Propositions as Types che ha grande importanza nei linguaggi funzionali tipati;
- i precedenti punti oltre ad introdurre aspetti tecnici chiariscono le motivazioni per cui in informatica i concetti logici hanno grande importanza e rendono logica e computazione due concetti strettamente legati. In particolare al termine del punto 2 avremo motivato l'importanza della logica Intuizionista in informatica. Saremo quindi pronti a presentare sintassi, semantica e sistemi di dimostrazione per la logica Classica e successivamente per la logica Intuizionista;
- le logiche modali sono un'ampia famiglia di logiche oggi ampiamente usate in informatica per applicazioni che vanno dalla verifica di sistemi formali, all'analisi di giochi, alla rappresentazione di sistemi di agenti. Studieremo le proprietà base di queste logiche per poi concentrarci sulle logiche descrittive;
- dal punto di vista formale, le logiche descrittive sono varianti delle logiche modali. Cambiano, invece, dal punto di vista applicativo: le logiche descrittive sono utilizzate per rappresentare la conoscenza e ragionare in sistemi intelligenti. In questo punto studieremo le tecniche di ragionamento di questi linguaggi e il loro uso in Intelligenza Artificiale.
Prerequisiti
Nozioni base dagli insegnamenti dei primi due anni della laurea Triennale in Informatica;
Modalità didattica
Lezioni frontali standard. Il sito di "e-learning" verrà usato per distribuire materiale ad-hoc.
Materiale didattico
Open Logic Project è un progetto collaborativo che riunisce in modo organico materiali relativi alla logica matematica insegnata nei corsi di filosofia. Contiene tutti gli argomenti trattati nell'insegnamento e può essere un buon riferimento .
Circa il materiale standard, purtroppo non esiste un unico libro che copra gli argomenti dell'insegnamento.
I seguenti libri ed articoli vengono suggeriti perchè in possesso della nostra biblioteca e/o scaricabili gratuitamente:
- Dirk van Dalen. Logic and structure (3. ed.). Universitext. Springer, 1994. Di interesse i capitoli su logica classica e intuizionista;
- Philip Wadler.Propositions as types. Commun. ACM, 58(12):75–84, 2015. Articolo divulgativo;
- Morten Heine Sörensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006. Testo avanzato che copre i punti da 1 a 3 del programma.
- Markus Krötzsch, Frantisek Simancik, Ian Horrocks. A Description Logic Primer. https://arxiv.org/abs/1201.4089 Breve introduzione alle logiche descrittive.
Periodo di erogazione dell'insegnamento
Secondo semestre;
Modalità di verifica del profitto e valutazione
- Solo prova finale (non ci sono prove in itinere);
- solo prova orale, che può svolgersi in una delle due seguenti modalità:
1. COLLOQUIO SUGLI ARGOMENTI SVOLTI A LEZIONE;
2. COLLOQUIO SU ARGOMENTI DI APPROFONDIMENTO NON TRATTATI A LEZIONE; - per entrambe le tipologie di prova la valutazione riguarda la conoscenza degli argomenti, compresa la capacità di rispondere a domande e svolgere esercizi, chiarezza espositiva e rigore matematico nell'esposizione.
Orario di ricevimento
Per appuntamento via email.
Aims
In this course we introduce the foundations of logic in order to explain the notion of computation. Our aim is to allow the student to manage the recent achievements of logic in computer science.
Contents
-
Historical overview and connections with the courses Programming Languages and
Languages and Computability -
The Curry-Howard Isomorphism or propositions as types paradigm;
-
Foundations of Classical and Intuitionistic logics;
-
Modal and Description Logics.
Detailed program
- Starting from functional programming and recursive theory, we present the intimate relationships between logic and computation. This motivates a brief introduction of the functional language known as Lambda Calculus and the notion of Type: both have an important role in the framework of program correctness;
- previous point motivates the introduction of the Curry-Howard Isomorphism, also known as Propositions as types paradigm that is theoretically important both in typed functional languages and in program correctness;
- previous points are the main motivations to study logic in computer science. It will be clear the importance of Intuitionistic logic in computer science. Thus we start to study Classical and Intuitionistic logic by introducing the key points: syntax, semantics and proof systems;
- Modal logics are widely used in computer science for applications ranging from formal verification, to game analysis, to multi-agent system representation. We will study the basic properties of these logics to focus later on description logics;
- from a formal point of view, description logics are variants of modal logics. They differ from the application point of view: description logics are used to represent knowledge and reason in intelligent systems. We will study the reasoning techniques associated to these languages, and their use in Artificial Intelligence.
Prerequisites
Basic notions from first and second year of Bachelor Degree in Informatica;
Teaching form
The course will be offered as a set of standard lectures during the term. “e-Learning” support will also be provided for the distribution of course material.
Textbook and teaching resource
Open Logic Project is a collection of teaching materials on mathematical logic used in logic courses as taught in many philosophy departments.
Open Logic contains the topics of the course and it can be a good reference.
As regards standard books, there is no a single book covering all points of the course.
The following books and papers are owned by our library and/or are freely downloadable:
- Dirk van Dalen. Logic and structure (3. ed.). Universitext. Springer, 1994. It contains material related to Classical and Intuitionistic logics (point 3 of the program);
- Philip Wadler.Propositions as types. Commun. ACM, 58(12):75–84, 2015. non-technical paper;
- Morten Heine Sörensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006. Advanced book, technical, contains points 1-3 of the program;
- Markus Krötzsch, Frantisek Simancik, Ian Horrocks. A Description Logic Primer. https://arxiv.org/abs/1201.4089 Brief introduction to description logics.
Semester
Second semester.
Assessment method
-
Final exam (no intermediate exam);
-
oral exam. Two possible choices:
- oral exam on the contents of the course;
- oral exam on deeper topics not considered in the program of the course.
-
In both cases we evaluate the knowledge of the topics, included the ability of answer to questions and solve exercises, clarity of presentation and mathematical precision.
Office hours
On request, scheduled via email.