Mathematical logic
A.A. 2018/2019
Obiettivi formativi
The content objectives of the course are threefold:
· Developing the attitude for formalizing problems in propositional and first order logic. The source problems will be taken from puzzles, games, verification of programs and protocols, and knowledge engineering.
· Understanding logic computations performed in appropriate state-of-the-art tools, such as for instance SAT-solvers, SMT-solvers, OBDD libraries, model checkers, provers based on resolution and rewriting or tableaus, and logic programming tools.
· Acquisition of fundamental mathematical concepts related to logic, including the formal semantics of propositional and first order logic.
· Developing the attitude for formalizing problems in propositional and first order logic. The source problems will be taken from puzzles, games, verification of programs and protocols, and knowledge engineering.
· Understanding logic computations performed in appropriate state-of-the-art tools, such as for instance SAT-solvers, SMT-solvers, OBDD libraries, model checkers, provers based on resolution and rewriting or tableaus, and logic programming tools.
· Acquisition of fundamental mathematical concepts related to logic, including the formal semantics of propositional and first order logic.
Risultati apprendimento attesi
Le competenze acquisite con l'insegnamento sono la capacità di ragionamento logico, e la conoscenza approfondita di alcune applicazioni della logica all'informatica (SAT, OBDD, sintesi logica e programmazione logica).
Periodo: Primo semestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Programma e organizzazione didattica
Linea Crema
Responsabile
Periodo
Primo semestre
Programma
L'insegnamento presenta nel dettaglio alcune applicazioni della Logica all'Informatica, con lo scopo di introdurre alcuni strumenti derivati dalla Logica per risolvere problemi informatici.
· Breve introduzione alla logica proposizionale e predicativa.
· Problemi di soddisfacibilità (SAT).
· Diagrammi binari di decisione (OBDDs and ZDDs).
· Sintesi logica.
· Risoluzione e programmazione logica.
· Breve introduzione alla logica proposizionale e predicativa.
· Problemi di soddisfacibilità (SAT).
· Diagrammi binari di decisione (OBDDs and ZDDs).
· Sintesi logica.
· Risoluzione e programmazione logica.
Informazioni sul programma
Le competenze acquisite con l'insegnamento sono la capacità di ragionamento logico, e la conoscenza approfondita di alcune applicazioni della logica all'informatica (SAT, OBDD, sintesi logica e programmazione logica).
Propedeuticità
Nessuna
Prerequisiti
Metodi di accertamento: L'esame consiste in una prova scritta. La prova scritta richiede la soluzione di esercizi di tipo applicativo e teorico, aventi contenuti e difficoltà analoghi a quelli affrontati nelle lezioni. Durante lo scritto non è ammessa la consultazione di testi o appunti.
Metodi didattici
Lezioni frontali
Materiale di riferimento
· Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition), Cambridge University Press, 2004.
· Mordechai Ben-Ari. Mathematical Logic for Computer Science (2nd edition), Springer, 2001.
· Papers in English, distributed by the lecturer and made available through the course's web page.
· Mordechai Ben-Ari. Mathematical Logic for Computer Science (2nd edition), Springer, 2001.
· Papers in English, distributed by the lecturer and made available through the course's web page.
Docente/i
Ricevimento:
Su appuntamento via e-mail
Dipartimento di Informatica - Via Celoria 18 - 20135 - Milano (MI)