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 :