Mathématiques pour l’Informatique 2

Introduction

Objectifs

• Raisonner sur des structures utiles en informatique :
  • graphes, séquences, arbres, ordres
• Savoir utiliser le calcul propositionnel :
  • système de déduction, modèle, représentation des connaissances

Plan

1. Rappels : logique, formalisation en théorie des ensembles
2. Graphes
3. Inférence, induction et récursion
4. Structures séquentielles, arbres
5. Ordres
6. Algèbre de Boole
7. Calcul Propositionnel

Préambule

Les mathématiques sont une science qui s’intéresse à établir des propriétés d’objets abstraits. Il y a plusieurs activités :

• définir les bons objets abstraits sur lesquels raisonner, faire le lien avec les problèmes concrets;
• énoncer des propriétés intéressantes à étudier (générales, pertinentes);
• démontrer des théorèmes c’est-à-dire construire un enchainement de raisonnements élémentaires qui garantissent que si certaines hypothèses sont satisfaites alors la propriété sera vérifiée.

L’activité mathématique passe par l’utilisation d’un langage commun spécifique afin d’éviter les ambiguités du langage naturel. Dans ce langage, on distingue une partie qui sert à décrire les objets, les mathématiciens utilisent courament le langage de la théorie des ensembles et une partie qui sert à décrire les enchainements logiques corrects en utilisant les connecteurs logiques.

Utiliser un langage précis permet également de faire faire des preuves à des machines. Dans ce cours nous aborderons deux classes d’outils. Nous utiliserons en TP un assistant de preuve (Coq) qui propose un langage puissant mais laisse à l’utilisateur la responsabilité d’indiquer les étapes de la preuve, l’ordinateur ne fait que vérifier que le raisonnement est correct. Nous étudierons dans le cours le calcul propositionnel et montrerons comment utiliser l’ordinateur pour démontrer automatiquement ces formules.

1  Le cadre logique

La logique définit les règles formelles que doit respecter tout raisonnement correct. La notion de preuve est essentielle en mathématiques et plus généralement dans toutes les activités scientifiques. Il ne s’agit pas juste de déterminer ce qui est vrai ou faux mais d’être capable de donner des explications qui justifient que le résultat annoncé est valide. Il y a donc des règles du jeu à suivre qui doivent être assez simples pour que chacun puisse se convaincre qu’il n’y a pas tricherie.

Il est important de bien comprendre la structure des énoncés mathématiques et des preuves afin de mieux les maitriser et de faire moins d’erreurs dans leur utilisation générale.

Cette partie du cours reprend des éléments vus dans le cours de Mathématiques pour l’Informatique 1 du premier semestre.

1.1  Formules

La première étape consiste à introduire des notations rigoureuses et standardisées pour représenter des énoncés. On parle de langage formel. Les informaticiens sont particulièrement sensibles à cet aspect car c’est une étape essentielle pour que les ordinateurs puissent manipuler de manière pertinente de tels objets.

Une formule décrit une propriété (vraie ou fausse) d’objets (par exemple des entiers, mais aussi des ensembles, des fonctions …). Pour décrire les objets, on dispose de constantes comme 0, 1, ∅…, d’opérations comme +, ×, ∪. Une opération s’applique à des objets pour former de nouveaux objets. Par exemple 3+2 est un objet qui est obtenu en appliquant l’opération + aux deux constantes 3 et 2. Chaque opération s’applique à un nombre fixe d’objets, par exemple 3+2 représente un objet mais 3+ ne représente rien.

On utilise également des variables qui sont des symboles permettant de représenter des objets arbitraires comme par exemple dans l’objet x+1.

Les formules atomiques incluent ⊤ (la propriété vraie) et ⊥ (la propriété fausse). On peut aussi introduire des symboles de prédicat comme l’égalité =, la comparaison ≤, l’appartenance ∈ et l’inclusion ⊆. Un symbole de prédicat associé à un ou plusieurs objets est une formule atomique.

Les formules composées se construisent à l’aide de connecteurs logiques. On distingue la partie dite propositionnelle :

