MATHEMATICAL LOGIC FOR COMPUTER SCIENCE
Course objectives
General Objectives: The objective of the course is to introduce students to the fundamental results and methods of Mathematical Logic with a special attention to their applications in Computer Science. Specific Objectives: The specific objective of the course is twofold. In the first place the course is meant to offer a rigorous knoweldge and an ability to apply those methods and results of Mathematical Logic that have numerous applications in many areas of Computer Science. In the second place the aim is to endow the student with a set of fundamental tools in the perspective of doing active research in theoretical Computer Science. Knowledge and Understanding: The course aims at endowing the student with a rigorous in-depth knowledge of the course topics through the study of poofs and the production of rigorous arguments in homework assignments. Particular attention is devoted to conceptual motivation, rigorous proofs and applicability of results and methods. Applying knowledge and understanding: The methods of Mathematical Logic play a fundamental role in many areas of Computer Science such as Complexity Theory, Database Theory, Artifical Intelligence. The aim of the course is to stimulate in the student the ability to apply the methods and the results in various contexts of Computer Science. Autonomy of judgement: Active participation to the course is encouraged. Autonomous judgement is exercised through homework assignments and problem-solving tasks. Communication skills: The student has the option to give a class presentation of a result as final exam in the form of an academic scientific talk. Future learning abilities: The methods of analysis and formalization acquired during the course can be fruitfully applied in many different contexts. The formalization and problem-solving exercise offered during the course strengthens the learning abilities and the capacity of acquiring new skills.
Channel 1
GIUSEPPE PERELLI
Lecturers' profile
Program - Frequency - Exams
Course program
Part 1 (Propositional calculus and First Order Logic)
- Foundations: Propositional calculus, structures and models. Theories. Definability, completeness, decidability, examples of complete theories, quantifier elimination, isomorphism and elementary equivalence of structures.
- Finite Model Theory: expressibility of queries in various logics. Methods to prove the non-expressibility of queries, Ehrenfeucht-Fraissé games, back and forth conditions, Gaifman locality, logical characterization of complexity classes (Fagin's Theorem on NP).
- Undecidability: undecidability of validity (Church and Trakhtenbrot Theorems), undecidability of arithmetic truth (Gödel Theorems), Arithmetic Hierarchy, computation with oracles, Post's Theorems, theorems with computable instances without computable solutions (König, Ramsey, Hindman Theorems).
Part 2 (Modal Logic)
- Basic Concepts: Relational Structures; Modal Languages; Models and Frames; General Frames; Modal Consequence Relations; Normal Modal Logics
- Models: Invariance Results; Bisimulation; Finite Models; The Standard Translation
- Frames: Frame Definability; Frame Definability and Second-Order Logic: Definable and Undefinable Properties; Finite Frames; Automatic First-Order Correspondence
Prerequisites
Basics of Set Theory and Discrete Mathematics.
Books
1. Introduction to Mathematical Logic, Elliot Mendelson (https://www.karlin.mff.cuni.cz/~krajicek/mendelson.pdf)
2. A concise introduction to Mathematical Logic, W. Rautenberg (Springer 2006)
3. Elements of Finite Model Theory, L. Libkin (https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf)
4. Modal Logic, P. Blackburn, M. de Rijke, Y. Venema (Cambridge University Press)
5. Reasoning about Knowledge, R. Fagin, J. Halpern, Y. Moses, M. Vardi (MIT Press)
Frequency
Non mandatory but strongly reommended, especially for completing the Homework.
Exam mode
A set of Homework taken during the course (40%) and a final exam (60%) with a class presentation on a topic related to those presented during the course.
Lesson mode
Face to face lessons.
GIUSEPPE PERELLI
Lecturers' profile
Program - Frequency - Exams
Course program
Part 1 (Propositional calculus and First Order Logic)
- Foundations: Propositional calculus, structures and models. Theories. Definability, completeness, decidability, examples of complete theories, quantifier elimination, isomorphism and elementary equivalence of structures.
- Finite Model Theory: expressibility of queries in various logics. Methods to prove the non-expressibility of queries, Ehrenfeucht-Fraissé games, back and forth conditions, Gaifman locality, logical characterization of complexity classes (Fagin's Theorem on NP).
- Undecidability: undecidability of validity (Church and Trakhtenbrot Theorems), undecidability of arithmetic truth (Gödel Theorems), Arithmetic Hierarchy, computation with oracles, Post's Theorems, theorems with computable instances without computable solutions (König, Ramsey, Hindman Theorems).
Part 2 (Modal Logic)
- Basic Concepts: Relational Structures; Modal Languages; Models and Frames; General Frames; Modal Consequence Relations; Normal Modal Logics
- Models: Invariance Results; Bisimulation; Finite Models; The Standard Translation
- Frames: Frame Definability; Frame Definability and Second-Order Logic: Definable and Undefinable Properties; Finite Frames; Automatic First-Order Correspondence
Prerequisites
Basics of Set Theory and Discrete Mathematics.
Books
1. Introduction to Mathematical Logic, Elliot Mendelson (https://www.karlin.mff.cuni.cz/~krajicek/mendelson.pdf)
2. A concise introduction to Mathematical Logic, W. Rautenberg (Springer 2006)
3. Elements of Finite Model Theory, L. Libkin (https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf)
4. Modal Logic, P. Blackburn, M. de Rijke, Y. Venema (Cambridge University Press)
5. Reasoning about Knowledge, R. Fagin, J. Halpern, Y. Moses, M. Vardi (MIT Press)
Frequency
Non mandatory but strongly reommended, especially for completing the Homework.
Exam mode
A set of Homework taken during the course (40%) and a final exam (60%) with a class presentation on a topic related to those presented during the course.
Lesson mode
Face to face lessons.
LORENZO CARLUCCI
Lecturers' profile
Program - Frequency - Exams
Course program
Fundamentals: predicate logic, models and structures. Theories. Definability, completeness, decidability, examples
of complete and decidable theories, quantifier elimination, isomorphism and elementary equivalence of structures.
Finite Model Theory: expressibility of queries in various logic. Methods for proving the non-expressibility of
queries, Ehrenfeucht-Fraissé games, Back-and-forth conditions, Gaifman locality, logical characterization of
complexity classes (Fagin's Theorem on NP).
Undecidability: undecidability of validity (Church's Theorem, Trakhtenbrot's Theorem), undecidability of arithmetical
truth, undefinability of arithmetical truth, Gödel's Incompleteness Theorems, Arithmetical Hierarchy, oracle computation,
Post's Theorem, theorems with computable instances and no computable solution (König, Ramsey, Hindman).
Miscellaneous: choice of more advanced research topics.
Prerequisites
Basic notions about boolean connectives, familiarity with the informal concept of algorithm.
Books
Handouts by the teacher.
Frequency
Attendance is strongly encouraged. The student who wishes to give the exam without attending the course should contact the instructor before the beginning of the lectures in order to agree on an adequate study program.
Exam mode
Homework: 4/5 sets of homework assignments.
Final: either a written exam with problems or a class presentation of a research topic/paper.
Grading policy: Final grade is 40% homework and 60% final.
Bibliography
1. Introduction to Mathematical Logic, Elliot Mendelson
2. A concise introduction to Mathematical Logic, W. Rautenberg
3. Elements of Finite Model Theory, L. Libkin
Lesson mode
Lecture. Student participation is strongly encouraged through a dialogical approach that favours interaction.
Significant space is given to the in-depth comprehension of the new concepts through the use of examples and exercises.
LORENZO CARLUCCI
Lecturers' profile
Program - Frequency - Exams
Course program
Fundamentals: predicate logic, models and structures. Theories. Definability, completeness, decidability, examples
of complete and decidable theories, quantifier elimination, isomorphism and elementary equivalence of structures.
Finite Model Theory: expressibility of queries in various logic. Methods for proving the non-expressibility of
queries, Ehrenfeucht-Fraissé games, Back-and-forth conditions, Gaifman locality, logical characterization of
complexity classes (Fagin's Theorem on NP).
Undecidability: undecidability of validity (Church's Theorem, Trakhtenbrot's Theorem), undecidability of arithmetical
truth, undefinability of arithmetical truth, Gödel's Incompleteness Theorems, Arithmetical Hierarchy, oracle computation,
Post's Theorem, theorems with computable instances and no computable solution (König, Ramsey, Hindman).
Miscellaneous: choice of more advanced research topics.
Prerequisites
Basic notions about boolean connectives, familiarity with the informal concept of algorithm.
Books
Handouts by the teacher.
Frequency
Attendance is strongly encouraged. The student who wishes to give the exam without attending the course should contact the instructor before the beginning of the lectures in order to agree on an adequate study program.
Exam mode
Homework: 4/5 sets of homework assignments.
Final: either a written exam with problems or a class presentation of a research topic/paper.
Grading policy: Final grade is 40% homework and 60% final.
Bibliography
1. Introduction to Mathematical Logic, Elliot Mendelson
2. A concise introduction to Mathematical Logic, W. Rautenberg
3. Elements of Finite Model Theory, L. Libkin
Lesson mode
Lecture. Student participation is strongly encouraged through a dialogical approach that favours interaction.
Significant space is given to the in-depth comprehension of the new concepts through the use of examples and exercises.
- Lesson code1047636
- Academic year2025/2026
- CourseComputer Science
- CurriculumSingle curriculum
- Year2nd year
- Semester2nd semester
- SSDINF/01
- CFU6