Séance de cours
Cette séance de cours traite de l'exhaustivité d'un système de preuve en logique propositionnelle classique, en se concentrant sur la dérivation de toutes les tautologies propositionnelles. Il explore la solidité et la réfutation des théorèmes de complétude, la résolution sur les clauses, la forme conjonctive, les littéraux et les clauses, ainsi que la résolution unitaire et la transformation des formules en forme normale conjonctive. La séance de cours couvre également la transformation de Tseytin, les solveurs SAT, l'algorithme DPLL, les structures de données dans un solveur SAT et la génération de preuves simples à partir des exécutions de solveurs SAT.