• ¬ P la négation d’une formule (non P)
• P ∧ Q la conjonction de deux formules (P et Q)
• P ∨ Q la disjonction de deux formules (P ou Q)
• P ⇒ Q l’implication de deux formules (P implique Q, ou encore si P alors Q)
• P ⇔ Q l’équivalence de deux formules (P si et seulement si Q, ou encore P est équivalent à Q)

Et les quantificateurs du premier ordre :

• ∀ x, P la quantification universelle (pour tout x, P)
• ∃ x, P la quantification existentielle (il existe x tel que P)

Notations, règles de parenthésage.

On peut introduire plusieurs variables dans un quantificateur, par exemple : ∀ x  y, P représente la formule ∀ x, ∀ y, P.

Comme pour les formules arithmétiques, il y a des règles de précédence pour les connecteurs logiques qui évitent l’utilisation des parenthèses. La précédence de ¬ est la plus forte, vient ensuite la conjonction ∧ puis la disjonction ∨ et finalement l’implication ⇒. Ces connecteurs associent à droite. On écrira par exemple A ⇒ B ⇒ C à la place de A ⇒ (B ⇒ C).

Dans ce cours, les quantificateurs ∀ et ∃ ont une précédence plus faible que les autres opérateurs. Leur portée s’étend donc aussi loin que possible.

1.2  Formule vraie

Pour définir quand une formule est vraie, il faut se placer dans un modèle qui explicite de quels objets on parle et également pour chaque symbole de prédicat, nous dit pour quels objets il est vérifié.

Par exemple 2 ≤ 4 est vrai mais 0=1 est faux.

Certaines propriétés peuvent être vraies dans un modèle et fausses dans un autre, par exemple ∀ x, x < 2 ⇒ x ≤ 1 est vrai si on considère les entiers mais faux si on s’intéresse aux rationnels.

Une fois que l’on connait quelles formules atomiques sont vérifiées, on peut définir quand une formule composée est vraie en fonction de la véracité des formules qui la composent. On utilise la valeur V pour une formule vraie et la valeur F pour une formule fausse.

Pour savoir si une formule propositionnelle est vraie, il “suffit” de la décomposer pour se ramener à la vérité des formules atomiques qui la composent.

Dans le cas où certains symboles de prédicats ne sont pas définis, ils sont vus comme des inconnus. On pourra s’intéresser à savoir si une formule est vraie pour toutes les interprétations possibles de ces prédicats (pour tous les modèles). Si c’est le cas on dira que la formule est valide ou encore que c’est une tautologie. Si la formule est vraie pour certaines interprétations, on dit que la formule est satisfiable, si elle est fausse dans toutes les interprétations alors elle est dite insatisfiable.

On peut faire le parallèle avec des identités remarquables en mathématiques (x+y)²=x²+2xy+y² est toujours vrai, x+y=3 est vrai pour certaines valeurs de x et de y, x+1=0 est toujours faux (sur les entiers naturels). Connaitre des formes standard de propriétés logiques toujours vraies ou toujours fausses permet de raisonner plus rapidement sans refaire de calculs.

1.3  Formule avec variable

Une formule logique peut contenir des variables qui représentent des objets arbitraires.

Une formule P avec variables représente un ensemble de formules closes obtenues en remplaçant les variables par des objets du modèle.

Par exemple x ≤ y est une formule avec deux variables x et y. Se poser la question de savoir si cette formule est vraie nécessite d’expliciter comment on traite les inconnues x et y.

Les variables représentent des objets arbitraires. On peut donc les remplacer dans une formule par d’autres objets (qui peuvent eux-mêmes contenir des variables). On notera P[x← t] la formule obtenue en remplaçant x par t dans P.

On ne peut pas dire a priori si une formule avec variables est vraie ou fausse. Il faut au préalable expliciter comment les variables sont interprétées. On pourra s’intéresser à s’il existe des objets pour lesquels la formule est vraie ou à une propriété plus forte qui dit que la formule est vraie quelle que soit la manière dont on remplace les variables.

Variables libres, liées.

