Ce cours est une introduction à la logique et à la preuve. La logique a de multiples applications: bases de données, programmation, intelligence artificelle, preuve automatique ou assistée par ordinateur, etc. Le cours présente plusieurs techniques de preuve standard (implication, contraposée, contradiction, équivalence, récurrence, etc) et avancées (induction structurelle, ensembles bien fondés, machines à états et invariants, preuve de programmes.)