Démontrer automatiquement des petits théorèmes, mini-Prolog

David Monniaux



Le projet dispose d'une page de suivi à l'URL :

Consultez-la !


Qui, essayant de démontrer un théorème mathématique, n'a jamais eu recours à la technique d'essayer d'appliquer tous les théorèmes ayant la bonne conclusion ? Il s'agit ici de faire un mini-prouveur de théorèmes se basant sur ce principe, appliqué selon la méthode dite de résolution.

1  Définitions et exemples

1.1  Définitions

On dispose d'un certain nombre de règles de déduction ou axiomes de la forme :
x1x2 ... ∀ xn  H1
t11(x1, ..., xn), ..., t1o1(x1, ..., xn)
∧ ... ∧ Hm
tm1(x1, ..., xn), ..., tmom(x1, ..., xn)
C
t1(x1, ..., xn), ..., to(x1, ..., xn)
    (1)


Les Hi sont les hypothèses de la règle, C est la conclusion. Il n'est pas obligatoire que chacune des variables xj interviennent dans toutes les hypothèses et dans la conclusion. L'ensemble des hypothèses peut être vide.

Les ti sont des termes. Un terme désigne soit une variable, soit l'application d'un symbole de fonction à des termes. Nous ne chercherons pas à attacher un sens aux symboles de fonctions et aux termes, il suffira donc de les traiter comme des entités syntaxiques formelles. Une fonction avec zéro paramètres est une constante.

1.2  Exemple : monoïdes

La théorie des monoïdes (version simplifiée des groupes, sans inverse; par exemple, le monoïde (,+) des entiers naturels) s'exprime par les axiomes :
x  x = x.e         (2)
x  x = e.x         (3)
x1y1x2y2  x1=x2y1=y2x1.y1 = x2.y2         (4)
xyz  (x.y).z = x.(y.z)         (5)
x  x=x         (6)
xy  y=xx=y         (7)
xyz  x=yy=zx=z         (8)
e est l'élément neutre, . l'opération. Remarquons que les symboles =, e et . n'ont pas de sens particulier : il s'agit juste d'entités syntaxiques.

Pour une meilleure compréhension, pensons en termes d'entiers naturels. 2 + (3 + 5) et 10 sont deux termes syntaxiquement différents. Toutefois, on peut définir une relation = (l'égalité au sens mathématique sur les entiers représentés par ces termes) sur ces termes, qui est une relation d'équivalence compatible avec l'opération + : par exemple, puisque 2 + (3 + 5) = 10, alors (2 + (3 + 5)) + 6 = 10 + 6.

Nous traduisons ces formules en forme préfixe, afin d'avoir une syntaxe proche du langage Prolog. P1 ∧ ... PnP est remplacé par P :- P1, ..., Pn.
egal(X, mul(X, e)).
egal(X, mul(e, X)).
egal(mul(X1, Y1), mul(X2, Y2)) :- egal(X1, X2), egal(Y1, Y2).
egal(mul(mul(X, Y), Z), mul(X, mul(Y, Z))).
egal(X, X).
egal(X, Y) :- egal(Y, X).
egal(X, Z) :- egal(X, Y), egal(Y, Z).

1.3  Exemple : relations familiales

Suivant la même syntaxe, quelques données sur les derniers rois de France Valois et le premier roi Bourbon (Henri IV).
homme(X) :- estLePereDe(X, Y).
femme(X) :- estLaMereDe(X, Y).

estParentDe(X, Y) :- estLePereDe(X, Y).
estParentDe(X, Y) :- estLaMereDe(X, Y).
estGrandMereDe(X, Z) :- estLaMereDe(X, Y), estParentDe(Y, Z).
estGrandPereDe(X, Z) :- estLePereDe(X, Y), estParentDe(Y, Z).
ontUnParentCommun(A, B) :- estParentDe(X, A), estParentDe(X, B).

aEteMarieA(X, Y) :- aEteLeMariDe(X, Y).
aEteMarieA(X, Y) :- aEteLeMariDe(Y, X).
homme(X) :- aEteLeMariDe(X, Y).
femme(X) :- aEteLeMariDe(Y, X).

