Outils pour utilisateurs

Outils du site


Panneau latéral



Contacts

Scolarité L1/L2

Audrey Dalla Francesca (coordinatrice Licence et Master, en appui à la gestion pédagogique L1-L2)
téléphone 01 57 27 94 36
bureau Sophie Germain - Bur. 3055
En télétravail les jeudis et vendredis
(permanences Zoom : 14h00-17h00)

connexion à la permanence d'Audrey Dalla Francesca (code: 482147)

Marie Chandellier (gestionnaire L1 et L2)
téléphone 01 57 27 94 99
bureau Sophie Germain - Bur. 3055
Ne travaille pas les vendredis
(permanences Zoom du lundi au jeudi: 10h00-12h00)

connexion à la permanence de Marie Chandellier (code: 222732)


Scolarité L3

Raja Taimes
téléphone 01 57 27 68 93
bureau Sophie Germain - Bur. 3005
En télétravail les mercredis et vendredis
(permanences Zoom : 10h00-12h00 ; 14h00-15h00)

connexion à la permanence de Raja Taimes (code: 481714)

formations:licences:ue:l3:lo5

Table des matières

Logique

Description

L'objectif principal est de savoir utiliser la logique pour modéliser des problèmes et les résoudre ensuite à l'aide de logiciels comme les solveurs SAT et les solveurs SMT. Cela demande une bonne familiarité avec les formules logiques, leur sémantique, et leur manipulation par exemple à l'aide de mises sous formes normales, ainsi qu'une compréhension des principes de base de ces solveurs.

Des implémentations en Java ou en OCaml (qui est introduit en cours programmation fonctionnelle PF5) de la plupart des constructions du cours sont soit fournies soit réalisées en exercice.

Le cours introduit des notions qui seront approfondies entre autres dans les cours de bases de données (BD6), puis en Master en calculabilité et complexité, programmation logique et par contraintes, preuves assistées par ordinateur, sémantique des langages de programmation, méthodes formelles de vérification, et modélisation et spécification.

Syllabus

Le cours revisite la logique propositionnelle vue en cours d'outils logiques (OL4), et introduit la logique du premier ordre. Le programme général est :

  1. Logique propositionnelle :
    • Syntaxe et sémantique
    • Conséquences et équivalences logiques
    • Formes normales, forme clausale
    • Modélisation, solveurs SAT, recherche de modèle, algorithme DPLL
    • Recherche de preuve, calcul des séquents propositionnel
  2. Logique du premier ordre :
    • Syntaxe et sémantique
    • Formes normales, skolémisation
    • Théories logiques, interprétations normales, élimination des quantificateurs
    • Modélisation, solveurs SMT
    • Recherche de preuve, calcul des séquents du premier ordre

Pré-requis

formations/licences/ue/l3/lo5.txt · Dernière modification : 2023/09/05 10:09 de treinen