Couvre la logique de premier ordre, les preuves de résolution, les fonctions Skolem et la vérification de la satisfaction en mathématiques et la vérification de programme.
Introduit des preuves informelles et leurs applications pratiques en informatique et en mathématiques, en soulignant l'importance de prouver des théorèmes par des méthodes directes et indirectes.