estBeauFrereParAllianceDe(X, Z) :- aEteLeMariDe(X, Y), ontUnParentCommun(Y, Z).

estLePereDe(henri_II, francois_II).
estLePereDe(henri_II, charles_IX).
estLePereDe(henri_II, henri_III).
estLePereDe(henri_II, marguerite_de_Valois).
estLaMereDe(catherine_de_Medicis, francois_II).
estLaMereDe(catherine_de_Medicis, charles_IX).
estLaMereDe(catherine_de_Medicis, henri_III).
estLaMereDe(catherine_de_Medicis, marguerite_de_Valois).
homme(francois_II).
homme(charles_IX).
homme(henri_III).
femme(marguerite_de_Valois).

aEteLeMariDe(henri_IV, marguerite_de_Valois).

1.4  Clauses existentielles

Notre formalise ne permet pas de représenter directement des propriétés du type ∀ x ∃ y P(x,y). Il existe cependant une transformation simple, appelée skolémisation, qui permet de le faire. La propriété ci-dessus est équivalente à l'existence d'une fonction f telle que ∀ x  P(x, f(x)).

2  Résolution propositionnelle

Plaçons d'abord dans le cas où l'on ne fait pas intervenir de variables ni de termes : les règles de déduction sont alors de simples implications de la forme P1 ∧ ... ∧ PnP.

Étant donné un tel ensemble de règles, une démonstration d'une propriété P est un arbre de preuve de la forme :
(A)

    
(A1)

    
(A11)

         
P11
     ...     
(A1n1)

         
P1n1
    
P1
     ...     
(Am)

    
(Am1)

         
Pm1
     ...     
(Amnm)

         
Pmnm
    
Pn
    
P
    (9)
Chaque règle
(A)

     P1      ...      Pn     
P
se lit : P s'obtient par application de la règle A sur les hypothèses P1 à Pn.

Pour rechercher un tel arbre de preuve, on peut procéder ainsi : pour chaque règle
(A)

     P1      ...      Pn     
P
, on essaye de relancer récursivement le procédé pour démontrer les hypothèses P1 à Pn.

On peut également voir cela de la façon suivante : on considère le graphe orienté G dont les sommets sont des arbres de preuve éventuellement incomplets (i.e. on n'a pas démontré toutes les branches de l'arbres), et dont les arêtes π1 → π2 sont présentes si l'arbre π2 est égal à l'arbre π1 dans lequel on a remplacé une proposition P0 non démontrée par l'application d'une règle A de conclusion P0 et d'hypothèses P1 à Pn : autrement dit, on remplace une sous-branche de la forme
()

     ???     
P0
par un sous-arbre de la forme
()

    
()

     ???     
P1
     ...     
()

     ???     
Pn
    
P0
.

Le problème de savoir s'il existe une démonstration de P se résume donc à savoir s'il existe un chemin de l'arbre de preuve incomplet
()

P
à un arbre de preuve complet (qui constitue donc une démonstration de P).

Si l'ensemble des règles applicables est infini, ce graphe peut être infini. Les méthodes de parcours en profondeur et en largeur peuvent être utilisées pour trouver une solution : la méthode en profondeur peut être plus facile à implémenter, mais elle peut partir dans des branches de raisonnement stérile et ne pas découvrir une démonstration ; le parcours en largeur doit découvrir toutes les démonstrations possibles. Notons que dans les deux cas, s'il n'existe pas de preuve alors l'exploration peut ne pas terminer.

3  Unification

Nous utilisons en fait des règles quantifiées universellement, avec des termes en argument. Une règle R de la forme ∀ x1 ... ∀ xn P1(x1, ..., xn) ∧ ... ∧ Pm(x1, ..., xn) ⇒ P(x1, ..., xn) représente en fait une infinité de règles sans variables : R dans laquelle on a remplacé x1,...,xn par des termes quelconques. Cela justifie notre discussion de la recherche de preuves avec un nombre infini de règles.

La recherche d'une règle dont la conclusion correspond à la propriété P choisie est maintenant plus complexe. Par exemple, si l'on a une règle R de la forme Q(x, y, z) ⇒ P(x, S(y), T(z)) et qu'on cherche à démontrer ∃ abc P(S(a), b, c), on pourra appliquer R avec x=S(a), b=S(y), c=T(z) ; on devra donc ensuite démontrer l'hypothèse Q en tenant compte de ces choix.

