Mathematical Logic
A.Y. 2018/2019
Learning objectives
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.
Expected learning outcomes
The principal skills acquired are the logical reasoning and the knowledge of some computer science applications (SAT, OBDD, logic synthesis, logic programming).
Lesson period: First semester
Assessment methods: Esame
Assessment result: voto verbalizzato in trentesimi
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Linea Crema
Responsible
Lesson period
First semester
Course syllabus
The course presents some detailed Logic applications to Computer Science, with the aim of introducing some tools, derived from Logic, to solve problems in Computer Science.
· Brief introduction to propositional and predicate logic.
· SAT problems.
· Binary decision diagrams (OBDDs and ZDDs).
· Logic synthesis.
· Resolution and logic programming.
· Brief introduction to propositional and predicate logic.
· SAT problems.
· Binary decision diagrams (OBDDs and ZDDs).
· Logic synthesis.
· Resolution and logic programming.
Professor(s)
Reception:
By appointment only
Dipartimento di Informatica - Via Celoria 18 - 20135 - Milano (MI)