Différences

Ci-dessous, les différences entre deux révisions de la page.

@@ Ligne 1: / Ligne 1: @@
+====== 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:ol3|Outils Logiques du L2]]
+  * Cours [[pf5|Programmation Fonctionnelle du L3]]

Outils pour utilisateurs

Outils du site

Différences

Outils de la page