Cette séance de cours couvre l'encodage des systèmes de transition finis en utilisant des fonctions booléennes, la logique propositionnelle, l'interprétation de la vérité en Scala, les problèmes de satisfaction et la représentation des fonctions booléennes avec des circuits. Il traite également de lélimination des variables dans les formules propositionnelles et les concepts de variables libres, de validité, déquivalence et de QBFs.