Forme prenexe

Forme prenexe

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 ssi G=Q_1 x_1 Q_2 x_2 ... Q_n x_n G^{\prime} avec Q_i \in \{\forall, \exists\}.

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


Pour mettre une formule logique en forme prénexe, on peut utiliser les règles suivantes:

  1. \lnot \forall x F \Rightarrow \exists x \lnot F
  2. (\forall x F) \land G \Rightarrow \forall x (F \land G)
  3. (\forall x F) \lor G \Rightarrow \forall x (F \lor G)
  4. (\forall x F)\supset G \Rightarrow \exists x(F \supset G)
  5. G \land (\forall x F) \Rightarrow \forall x (G \land F)
  6. G \lor (\forall x F) \Rightarrow \forall x (G \lor F)
  7. G \supset (\forall x F) \Rightarrow \forall x (G \supset F)
  8. \lnot \exists x F \Rightarrow \forall x \lnot F
  9. (\exists x F) \land G \Rightarrow \exists x (F \land G)
  10. (\exists x F) \lor G \Rightarrow \exists x (F \lor G)
  11. (\exists x F)\supset G \Rightarrow \forall x(F \supset G)
  12. G \land (\exists x F) \Rightarrow \exists x (G \land F)
  13. G \lor (\exists x F) \Rightarrow \exists x (G \lor F)
  14. G \supset (\exists x F) \Rightarrow \exists x (G \supset F)

La variable x ne doit avoir aucune occurrence libre dans G (voir Calcul des prédicats). Sinon, utiliser un renommage de x en x'.

Ce document provient de « Forme pr%C3%A9nexe ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Forme prenexe 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 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 si et seulement si avec et une formule sans quantificateurs. Toutes… …   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”