Algorithmes de résolution en logique propositionnelle

1) Introduction

...

2) Définitions booléennes

La logique propositionnelle comprend des inconnues booléens `x,y,z,...` et des connecteurs booléens. La valeur logique vrai est notée `1`, la valeur logique faux est notée `0`. Les connecteurs booléens les plus utilisés sont `"¬", "∧","∨","→","↔"` et correspondent à des opérations booléennes défini comme suit :

Libellé	Connecteur	Table de vérité
Faux	`0`	`0`
Vrai	`1`	`1`
Négation	`"¬"a`	`"¬"0=1` `"¬"1=0`
Conjonction	`a"∧"b`	`0"∧"0=0` `0"∧"1=0` `1"∧"0=0` `1"∧"1=1`
Disjonction	`a"∨"b`	`0"∨"0=0` `0"∨"1=1` `1"∨"0=1` `1"∨"1=1`
Implication	`a"→"b`	`0"→"0=1` `0"→"1=1` `1"→"0=0` `1"→"1=1`
Équivalence	`a"↔"b`	`0"↔"0=1` `0"↔"1=0` `1"↔"0=0` `1"↔"1=1`

S'il y a `n` inconnus booléens `x_1,x_2,x_3,..., x_n` alors il y a `2^n` modèles envisageables (`2^n` combinaisons).

Etant donnée deux propositions `alpha, beta` érites dans ce langage `"<""¬", "∧","∨","→","↔",0,1,x_1,x_2,...,x_n">"`, l'implication sémantique `alpha |== beta` signifie que tout modèle qui réalise `alpha` réalise `beta`. Tandis que l'implication syntaxique `alpha |-- beta` signifie qu'il existe une démonstration de `beta` utilisant `alpha` comme hypothèse. En logique propositionnelle, et avec les règles de déduction naturel, nous avons la propriété de complétude qui dit que tout ce qui est vrai est démontrable, ou en d'autre terme que pour toutes propositions `alpha`, `beta`, si `alpha |== beta` alors `alpha |-- beta`. La réciproque étant évidente, les deux symboles ont alors la même signification. On utilise le symbole `|==` pour évoquer les modèles (combinaisons), et on utilise le symbole `|-` pour évoquer les démonstrations.

3) Règles booléennes

On remarque les règle de substitutions autorisée où `x, y, z` représente n'importes quelles propositions :

Commutativité de `∧`	`(x ∧ y) = (y ∧ x )`
Commutativité de `∨`	`(x ∨ y) = (y ∨ x)`
Associativité de `∧`	`((x ∧ y) ∧ z) = (x ∧ (y ∧ z)) `
Associativité de `∨`	`((x ∨ y) ∨ z) = (x ∨ (y ∨ z)) `
Élimination de la double négation	`¬(¬x) = x`
Contraposition	`(x ⇒ y) = (¬y ⇒ ¬x) `
Élimination de l’implication	`(x ⇒ y) = (¬x ∨ y) `
Élimination de l'équivalence	`x ⇔ y = ((x ⇒ y) ∧ (y ⇒ x))`
De Morgan	`¬(x ∧ y) = (¬x ∨ ¬y) `
De Morgan	`¬(x ∨ y) = (¬x ∧ ¬y) `
Distributivité de `∧` sur `∨`	`(x ∧ (y ∨ z)) = ((x ∧ y) ∨ (x ∧ z))`
Distributivité de `∨` sur `∧`	`(x ∨ (y ∧ z)) = ((x ∨ y) ∧ (x ∨ z)) `

4) Forme normale

• La disjonction étant associative et commutative, on appelle une disjonction, un ensemble fini de propositions connectées par l'opération de disjonction.
• La conjonction étant associative et commutative, on appelle une conjonction, un ensemble fini de propositions connectées par l'opération de conjonction.
• On appelle littéraux, les inconnues `x,y,z,...` ainsi que leur négation `"¬"x,"¬"y,"¬"z,...`.
• On appelle une clause disjontive, une disjonction de littéraux.
• On appelle une clause conjonctive, une conjonction de littéraux.
• On appelle une forme normale conjonctive (FNC), une conjonction de clauses disjonctives
• On appelle une forme normale disjonctive (FND), une disjonction de clauses conjonctives

Les 4 étapes de conversion en forme normal conjonctive :

• Élimination de l'équivalence
• Élimination de l’implication
• Déplacer `"¬"` à l'intérireur pour qu'il n'apparaise que dans les littéraux (loi De Morgan).
• Appliquer la loi de distributivité de `∨` sur `∧`.

5) Algorithme de résolution

Etant donné une proposition `B` servant de base de connaissance. Etant donné une proposition `p`. Voici l'algorithme pour déterminer si `p` est vrai sachant que la base de connaissance `B` est vrai, c'est à dire pour savoir si `B|==p`. On regarde si `B"∧¬"p` est intrinsèquement faux, autrement dit, si c'est contradictoire, si c'est faux quelques soient les hypothèses.

On met la base de connaissance `B`, ainsi que la proposition `p`, sous forme normale conjonctive c'est à dire une conjonction de clauses disjonctives de littéraux. Une clauses disjonctives de littéraux est appellé simplement une clause. On regroupe les deux pour former la proposition `B"∧¬"p` que l'on remet sous forme normale conjonctive et sur laquelle on applique le traitement suivant :

La conjonction en cours de traitement correspond à un ensemble de clauses. Et chaque clause correspond à un ensemble de littéraux,

1. Si la conjonction est vide alors retourner `1`.
2. Si une clause est vide alors retourner `0`.
3. Si une clause contient un littérale et sa négation, alors supprimer la clause de la conjonction.
4. Si une clause contient plusieurs fois un même littéral alors n'en garder qu'un dans la clause.
5. Si une clause est incluse dans une autre alors garder la plus petite et supprimer l'autre de la conjonction.
   
6. Si une clause contient un littérale `x` et une autre clause contient le littérale `"¬"x` alors ajouter la clause réunion des deux en enlevant les littéraux `x` et `"¬"x`.
   

PL-RESOLUTION(B,p) :

.