Duration
24h Th, 20h Pr
Number of credits
Lecturer
Language(s) of instruction
English language
Organisation and examination
Teaching in the first semester, review in January
Schedule
Units courses prerequisite and corequisite
Prerequisite or corequisite units are presented within each program
Learning unit contents
The course introduces logic, as a means of specification and reasoning for the engineer and computer scientist.
The first part of the course focuses on propositional logic, and the fundamental NP-complete problem: propositional satisfiability (SAT). Modern SAT solving techniques are introduced. We model a few concrete puzzles and solve them using SAT solving techniques.
The second part of the course introduces the predicate calculus, with the Herbrand Theorem. Undecidability of first-order logic is discussed, and an example of a decidable subclass (namely, the Bernays-Schönfinkel class). First-order logic is put into perspective, with a short introduction to logic programming, and a glimpse on formal verification.
The end of the course surveys a few advanced topics: first-order logic with equality, satisfiability modulo theories, proof assistants, Gödel Theorem, as well as model-checking.
Practical sessions focus on modeling problems in logic and methods for solving logic formulas.
Learning outcomes of the learning unit
At the end of this course, students will have a concrete knowledge of formal reasoning, they will be able to recognize problems that can be modeled in logic, and they will be able to use techniques to solve problems encoded in logic.
This course contributes to the learning outcomes I.1, I.2, I.3, II.1, III.1, IV.1, IV.3, VII.1, VII.2, VII.4 of the MSc in data science and engineering.
This course contributes to the learning outcomes I.1, I.2, II.1, III.1, IV.1, IV.3, VII.1, VII.2, VII.4 of the MSc in computer science and engineering.
Prerequisite knowledge and skills
Some introduction to discreete mathematics, e.g. as provided by the courses:
MATH2032-1, Introduction aux mathématiques discrètes
MATH2019-1, Mathématiques pour l'informatique 1
Advanced knowledge in programming, with some notions of complexity, e.g. as provided by:
INFO0902-1, Structures des données et algorithmes
INFO2050-1, Programmation avancée
Support for the assignment is given in Python. It is assumed that the student is sufficiently fluent with imperative programming to jump into a simple Python program and modify it.
Planned learning activities and teaching methods
Lectures are given in English. The practical sessions include formalizing problems into logic, and solving logic formulas. The evaluated assignment will also be about modeling some puzzle in logic.
Mode of delivery (face to face, distance learning, hybrid learning)
Face-to-face course
Additional information:
1st quadrimester.
Lectures are given in English.
Recording of the course will be given as best effort: there is no guarantee everything will be recorded, and there is no guarantee on the quality of the recordings.
Recommended or required readings
Notes and transparencies available on the course space on eCampus.
Exam(s) in session
Any session
- In-person
written exam ( open-ended questions )
Written work / report
Additional information:
The grade will be the weighted average of the assignment mark (20%) and of the exam mark (80%).
For the exam, two A4 sheets of notes (four pages), handwritten or typeset in a reasonable font (>= 10 pt), are allowed.
Work placement(s)
None
Organisational remarks and main changes to the course
The contents of the theoretical and practical sessions, as well as the assignments and useful links, will be made available on the e-Campus space for the course.
Contacts
Teacher: Pascal Fontaine
Phone: 04 366 28 75
e-mail: Pascal.Fontaine@uliege.be
Association of one or more MOOCs
There is no MOOC associated with this course.