Course teacher(s)
Emmanuel FILIOT (Coordinator)ECTS credits
5
Language(s) of instruction
french
Course content
-
Boolean logic: syntax, semantics, satisfiability testing algorithms, natural deduction, resolution.
-
Problem reduction, particularly reduction to the Boolean satisfiability problem, and the use of SAT solvers.
-
Introduction to problem complexity: complexity classes P and NP, NP-completeness, other classes.
-
Introduction to computability: Turing machines, undecidable problems.
-
First-order logic: syntax, semantics, resolution, problem modeling in first-order logic, and use of solvers.
-
Formalization of program properties and correctness proofs: Hoare triples.
-
Finite automata and regular expressions.
Objectives (and/or specific learning outcomes)
This course aims to familiarize students with the fundamental concepts of computer science: logic and its applications, proof systems, problem reduction, complexity, computability, computational models, program correctness. The course provides a general introduction to these notions and does not replace more advanced Master-level courses, particularly those on computability and complexity.
For problem reduction, the course will focus especially on the Boolean satisfiability problem, for which many solving tools exist.
By the end of this course, students should:
-
Understand the basic notions covered,
-
Be able to model and formalize concrete computer science problems, especially in logic,
-
Be able to formalize mathematical properties,
-
Master classical deduction rules for proof formalization.
Prerequisites and Corequisites
Required and Corequired knowledge and skills
Basic notions of algorithmic (sorting algorithms, graph algorithms such as graph traversals) and programming (in Python).
Cours co-requis
Cours ayant celui-ci comme co-requis
Teaching methods and learning activities
-
Lectures and exercises.
-
Completion of a project: solving a problem using logical formalization and a solver.
References, bibliography, and recommended reading
Université Virtuelle (slides given by the teacher)
Course notes
- Université virtuelle
Contribution to the teaching profile
This course contributes to learning the rigorous formalization of problems and their analysis. The concepts covered are fundamental and part of the essential knowledge required for rigorous analysis of both practical and theoretical problems.
Other information
Contacts
efiliot@ulb.be
Campus
Plaine
Evaluation
Method(s) of evaluation
- Other
Other
Written exam and project.
Important note: During each exam session, a student may be contacted by the course coordinator to justify their answers to the written exam. The date for such convocations will be communicated to the whole cohort at the start of the session. Students will be contacted by email at least one day in advance. Failure to attend will result in a grade of zero for the course.
Mark calculation method (including weighting of intermediary marks)
First session
-
The written exam contains a question about the project.
-
If the student scores at least 50% of the points on that question:
-
The project can count for one quarter of the final grade, but only if it improves the overall grade.
-
In this case, the final grade is either the exam grade alone, or the weighted combination of exam and project (¾ exam, ¼ project), whichever is higher.
-
-
If the student scores less than 50% on that question:
-
The project is not taken into account.
-
The final grade is simply the exam grade.
-
Important note: The project question contributes to the written exam grade itself, so doing the project is strongly recommended. Also, project grades cannot be carried over from one year to the next.
Second session
-
The second session is a written exam only; there is no new project.
-
The exam does not include a project-related question.
-
However, the project may still count for one quarter of the grade if two conditions are met:
-
The student had scored at least 50% on the project-related question in the first session exam.
-
Including the project grade improves the overall grade.
-
-
Otherwise, the final grade is simply the second-session exam grade.
Language(s) of evaluation
- french