Introduction

Les mathématiciens ont raisonné correctement durant des siècles sans connaître la logique formelle. La logique moderne est née de l'ambition de formaliser (mécaniser) le raisonnement mathématique : ce projet a reçu une impulsion décisive quand il est apparu que l'absence de formalisation pouvait conduire à des contradictions. Le développement actuel de la logique continue avec

• le besoin de prouver la correction des programmes (particulièrement quand ces programmes sont utilisés dans des domaines où la sécurité est en jeu)
• l'ambition de représenter en machine l'ensemble des connaissances mathématiques

Cependant la terminologie des mathématiciens est restée différente de celle des logiciens. Pour exprimer que p implique q, le mathématicien dira par exemple :

p entraîne q

p est une condition suffisante de q

pour que q soit vrai, il suffit que p soit vrai

q est une condition nécessaire de p

pour que p soit vrai, il faut que q soit vrai

Nous restreindrons notre étude à la logique classique (par opposition à la logique intuitionniste). La logique classique est la logique à deux valeurs de vérité. De plus cette logique est celle des circuits combinatoires, ce qui explique sa grande importance pratique.

Plan :

Nous présentons dans la première partie la logique propositionnelle. Plus précisément dans un premier chapitre nous donnons les définitions et résultats de base de la logique des prédicats. Dans le second chapitre nous parlons de la résolution propositionnelle en introduisant la résolution binaire, la stratégie complète et l'algorithme DPLL. Enfin nous illustrons une méthode de raisonnement logique en présentant la déduction naturelle. Dans le seconde partie du cours nous revisitons l'ensemble des notions, résultats et techniques présentés dans la première partie pour la logique du premier ordre.

Exercices :

Nous proposons à la fin de chaque chapitre une série d'exercices portant sur le contenu du chapitre. Nous indiquons par des étoiles la difficulté des exercices proposés, plus il y a d'étoiles plus l'exercice est difficile. Nous indiquons par les exercices qui complètent les preuves vues durant le cours. Les exercices proposés sont de trois catégories. Nous avons des exercices:

• Basiques qui aident l'étudiant à se familiariser avec le vocabulaire et à manipuler les notions introduites en cours.
• Techniques qui sont des applications directes ou immédiates des résultats vus en cours.
• Réflexifs qui permettent à l'apprenant à raisonner, démontrer, prouver des résultats à partir des techniques et notions apprises grâce aux deux autres types d'exercices.

Objectifs :

Les compétences et connaissances que nous souhaitons transmettre sont les suivantes :

• Comprendre un raisonnement : être capable de déterminer si un raisonnement logique est correct ou non.
• Raisonner, c'est-à-dire, construire un raisonnement correct utilisant les outils de la logique propositionnelle et du premier ordre.
• Modéliser et formaliser un problème.
• Écrire une preuve rigoureuse.