2023-2024 / INFO9015-1

Logic for Computer Science


24h Th, 20h Pr

Number of credits

 Bachelor of Science (BSc) in Computer Science5 crédits 
 Master of Science (MSc) in Data Science5 crédits 
 Master of Science (MSc) in Computer Science and Engineering5 crédits 
 Master of Science (MSc) in Data Science and Engineering5 crédits 
 Master of Science (MSc) in Computer Science5 crédits 


Pascal Fontaine

Language(s) of instruction

English language

Organisation and examination

Teaching in the first semester, review in January


Schedule online

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)


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.


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.