Ce cours propose une introduction à la logique mathématique et ses liens avec l'’informatique.
L'’objectif est de décrire aussi bien la sémantique que la théorie des preuves de différentes logiques.
Le cours commencera par présenter la logique classique propositionnelle et du premier ordre : sémantique, systèmes de déduction (système de Hilbert, déduction naturelle, calcul des séquents LK), théorèmes d’'adéquation et de complétude, théorème de compacité, théorème d'’élimination des coupures.

Il donnera une introduction aux méthodes et outils de démonstration automatiques (Algorithme de Davis-Putnam-Logemann-Loveland, solveurs SAT, Skolémisation, Unification, Résolution).
Il décrira ensuite la logique intuitionniste :calcul des séquents LJ. Traduction de la logique classique vers la logique intuitionniste.
Enfin, une introduction à la logique linéaire sera proposée : sémantique des phases et sémantique des espaces cohérents, calcul des séquents et réseaux de preuves.