====== 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 [[pf5|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 [[bd6|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 :

  - 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
  - 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 =====

  * Cours [[..:l2:ol4|Outils Logiques du L2]]
  * Cours [[pf5|Programmation Fonctionnelle du L3]]