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 mean 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 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.
This is the second year that the course is given, the program is still subject to change.
Learning outcomes of the learning unit
At the end of this course, the student will have a concrete knowledge of formal reasoning, she/he will be able to recognize problems that can be modeled in logic, and she/he 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 ) AND oral exam
Written work / report
Additional information:
The grade will be the weighted average of the assignment mark (20%) and of the exam mark (80%).
Since the course is quite new and the number of students is not predictable, we will not settle for a written or oral exam. If the number of students is large (over 40), the exam will be written. Otherwise, a poll will be organized and the majority of answers will determine if the exam will be written or oral. In case of tie, the teacher will choose.
Work placement(s)
Organizational remarks
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