Le processus par lequel on rapproche deux termes, ici P(x, S(y), T(z)) et P(S(a), b, c), en cherchant sous quelles conditions minimales sur les variables ces termes peuvent être syntaxiquement égaux s'appelle unification. Formellement parlant, un unificateur de deux termes t1 et t2 est une substitution associant un terme (avec variables) à chaque variable ; on note σ.t le résultat de la substitution dans t selon les règles de σ. Ce que l'on recherche, c'est un unificateur général, de telle sorte que tout autre unificateur qui convienne soit un cas particulier de cet unificateur général, c'est-à-dire qu'il se décompose en la composée σ1 ∘ σ2 de deux substitutions.

L'algorithme d'unification est simple. Prenons par exemple l'unification des deux termes P(x, S(y), T(z)) et P(S(a), b, c). Les symboles de tête coïncident (mais on n'aurait pas pu, par exemple, unifier P(x,y) et Q(x,y)); on peut donc continuer. On va unifier x et S(a) ; on met donc à jour σ en rajoutant la substitution xS(a). On passe ensuite à l'unification de S(y) et b ; on obtient alors bS(y).

Il convient cependant de faire attention au phénomène dit de capture des variables. Prenons par exemple une règle R : ∀ x P(x) ⇒ Q(x) ; nous cherchons à démontrer ∃ x Q(f(x)). Une approche naïve serait d'unifier Q(x) et Q(f(x)), et cela nous donne xf(x), ce qui est bizarre et même indésirable (voir plus loin). Notons que la règle R est strictement équivalente à la règle ∀ xP(x') ⇒ Q(x') par renommage des variables.1 Si on emploie cette règle, on obtient x' ↦ f(x), ce qui est raisonnable. Il convient donc, avant d'essayer d'appliquer une règle, de renommer les variables de cette règle en des noms frais (non déjà utilisés).

Un autre problème est celui du test d'occurrence ( occur-check). Nous ne désirons pas avoir des solutions comme xf(x), c'est-à-dire des solutions où une variable intervient dans sa propre définition. Prenons un exemple simple pour voir en quoi ceci est indésirable : supposons que nous ayons une règle ∀ x P(S(x)) ⇒ P(x), une formalisation d'une propriété P sur les entiers naturels telle que ∀ n  P(n+1) ⇒ P(n). Une solution de la forme x = S(x) donnerait n=n+1, une solution absurde. En fait, si notre seule hypothèse est ∀ n  P(n+1) ⇒ P(n), nous ne pouvons pas démontrer P(0). En conséquence, il devra y avoir un test pour que la définition d'une variable dans une substitution ne fasse pas intervenir cette même variable.

4  Syntaxe et utilisation

Nous avons proposé ci-dessus des exemples écrits dans une syntaxe proche de celle du langage Prolog. Ces exemples sont une succession de trois types de commandes : En réponse à une requête P : Ainsi, sur l'exemple familial ci-dessus, la requête
?- estBeauFrereParAllianceDe(henri_IV, X).
va produire les solutions :
{
  X -> francois_II()
}
{
  X -> charles_IX()
}
{
  X -> henri_III()
}
{
  X -> marguerite_de_Valois()
}
Remarquons qu'il y a une faiblesse dans la définition de frère et soeur : une personne est considérée comme son propre frère (ou sa propre soeur). L'ajout et l'utilisation d'une propriété different et d'axiomes different(x, y) pour toute paire de personnes différentes est laissé comme exercice au lecteur.

Il n'est pas demandé de faire un algorithme optimisé. Il existe cependant un grand nombre d'optimisations possibles : simplification des unificateurs ; si pour démontrer une propriété P, on demande de démontrer la même propriété ou une propriété essentiellement isomorphe, alors on arrête dans cette voie ; etc. Remarquons que certaines règles peuvent provoquer de tels problèmes : il s'agit notamment des règles d'associativité et de commutativité.


1
On appelle parfois ce renommage α-conversion.

Ce document a été traduit de LATEX par HEVEA