Forme prénexe

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Une formule de la logique du premier ordre est en forme prénexe si tous ses quantificateurs (\forall et \exists) apparaissent à gauche dans cette formule. C’est-à-dire, G est en forme prénexe si et seulement si G=Q_1 x_1 Q_2 x_2 ... Q_n x_n G^{\prime} avec Q_i \in \{\forall, \exists\} et G^{\prime} une formule sans quantificateurs.

Toutes les formules du premier ordre sont logiquement équivalentes à une formule en forme prénexe.

La complexité d'une formule de logique mise en forme prénexe se mesure à son premier quantificateur et au nombre d'alternance de blocs de quantificateurs universels ou existentiels qui le suivent et précèdent la formule sans quantificateur.

Règles de transformations[modifier | modifier le code]

Pour mettre une formule logique en forme prénexe, on peut utiliser les règles de transformation suivantes Gauche \Rightarrow Droite entre formules équivalentes :

# Forme initiale Forme prénexe
1 \lnot \forall x F \exists x \lnot F
2 (\forall x F) \land G  \forall x (F \land G)
3 (\forall x F) \lor G  \forall x (F \lor G)
4 (\forall x F)\rightarrow G  \exists x(F \rightarrow G)
5 G \land (\forall x F)  \forall x (G \land F)
6 G \lor (\forall x F)  \forall x (G \lor F)
7 G \rightarrow (\forall x F)  \forall x (G \rightarrow F)
8 \lnot \exists x F  \forall x \lnot F
9 (\exists x F) \land G  \exists x (F \land G)
10 (\exists x F) \lor G  \exists x (F \lor G)
11 (\exists x F)\rightarrow G  \forall x(F \rightarrow G)
12 G \land (\exists x F)  \exists x (G \land F)
13 G \lor (\exists x F)  \exists x (G \lor F)
14 G \rightarrow (\exists x F)  \exists x (G \rightarrow F)

La variable x ne doit avoir aucune occurrence libre dans G (voir Calcul des prédicats). Sinon renommer au préalable x par une variable nouvelle n'apparaissant pas librement dans les formules F et G.

Remarques[modifier | modifier le code]

Il n'y a pas de règles simples de transformation pour une formule comportant le connecteur  \leftrightarrow mais ces règles suffisent car \{\lnot, \land, \lor, \rightarrow\} est un système complet de connecteurs. Pour transformer une formule, on peut donc appliquer cette démarche :

  1. Supprimer les équivalences, en les remplaçant par des implications ;
  2. Transporter les négations devant les formules atomiques ;
  3. Transporter les quantificateurs en tête de la formule, en renommant les variables si nécessaire.

Articles connexes[modifier | modifier le code]