Dans les formules ∀ x, P et ∃ x, P, la variable x est dite liée, en effet les occurrences de x sont reliées au quantificateur correspondant et on peut changer le nom de manière cohérente dans P et le quantificateur sans changer le sens de la formule:
∀ x, ∃ y, x < y exprime la même propriété que ∀ t, ∃ u, t < u. Une variable x qui apparait dans une formule P mais qui n’est pas dans une sous-expression de la forme ∀ x, Q ou ∃ x, Q est dite libre. Par exemple dans la formule ∃ y, x < y, la variable x est libre et y est liée.

La notion de variable libre et liée se retrouve également dans les programmes informatiques avec les paramètres des procédures et fonctions et les variables globales ou locales.

Validité.

La vérité d’une formule avec des variables libres, dépend de l’interprétation de ces variables qui est représentée par un environnement qui associe une valeur à chaque variable.

La vérité d’une formule avec des quantificateurs du premier ordre dépend en général de l’exploration de la vérité d’un ensemble infini de formules (obtenues en interprétant les variables par des objets en nombre potentiellement infini).

• La formule ∀ x,P est vraie dans un environnement ρ si et seulement si pour toute valeur t, la formule P est vraie dans l’environnement ρ étendu avec la variable x qui a pour valeur t.
• La formule ∃ x,P est vraie si et seulement si il existe un objet t tel que la formule P est vraie dans l’environnement ρ étendu avec la variable x qui a pour valeur t.

Définitions.

Il serait trop laborieux de devoir toujours revenir aux définitions de base, aussi on est amené en mathématiques à introduire des définitions. Une définition mathématique est juste l’introduction d’une abbréviation pour une certaine notion afin de pouvoir l’utiliser simplement. Ces notations dépendent souvent de paramètres qui pourront être remplacés par des valeurs arbitraires. Ainsi pour la parité d’un nombre, on peut introduire la notation

L’écriture pair(4) est juste un raccourci pour la formule ∃ y, 4=2× y (on a remplacé le paramètre x par la valeur 4) on peut de même écrire pair(3) qui représente la formule ∃ y, 3=2× y (une formule fausse sur les entiers) ou encore pair(2× x).

Si on veut exprimer une propriété comme la somme de deux entiers pairs est pair on pourra l’écrire :

Mais il faut faire attention lorsque l’on déplie la définition de pair(y) ou de pair(x+y) qu’on ne peut pas juste remplacer x par y car la variable y est utilisée comme variable liée dans la définition de pair(x). Le remplacement textuel donne ∃ y, y=2× y qui est une formule qui ne dépend plus de y et qui est toujours vrai (il suffit de choisir y=0). La bonne manière de procéder est de renommer la variable liée y dans la définition de pair(x) en un autre nom qui est différent des noms des variables libres. Le renommage des variables liées ne modifie pas le sens des formules

on peut ensuite procéder au remplacement textuel de x par y.

1.4  Formule démontrable

Plutôt que de calculer des valeurs de vérité (ce qui peut être très fastidieux, voir impossible), on peut formaliser des étapes de raisonnement qui nous permettent d’aller plus vite.

Par exemple un principe bien connu est le “modus ponens” : si on a établi d’un côté que P⇒ Q est vrai et de l’autre que P est vrai alors on peut en déduire que Q est vrai.

L’activité de preuve ne consiste pas juste à déterminer si un énoncé est vrai ou non, mais s’intéresse plutôt à des étapes de raisonnement qui à partir d’un certain nombre d’hypothèses (des énoncés qui sont supposés vrais), déduisent une conclusion (un autre énoncé) que l’on cherche à établir.

On peut ainsi avoir des principes de preuve plus élaborés. Par exemple si à partir d’une hypothèse ¬ H on est capable d’établir la propriété P mais aussi d’établir la proprété contraire ¬ P alors c’est qu’il y a une contradiction et donc que l’hypothèse ¬ H est fausse, cela permet de justifier que H est vrai (on a raisonné par l’absurde). Un autre exemple est si d’une hypothèse H on est capable d’établir la propriété P et à partir de l’hypothèse contraire ¬ H on est aussi capable d’établir la propriété P c’est que P est vrai sans aucune hypothèse (il s’agit d’un raisonnement par cas).

Pour établir la validité des formules, on va donc utiliser des systèmes de déduction qui permettent de déduire qu’une formule (la conclusion) est une conséquence logique d’un ensemble de formules (les hypothèses).

