EPITA

Introduction à Prolog, cours n° 3

Jean-François Perrot

La résolution dans le cas propositionnel


  1. Forme clausale
    1. Forme clausale
      1. Notion de clause : définition
      2. Notion de clause : interprétation
      3. Forme clausale
      4. Forme clausale réduite et algorithme de Wang
    2. Forme clausale et preuve par réfutation
      1. Réfutation
      2. Exemple simple
      3. Retour à Prolog

  2. La résolution
    1. L'opération de base : la réduction
    2. Résolvante
    3. Exemples

  3. La résolution propositionnelle linéaire
    1. Principe
    2. La résolution propositionnelle SLD pour les clauses de Horn
    3. La résolution simplifiée à la Prolog


Pour la réalisation en Prolog de tout ce discours, voir ici.

Forme clausale

  1. Forme clausale

  2. Forme clausale et preuve par réfutation

La résolution

  1. L'opération de base : la réduction

    Étant donné deux clauses différentes A et B contenant des littéraux de signes opposés,
    c'est-à-dire que A contient le littéral positif a, et B le littéral opposé ¬a ou vice-versa,
    l'opération de réduction consiste à construire une troisième clause C en réunissant
    (ou vice-versa).

    En somme, les deux littéraux opposés s'éliminent l'un l'autre...
    La clause C ainsi construite s'appelle une résolvante de A et B.

    Par exemple : A = (¬r ⋁ s) et B = (¬t ⋁ ¬s),  en prenant a = s,
    on construit C = (¬r ⋁ ¬t).

  2. Résolvante

    (terme emprunté à la tradition des algébristes : résolution des équations...)

    La propriété essentielle d'une résolvante quelconque R de deux clauses A et B  est l'implication
    A⋀ B ⊃ R.

    En effet, vu que les deux littéraux opposés a et ¬a ne peuvent être vrais en même temps, 
    la conjonction du membre gauche ne peut être vraie que si "les restes de chaque clause" sont simultanément vrais,
    ce qui entraîne a fortiori que leur disjonction, qui compose la clause R, soit vraie.

    Dans notre exemple il s'agit de ¬r et ¬t.
    Le même exemple montre que l'implication A⋀ B ⊃ R n'est pas une équivalence !
    La résolvante R peut être vraie sans que la conjonction A⋀ B le soit.

    Cette implication a pour conséquence que si R est vide, donc fausse,
    alors nécessairement A et B sont incompatibles.

    Attention ! Il est essentiel de supposer que les deux clauses A et B sont différentes,
    sans quoi on tirerait une résolvante vide de la clause tautologique (¬a ⋁ a) résolue contre elle-même !

    La stratégie de réfutation par résolution va donc consister en la recherche d'une résolvante vide
    en répétant les opérations de réduction à partir du système de clauses initial.

  3. Exemples

    1. La négation de la proposition "[(p ⊃ q) ⋀ (q ⊃ r) ⋀ (r⊃ s) ⋀ (t ⊃ ¬s)] ⊃ (p ⊃ ¬t)"

      en forme clausale "(¬p ⋁ q) ⋀  (¬q ⋁ r) ⋀ (¬r ⋁ s) ⋀ (¬t ⋁ ¬s) ⋀ p ⋀ t"
                    ---------------------                     |                       |                |
                                            (¬p ⋁ r)                  |           |       |
                         ---------------------------           |       |
                                      (¬p ⋁ s)                       |       |
                                -------------------------------        |
                                                  (¬p ⋁ ¬t)                  |
                                            ----------------------------
                                                              (¬t ⋁ ¬t) 
                                                        ---------
                                                            ()
    2. La girafe
      "(¬herbivore ⋁ girafe ⋁ buffle⋁ antilope) ⋀
      (¬herbivore ⋁ ¬félin) ⋀ ( ¬ panthère ⋁ félin ) ⋀
      (¬tacheté ⋁ panthère ⋁ girafe ) ⋀ herbivore ⋀ tacheté ⋀ ¬girafe      "

      ou pour abréger
      "(¬h ⋁ g ⋁ b ⋁ a) ⋀ (¬h ⋁ ¬f) ⋀ (¬p ⋁ f) ⋀ (¬t ⋁ p ⋁ g) ⋀ h ⋀ t ⋀ ¬g"
      -----------------                                          --        |
              |                                                   |        |
              -----------------------------------------------------        |
                                 (g ⋁ b ⋁ a)                               |
                                 ------------------------------------------
                                                   (b ⋁ a)  

      Cette tentative n'aboutit pas (aucun moyen d'éliminer a et b). Essayons autre chose.

      (¬h ⋁ g ⋁ b ⋁ a) ⋀ (¬h ⋁ ¬f) ⋀ (¬p ⋁ f) ⋀ (¬t ⋁ p ⋁ g) ⋀ h ⋀ t ⋀ ¬g
                          -------------------                |  |   |     |
                              (¬h ⋁ ¬p)                      |  |   |     |
                              -------------------------------   |   |     |
                                     (¬h ⋁ ¬t ⋁ g)              |   |     |
                                     ----------------------------   |     |
                                               (¬t ⋁ g)             |     |
                                               ----------------------     |
                                                      ( g )               |
                                                      --------------------
                                                               ()
      Et si on remplaçait la conclusion girafe par panthère ?
      On voit que la seule façon d'éliminer panthère va faire apparaître girafe dans la résolvante,
      qui restera indélébile...

La résolution propositionnelle linéaire

  1. Principe

    Comme on l'imagine, le processus de résolution exhaustif, tel que nous l'avons défini, est extrêmement coûteux,
    puisque le but poursuivi n'est pas de construire toutes les résolvantes, mais
    Depuis l'invention de la règle de résolution en 1965, la recherche s'est orientée vers l'élaboration de stratégies efficaces.
    La principale de ces stratégies est la résolution linéaire.
    Son principe est que l'une des deux clauses qu'on tente de réduire à chaque étape est la résolvante produite à l'étape précédente. .

    Les deux exemples de résolution que nous avons vus plus haut étaient l'un et l'autre linéaires.
    Le second montre que le choix de la clause choisie pour lancer le processus peut être décisif,
    et qu'on doit parfois le remettre en question par un retour en arrière.

  2. La résolution propositionnelle SLD pour les clauses de Horn

    C'est une réalisation de la résolution linéaire dans le cas restreint où
    Or la résolution linéaire à partir de cette clause négative donne à chaque pas
    une résolvante courante qui reste négative     (c'est la liste de buts courante).

    Ainsi dans notre processus il y a à chaque pas une seule clause négative à gérer,
    qui est connue par sa localisation.

    Le seul degré de liberté est le choix de la construction de la résolvante,
    qui doit réaliser la réunion des listes d'atomes (littéraux négatifs) SButs et de la queue de clause Q.
    La stratégie Prolog de recherche en profondeur (la résolvante étant gérée comme une pile)
    se traduit par union = append et elle entraîne des bouclages intempestifs.
    La méthode correcte est de faire une union sans  duplication.

  3. La résolution simplifiée à la Prolog

    L'interprète Prolog gère la résolvante comme une pile, et ne mémorise pas les résolvantes précédentes,
    d'où un programme beaucoup plus simple, mais qui a une forte tendance a boucler,