Logiques 
La logique propositionnelle et la logique du premier ordre en tant que langages de représentation des connaissances et de spécification, formalisation du raisonnement et des preuves, déduction naturelle.

Vérification et complexité 
Dans le cadre de la programmation impérative séquentielle, notion d’invariant et variant de boucle, correction partielle, terminaison, correction totale et complexité des programmes. Preuves de correction partielle, terminaison et complexité de programmes.