On écrit cette relation Γ ⊢ P avec Γ un ensemble de formules (que l’on pourra aussi écrire H₁,…,H_n en explicitant les formules) et P une formule. On appelle cet objet un séquent. Les formules de Γ sont appelées les hypothèses et la formule P est la conclusion du séquent.

L’interprétation de cette relation est que si on a pu établir Γ ⊢ P et si on se place dans un monde dans lequel les formules dans Γ sont vraies alors la formule P est également vraie dans ce monde.

1.4.1  Règles élémentaires

Il existe plusieurs systèmes de preuve, nous introduisons ici un système semi-formel qui s’inspire des calculs des séquents de Gentzen.

Ce système organise les étapes de raisonnement en deux catégories en fonction du connecteur principal d’une formule P. Les étapes d’introduction (à droite du signe ⊢) qui expliquent comment on peut établir une dérivation de Γ ⊢ P et des règles d’élimination d’hypothèses (à gauche du signe ⊢) qui expliquent comment on peut exploiter une propriété P qui apparait comme hypothèse.

Nous présentons ces règles logiques comme un système d’inférence. On se donne des briques élémentaires de la forme

dans lesquelles chaque Γ représente un ensemble de formules et chaque C représente une formule. On donne un nom à la règle pour pouvoir mieux l’identifier ensuite.

Dans la suite nous présentons chaque règle de preuve sous deux formes. La première forme est une règle d’inférence qui doit se lire de la façon suivante : si on a établi les séquents au dessus de la barre alors celui dessous la barre est également justifié. La seconde forme se rapproche de la manière dont on fait une démonstration avec un problème à résoudre et à chaque fois que l’on utilise une règle, soit on conclut la preuve, soit on se ramène à un ou plusieurs sous-problèmes qu’il suffit de résoudre pour justifier la correction du problème initial.

Règles de base.

Une première série de règles permet de terminer une preuve dans les cas “élémentaires”.

• Hypothèse : si la conclusion fait partie des hypothèses alors la preuve est terminée.

  (Hyp)

  Γ ⊢ A

  si A ∈ Γ

  Γ ⊢?  A  par   Hyp car A ∈ Γ

• Si la conclusion est une formule atomique qui est valide alors la preuve est terminée.

  (Ax)

  Γ ⊢ A

  si A formule atomique vraie

  Γ ⊢?  A  par   Ax car A formule atomique vraie

Règles (droites) d’introduction.

Les règles suivantes expliquent comment ramener la preuve d’une formule à des preuves de certaines de ses sous-formules. On les appelle des règles droites ou encore règles d’introduction :

• Si on veut prouver A∧ B alors on peut se ramener à démontrer d’une part la conclusion A d’autre part la conclusion B. Les hypothèses ne changent pas.

  (∧ I)

  Γ ⊢ A     Γ ⊢ B  Γ ⊢ A ∧ B

  Γ ⊢?  A ∧ B  par   ∧ I −Γ ⊢?  A −Γ ⊢?  B

• Si on veut montrer A∨ B alors on a deux possibilités : on peut se ramener à démontrer la conclusion A avec les mêmes hypothèses ou bien on peut se ramener à démontrer la conclusion B avec les mêmes hypothèses. Attention l’utilisation de l’une ou l’autre de ces règles peut ne pas aboutir car il y a des situations où A∨ B est vrai sans qu’on puisse conclure que A est vrai ou B est vrai … Par exemple, on peut déduire B∨ A à partir de l’hypothèse A∨ B mais à partir de l’hypothèse A∨ B, on ne peut déduire ni B ni A.

  (∨ I)

  Γ ⊢ A  Γ ⊢ A ∨ B

  (∨ I)

  Γ ⊢ B  Γ ⊢ A ∨ B

  Γ ⊢?  A ∨ B  par   ∨ I −Γ ⊢?  A

  Γ ⊢?  A ∨ B  par   ∨ I −Γ ⊢?  B

• Si on veut montrer ¬ A alors on peut se ramener à démontrer une contradiction en ajoutant la propriété A dans les hypothèses.

  (¬ I)

  Γ,A ⊢ ⊥  Γ ⊢ ¬ A

  Γ ⊢?  ¬ A  par   ¬ I −Γ,A ⊢?  ⊥

