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...
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 homework and practical 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.
There is a homework, where students are asked to formalize a problem into propositional logic, and solve it using a SAT solver.
An evaluated assignment on the university computers will occur during the allocated slots for the course.
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.
Course materials and 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 )
Other : Practical evaluation on the university computers.
Further information:
There will be a practical evaluation on machines, during the allocated slots for the course. No internet connection will be available. The student will have access to static documentation including python reference, and slides of the course. Students might suggest (at the latest two weeks before the evaluation) additional material that will be subject to approval. No AI tool, web search, community, repositories of solved problems, etc... may be used for this practical evaluation.
For the exam, no document and no electronic help is allowed.
The final grade is 15% for the practical evaluated assignement on the university computers and 85% for the written exam. There is a 5% bonus for answering half the wooclap quizzes successfully.
Students that have a good reason not to attend the course in person must notify the professor within the first three weeks of the course.
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.