Ensimag Rubrique Formation 2022

Logic bases for computer science - 4MMFLI

  • Number of hours

    • Lectures 16.5
    • Projects -
    • Tutorials 16.5
    • Internship -
    • Laboratory works -
    • Written tests -

    ECTS

    ECTS 3.0

Goal(s)

The aim of this class is to introduce students to several fundamental notions of Logic that are frequently used in computer science. Among other things, students will discover the formal notions of proofs and models, as well as some links between the expressivity of a logic and its decidability. The course focuses on propositional and first-order logic, but more advanced notions such as Satisfiability Modulo Theories are also introduced.

Responsible(s)

Mnacho ECHENIM

Content(s)

Inference systems and logics
Propositional logic

  • Normalization, conjunctive normal form, renaming
  • Refutational inference systems, Resolution
  • Compactness theorem, DPLL
    First-order logic
  • Syntax and semantics
  • Herbrand's theorem, Skolemization
  • The Resolution calculus
  • Congruence closure, Satisfiability Modulo THeories

Prerequisites

Notions of discrete mathematics (definition of a language, proofs by structural induction)
Basic notions from set theory (standard set operations, set-theoretic definition of a function, of a relation...)

Test

Howework, a written exam that lasts two hours.

    • MCC en présentiel **
      N1 = 1/4 CC + 3/4 examen écrit
      N2 = examen écrit
    • MCC en distanciel **
      N1 = 1/3 CC + 2/3 devoir à la maison
      N2 = examen écrit ou oral

Calendar

The course exists in the following branches:

see the course schedule for 2023-2024

Additional Information

Course ID : 4MMFLI
Course language(s): FR

The course is attached to the following structures:

You can find this course among all other courses.

Bibliography

T. Boy de la Tour, M. Echenim: Eléments du cours de Logique 2A Ensimag
R. Caferra: Logique pour l'informatique et pour l'intelligence artificielle. Editions Hermès - Lavoisier