Présentation des méthodes de résolution de problèmes complexes

Dans certains domaines, ou devrais-je dire dans presque tous les domaines, on est parfois amené à vouloir trouver des théorèmes, ou des solutions, en partant d’une base de connaissances. Cette base de connaissance, ces choses prouvées, s’appelle dans le domaine la base de faits.

Exemple en médecine, on connaît les symptômes d’un patient, et on sait également des tas d’autres facteurs : catégorie du sang, allergies connues, anomalies à certains organes … etc. D’après tous ces faits, on peut établir une base de faits. Et de déduction en déduction, on arrive à une conclusion. Le patient x est atteint de la maladie y.

Note : Les clauses finales se nomment les clauses de Horn, ce sont les choses que l’on a démontrées.

C’est dans ce but qu’existe les différents types de résolution de problèmes que nous allons survoler. Les trois méthodes de résolutions que je vais étudier ici seront la résolution de Herbrand, le chaînage avant et le chaînage arrière.

Généralités : mise sous forme logique

Tout d’abord, il faut savoir que nous allons travailler seulement avec de la logique du premier ordre, c’est à dire qu’on ne peut pas « imbriquer » les règles dans d’autres règles.

En premier lieu, on doit modéliser notre problème en logique des prédicats du premier ordre. En admettant le problème suivant :

  1. Tous les apprentis aiment les grandes vacances
  2. Tous ceux qui aiment les grandes vacances aiment toutes les plages
  3. Copacabana est une plage, et Copacabana est très animée
  4. Tout ce qui est très animé est un lieu branché ou est une cour de récréation
  5. Aucune plage n’est une cour de récréation
  6. Jim n’aime aucun lieu branché
  7. Jim n’est pas un apprenti

Admettons les prédicats suivants :

  • app(x) : x est un apprenti
  • aime(x,y) : x aime y
  • pla(x) : x est une plage
  • ani(x) : x est très animé
  • bra(x) : x est un lieu branché
  • rec(x) : x est une cour de récréation

Les constantes qu’on utilisera seront les suivantes : LGV (les grandes vacances), C (Copacabana) et J (Jim).

Notes : ^ représente le ET dans les expressions et ∨ représente le OU. Le symbole ¬ représente la négation.

Pour établir nos règles logiques, on va utiliser des quantificateurs universels (∀) et existentiels (∃). Ces deux quantificateurs signifient en « français » respectivement « quel que soit/ pour tout » et « pour au moins un »

  1. (∀x)(app(x) -> aime(x, LGV)) : on peut traduire ceci par : (pour tout x)(si x est un apprenti, alors x aime les grandes vacances), on a représenté simplement la règle n°1 de notre base de faits.
  2. (∀x)(∀y)(aime(x, LGV) ^ pla(y) -> aime(x,y)) : (pour tout x et tout y)(si x aime les grandes vacances et que y est une plage, alors x aime y)
  3. pla(C) ^ ani(C) : ici on a pas de variables, on annonce simplement que Copacabana est une plage et est animée.
  4. (∀x)(ani(x) -> bra(x) ∨ rec(x)) : (pour tout x)(si x est un lieu animé, alors c’est soit un lieu branché soit une cours de récréation)
  5. (∀x)(pla(x) -> ¬rec(x)) : pour tout x, si x est une plage alors x n’est pas une cours de récréation. On peut aussi l’écrire ¬(∃x)(pla(x)∧rec(x))), ce qui veut dire : (pour tout sauf x)(x est une plage et x est une cours de récréation).
  6. (∀x)(bra(x) -> ¬aime(J,x)) : pour tout x, si x est un lieu branché alors Jim n’aime pas x.
  7. ¬app(J) : Jim n’est pas un apprenti

On retrouve ici toutes nos règles sous forme logique. Maintenant il va falloir trouver la pile de résolution, de façon à pouvoir appliquer notre méthode de résolution.

Généralités : pile de résolution

Nous allons passer par 6 étapes pour obtenir notre pile de résolution. Chaque règle précédemment trouvée (de 1 à 7), devra donc être normalisée sous forme conjonctive via ces 6 étapes.

Je vais tout d’abord expliquer les 6 étapes avec un exemple différent de celui pris avant : car les exemples sont trop simplistes pour qu’on puisse tous leur appliquer ces étapes.

Soit la règle logique suivante : E = (∀x) (p(x) -> ( (∃y) (p(y) ∨ ¬R(a,x,y) ) -> ( (∀z) (¬S(y,z) ) ) )  : c’est un peu plus costaud que ce qu’on a vu avant.

Etape 1 : Mise sous forme prénexe

Il faut faire passer tous les quantificateurs à gauche (Attention, il n y a pas de commutativité). On renommera également les variables quantifiées si nécessaire.

Dans notre exemple cela donne : (∀x) (∃y) (∀z) (p(x) -> (  (p(y) ∨ ¬R(a,x,y) ) -> ( (¬S(y,z) ) ) )

Etape 2 : Elimination des quantificateurs existentiels (Skolémisation)

[To be continued]

Résolution de Herbrand

 

Laisser un commentaire