• Si on veut montrer A⇒ B alors on peut se ramener à démontrer la conclusion B en ajoutant la propriété A dans les hypothèses.

  (⇒ I)

  Γ,A ⊢ B  Γ ⊢ A⇒ B

  Γ ⊢?  A⇒ B  par   ⇒ I −Γ,A ⊢?  B

• Si on veut montrer ∀ x, P alors on se ramène à prouver P pour un x quelconque. La contrainte x quelconque impose que le nom x ne soit pas déjà utilisé ailleurs et donc qu’il ne soit pas libre dans les hypothèses. On peut toujours se ramener à ce cas là, car si x était utilisé dans les hypothèses, comme x est lié dans la formule ∀ x, P, on peut procéder à un renommage : on choisit un nom y qui n’apparaît pas par ailleurs, et on remplace ∀ x, P par ∀ y, P[x← y]

  (∀ I)

  Γ ⊢ P  Γ ⊢ ∀ x,P

  si x ∉Vl(Γ)

  Γ ⊢?  ∀ x,P  par   ∀ I car x ∉Vl(Γ) −Γ ⊢?  P

• Si on veut montrer ∃ x, P alors il suffit de produire un objet t, et on se ramène à prouver P[x← t]. Attention si on choisit mal l’objet t, on risque de se ramener à quelque chose qui n’est pas prouvable.

  (∃ I)

  Γ ⊢ P[x← t]  Γ ⊢ ∃ x, P

  Γ ⊢?  ∃ x, P  par   ∃ I −Γ ⊢?  P[x← t]

Ces règles sont suffisantes pour prouver les propriétés suivantes (sans hypothèses) :

• P ⇒ Q ⇒ P
• P ⇒ (P ∨ Q)

mais elles ne sont pas suffisantes pour montrer une propriété comme (P ∨ Q) ⇒ (¬ P ⇒ Q). En effet elles se contentent de traiter des connecteurs dans la conclusion, nous allons donner maintenant des règles qui permettent aussi de traiter des connecteurs dans les hypothèses.

Règles (gauche) d’élimination.

Les règles suivantes expliquent comment utiliser des connecteurs dans les hypothèses.

• Si l’absurde (une propriété toujours fausse) fait partie des hypothèses, alors on peut prouver n’importe quoi :

  (⊥ H)

  Γ,⊥ ⊢ C

  Γ,⊥ ⊢?  C  par   ⊥ H

• Si ¬ A est dans les hypothèses et que l’on sait aussi prouver A alors on a une contradiction et donc on peut prouver n’importe quoi:

  (¬ H)

  Γ,¬ A ⊢ A  Γ,¬ A ⊢ C

  Γ,¬ A ⊢?  C  par   ¬ H −Γ,¬ A ⊢?  A

• Si A ∧ B est dans les hypothèses alors on peut décomposer en deux hypothèses A et B:

  (∧ H)

  Γ,A,B ⊢ C  Γ,A∧ B ⊢ C

  Γ,A∧ B ⊢?  C  par   ∧ H Γ,A,B ⊢?  C

• Si A ∨ B est dans les hypothèses alors on peut raisonner par cas, en considérant deux instances de notre problème, l’un avec l’hypothèse A en plus et l’autre avec l’hypothèse B en plus:

  (∨ H)

  Γ,A ⊢ C      Γ,B ⊢ C  Γ,A∨ B ⊢ C

  Γ,A∨ B ⊢ C  par   ∨ H −Γ,A ⊢?  C −Γ,B ⊢ C

• Si A ⇒ B est dans les hypothèses et que l’on peut prouver A alors on peut ajouter B dans les hypothèses:

  (⇒ H)

  Γ,A⇒ B ⊢ A     Γ,B ⊢ C  Γ,A⇒ B ⊢ C

  Γ,A⇒ B ⊢?  C  par   ⇒ H −Γ,B ⊢?  C −Γ,A⇒ B ⊢?  A

