Introduit la résolution de théories modulo de satisfaction (SMT), couvrant la logique propositionnelle, les fonctions non interprétées et l'instanciation de quantificateur.
Explore les techniques d'induction dans les résolveurs SMT, en mettant l'accent sur l'implémentation de CVC4 et la performance compétitive avec d'autres proverbes.
Explore le problème de satisfabilité booléenne et l'algorithme Davis-Putnam-Logemann-Loveland, ainsi que les résolveurs SAT modernes et les techniques de résolution efficaces.
