Forme prénexe

Forme prénexe

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.

Règles de transformations

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

# Forme intiale 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

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

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Forme prénexe de Wikipédia en français (auteurs)

Игры ⚽ Нужен реферат?

Regardez d'autres dictionnaires:

  • Forme Prénexe — Une formule de la logique du premier ordre est en forme prénexe si tous ses quantificateurs ( et ) apparaissent à gauche dans cette formule. C’est à dire, G est en forme prénexe ssi avec . Toutes les formules du premier ordre sont logiquement… …   Wikipédia en Français

  • Forme prenexe — Forme prénexe Une formule de la logique du premier ordre est en forme prénexe si tous ses quantificateurs ( et ) apparaissent à gauche dans cette formule. C’est à dire, G est en forme prénexe ssi avec . Toutes les formules du premier ordre sont… …   Wikipédia en Français

  • Forme Normale De Skolem — Skolémisation En logique mathématique, la skolémisation d une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel… …   Wikipédia en Français

  • Forme normale de Skolem — Skolémisation En logique mathématique, la skolémisation d une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel… …   Wikipédia en Français

  • Forme normale de skolem — Skolémisation En logique mathématique, la skolémisation d une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel… …   Wikipédia en Français

  • Theoreme de Herbrand — Théorème de Herbrand En logique, le théorème de Herbrand établit un lien entre calcul des prédicats et calcul des propositions. Alors qu il est possible de déterminer de manière certaine si une proposition du calcul des propositions est… …   Wikipédia en Français

  • Théorème de Herbrand — En logique, le théorème de Herbrand établit un lien entre calcul des prédicats et calcul des propositions. Alors qu il est possible de déterminer de manière certaine si une proposition du calcul des propositions est démontrable ou pas, la… …   Wikipédia en Français

  • Théorème de herbrand — En logique, le théorème de Herbrand établit un lien entre calcul des prédicats et calcul des propositions. Alors qu il est possible de déterminer de manière certaine si une proposition du calcul des propositions est démontrable ou pas, la… …   Wikipédia en Français

  • Theoreme de completude de Godel — Théorème de complétude de Gödel Le théorème de complétude du calcul des prédicats du premier ordre a été démontré par Kurt Gödel (1929, thèse de doctorat, sur la complétude du calcul logique). Il affirme que le calcul des prédicats est complet au …   Wikipédia en Français

  • Théorème de complétude — de Gödel Le théorème de complétude du calcul des prédicats du premier ordre a été démontré par Kurt Gödel (1929, thèse de doctorat, sur la complétude du calcul logique). Il affirme que le calcul des prédicats est complet au sens où toute… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”