• Si ∀ x,P, est une des hypothèses alors on peut ajouter dans les hypothèses des instances de P en remplaçant x par n’importe quel objet t :

  (∀ H)

  Γ,(∀ x,P),P[x← t] ⊢ C  Γ,(∀ x,P) ⊢ C

  Γ,(∀ x,P) ⊢?  C  par   ∀ H −Γ,(∀ x,P),P[x← t] ⊢?  C

• Si ∃ x,P est dans les hypothèses, alors on peut donner un nom à cet objet (que l’on ne connaît pas) et ajouter l’hypothèse que cet objet satisfait P. Comme on ne connaît rien de l’objet (sauf qu’il existe), le nom que l’on choisit doit être neuf et donc ne doit pas être déjà utilisé. Comme le nom x est lié dans ∃ x,P, on peut toujours procéder à un renommage ∃ y,P[x← y] pour choisir un nom nouveau.

  (∃ H)

  Γ,P ⊢ C  Γ,(∃ x,P) ⊢ C

  si x ∉Vl(Γ,C)

  Γ,(∃ x,P) ⊢?  C  par   ∃ H car x ∉Vl(Γ,C) − Γ,P ⊢?  C

Coupure.

Les règles précédentes permettent d’ajouter des nouvelles hypothèses mais qui sont en lien direct avec les hypothèses déjà présentes.

La règle de coupure consiste à ajouter librement une nouvelle hypothèse A, pourvu que par ailleurs on soit capable de prouver que A est vrai.

Cela correspond à utiliser dans une preuve un lemme qui est montré par ailleurs.

La forme de cette règle est :

Cette règle n’est pas essentielle dans le sens où il existe un théorème d’élimination des coupures qui dit que si on fait une preuve avec cette règle, alors il existe une preuve du même séquent qui n’utilise pas cette règle. C’est un résultat important pour la démonstration automatique, car si on se place du point de vue de la machine qui cherche à montrer Γ ⊢_?  B alors pour utiliser cette règle, il lui faudrait deviner la formule A.

Par contre du point de vue de l’humain, la preuve sans la règle de coupure peut être exponentiellement plus grande que la preuve qui utilise la règle de coupure. Cette dernière est donc essentielle pour obtenir des preuves “lisibles”.

Raisonnement par l’absurde.

Enfin, les règles précédentes ne suffisent pas à prouver toutes les formules valides, il faut y ajouter le schéma de raisonnement classique qui capture ce que l’on appelle le raisonnement par l’absurde. Si on veut prouver A alors on peut supposer ¬ A et en déduire une contradiction.

On peut résumer ces règles logiques dans le tableau suivant :

1.4.2  Règles dérivées

A partir des règles de base données précédemment, on peut déduire des règles avancées qui permettent de faire des preuves plus courtes.

Oublier des hypothèses.

On remarque que si une formule A est une conséquence d’hypothèses Γ alors a fortiori A est une conséquence d’un ensemble d’hypothèses Γ′ qui contient les hypothèses de Γ. Rajouter des hypothèses ne fait que rendre le problème plus facile à résoudre. C’est vrai pour la règle hypothèse, puis c’est préservé par toutes les règles.

Ce principe s’énonce ainsi : si Γ ⊢ A et Γ ⊆ Γ′ alors Γ′ ⊢ A. On peut aussi l’écrire sous forme de règle d’inférence :

On peut donc oublier des hypothèses inutiles lorsque l’on construit une preuve de bas en haut.

Règle de modus ponens.

La règle de modus ponens mentionnée précédemment peut se déduire des règles précédentes.

1.4.3  Théories

Un système de déduction doit également comporter des règles pour prouver les formules atomiques.

Egalité.

Une théorie importante est celle de l’égalité. Les règles pour l’égalité sont :

On retrouve ici aussi une règle d’introduction et une règle d’élimination d’hypothèse. La deuxième règle traduit le fait que si l’égalité t=u est vérifiée alors on peut remplacer t par u dans une formule quelconque sans en changer la vérité.

Dans le cas des entiers avec l’addition et l’égalité, on ajoutera des axiomes qui vont se comporter comme des hypothèses supplémentaires traitées de manière implicite (c’est-à-dire qu’on ne les écrit pas dans Γ). Les axiomes de Peano considèrent comme primitives la constante 0 et l’opération ajouter 1. L’addition entre deux entiers est caractérisée en fonction de la forme du premier argument suivant si c’est 0 ou un entier de la forme x+1. On peut aussi voir l’addition comme une opération de groupe avec des propriétés de commutativité et d’associativité Pour travailler avec uniquement des entiers, on peut se donner les hypothèses suivantes :

