Ce livre est une synthèse des cours de logique de licence et maîtrise des auteurs à l’université de Savoie. Il s’adresse donc tout particulièrement aux étudiants qui préparent le CAPES et l’Agrégation, mais aussi aux étudiants de certains DESS.

La première partie (chapitre 1 à 3) présente la logique comme un outil pour répondre en mathématiciens aux questions « qu’est-ce qu’un énoncé, une formule ? », « qu’est-ce qu’une démonstration, une preuve ? », « quelles en sont les règles ? ». Les points de vue syntaxique et sémantique (étude de la « vérité » d’une formule) sont abordés. Les exemples sont issus de théories mathématiques courantes (arithmétique, théorie des ensembles).
La deuxième partie (chapitre 4 à 6) commence par la présentation (syntaxe et sémantique de Kripke) de la logique intuitionniste ; l’intérêt de cette logique réside dans le fait de donner des preuves constructives, ce qui est essentiel en informatique. En effet « Preuves vs Programmes » est un domaine très actif de recherche, d’où un chapitre consacré au calcul des séquents et aux logiques d’ordre supérieur qui constituent la base de la plupart des logiciels d’aide à la démonstration.
Le dernier chapitre est consacré aux techniques de base de la démonstration automatique. Enfin, l’annexe présente le logiciel Phox qui est un assistant de preuves développé par les auteurs.
Cet ouvrage en français rassemble en quelques chapitres les notions fondamentales de la logique classique à la logique pour l’informatique, jusque là difficilement accessibles.