Formes normales (Normalisation)
Définition :
Toute formule peut se réécrire sous la forme :
C1 ∧ C2 ∧ ... ∧ Cn
Où chaque Ci (appelé clause) est elle-même de la forme :
p1 ∨ p2 ∨ ... ∨ pm ∨ ¬q1 ∨ ¬q2 ∨ ... ∨ ¬qr
Où les pj et qk sont des atomes.
Cette forme est appelée forme normale conjonctive.
Méthode : Algorithme FNC
Exemple : ((b ∨ c) ⇒ a) ∨ d
Appliquer l'équivalence double-implique et implique-ou pour supprimer les ⇒ et ⇔.
≈ (¬(b ∨ c) ∨ a) ∨ d
Appliquer De Morgan pour "descendre" les négations près des variables.
≈ ((¬b ∧ ¬c) ∨ a) ∨ d
Appliquer la distributivité pour descendre les ∨ et remonter les ∧
≈ ((¬b ∨ a) ∧ (¬c ∨ a)) ∨ d ≈ ((¬b ∨ a) ∨ d) ∧ ((¬c ∨ a)) ∨ d)
Appliquer l'associativité des ∨ et ∧ ≈ (¬b ∨ a ∨ d) ∧ (¬c ∨ a ∨ d)