Preuve:

□

L’ensemble d’axiomes proposé précédemment pour raisonner sur les entiers naturels ne permet pas de prouver toutes les propriétés des entiers naturels. Par exemple la propriété ∀ x,x≠x+1 qui est vraie n’est pas démontrable. En effet on peut construire un modèle avec les entiers usuels plus un objet infini ∞ tel que ∞+1=∞. Toutes les règles logiques données pour les entiers sont vérifiées mais pas ∀ x,x≠x+1.

Il nous manque en particulier le principe de raisonnement par récurrence qui pourra s’écrire sous forme de règle d’inférence ou de raisonnement :

qui exprime qu’un entier est de la forme 0+1+⋯ +1.

1.5  Assistant de preuve

Des outils informatiques permettent de faire des preuves sur ordinateur.

1.5.1  Démonstration automatique

Certains outils font de la démonstration automatique, ils prennent en entrée un problème (par exemple sous la forme Γ ⊢ A) et se placent dans une certaine logique. Ils établissent si oui ou non le problème donné est valide (ou satisfiable) dans la logique.

Dans la pluspart des logiques un peu expressives, le problème est indécidable, c’est-à-dire qu’il n’existe pas de programme informatique qui répond exactement à la question. On peut avoir des programmes qui répondent partiellement, c’est-à-dire que dans certains cas, ils ne pourront pas dire si le problème est valide ou non.

Si on se place dans le fragment propositionnel (pas de quantificateurs) alors on peut savoir si une formule est satisfiable, valide ou non. Les SAT-solvers sont des outils qui permettent de traiter des problèmes propositionnels. L’idée est d’avoir des variables pour des propositions atomiques qui peuvent valoir vrai ou faux, puis de décrire un problème sous la forme de contraintes sur ces variables exprimées comme des formules propositionnelles. L’outil détermine s’il existe une manière d’affecter une valeur vrai ou faux à chaque variable propositionnelle qui rende le problème vrai.

Les SAT-solvers utilisent des algorithmes sophistiqués pour pouvoir traiter des formules avec un très grand nombre de variables propositionnelles.

Sur le problème du Sudoku, on voit qu’utiliser des formules du premier ordre avec des variables pour représenter les positions et les chiffres permet de factoriser la description. Au lieu des variables propositionnelles, on introduira un symbole de prédicat pos(i,j,k) qui sera vrai lorsque le chiffre k est à la position (i,j). D’autres fragments de logique sont décidables comme l’arithmétique linéaire (l’addition mais pas la multiplication). Cependant les procédures pour résoudre de tels problèmes ont une forte complexité.

Des outils comme les SAT-solvers sont utilisés pour vérifier des programmes, ou bien pour résoudre des problèmes de planification qui seront modélisés de manière logique.

1.5.2  Assistant de preuve

Si établir la vérité d’un problème Γ ⊢ A est complexe, il est par contre élémentaire de vérifier qu’une démonstration de ce même problème suit les règles de déduction de la logique. C’est ce que font les assistants de preuve. Ils proposent des environnements qui permettent de construire interactivement des preuves. L’utilisateur indique les étapes de démonstration et l’ordinateur maintient l’état du problème : ce qui a été démontré, ce qu’il reste à résoudre. On peut ainsi construire de grosse preuves en garantissant la correction du résultat. L’environnement peut également aider à construire des preuves complexes en introduisant des étapes de preuve qui correspondent à un enchainement de règles logiques élémentaires.

Dans les travaux pratiques de ce cours nous utiliserons l’assistant de preuve Coq. Cet outil est utilisé à la fois pour garantir la correction de programmes (sécurité de la plateforme JavaCard, preuve de compilateurs, algorithmes de calculs sur les flottants, cryptographie …), mais aussi pour des preuves mathématiques avancées (théorème des 4 couleurs, conjecture de Kepler, classification des groupes finis …).

Ce document a été traduit de L^AT_EX par H^EV^EA