3 Forme normale
La mise sous forme normale va nous permettre de :
-
simplifier les formules en supprimant les quantificateurs ;
- pouvoir faire de la démonstration par résolution.
3.1 Forme prénexe
Définition 7
Une formule est sous forme prénexe si elle s'écrit
Q1x1... Qnxn F
où les Qi sont des quantificateurs (" ou $) et F est
une formule sans quantificateur.
Propriété 20
Toute formule est équivalente à une formule sous forme prénexe.
Preuve : transformation de la formule :
-
Supprimer les équivalences ( « ) et les implications
( ® ) :
-
A « Bº(A ® B) Ù (B ® A)
- A ® Bº¬ A Ú B
- Faire « descendre » les négations :
-
¬ " x Aº$ x ¬ A
- ¬ $ x Aº" x ¬ A
- Faire « remonter » les quantificateurs en renommant les variables
(a-conversion) et en utilisant l'équivalence
( Qx A) Ù Bº B Ù ( Qx A)º
Qx (A Ù B) (idem pour Ú )
où Q est un quantificateur et x une variable non libre dans B.
Exemple : " x p(x) ® $ x p(x)
3.2 Skolémisation
Suppression des quantificateurs existentiels ($).
Intuition : penser à l'h dans l'expression de la continuité.
Définition 8 [skolémisation]
On obtient la forme skolémisée d'une formule sous forme prénexe en :
-
associant à chaque variable x quantifiée existentiellement un
(nouveau) symbole fonctionnel f (éventuellement une constante) d'arité égale au nombre de quantifications
universelles antérieures x1... xn ;
- supprimant la quantification existentielle ;
- remplaçant chaque occurrence de la variable x par le terme f(x1,...,xn).
Attention : la formule skolémisée n'est pas équivalente à la formule originale.
Exemple : " x(" y p(x,y) ® ¬ $ z q(x,z))
Propriété 21
Soit A* la forme skolémisée d'une formule A.
-
A*|= A ;
- A est satisfiable ssi A* l'est.
3.3 Forme standard
Remarques :
-
les quantifications universelles d'une formule prénexe et
skolémisée étant inutiles, on les oublie ;
- une formule prénexe et skolémisée peut être mise sous forme
normale conjonctive (clausale).
Définition 9
Une formule prénexe-skolémisée-clausale est dite sous forme standard.