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.

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

• Cours Outils Logiques du L2
• Cours Programmation Fonctionnelle du L3