Forme normale conjonctive

Forme normale conjonctive
Article principal : Calcul des propositions.

En logique booléenne et en calcul des propositions, une forme normale conjonctive (FNC) est une normalisation d'une expression logique qui est une conjonction de clauses, autrement dit une conjonction de disjonction de littéraux. Les formules en FNC sont utilisée dans le cadre démonstration automatique de théorèmes ou encore dans la résolution du problème SAT.

Sommaire

Définition et exemples

Une expression logique est en FNC si et seulement si elle est une conjonction d'une ou plusieurs disjonction(s) d'un ou plusieurs littéraux. Tout comme dans une forme normale disjonctive (FND), les seuls opérateurs dans une FNC sont le et logique, le ou logique et la négation. L'opérateur non ne peut être utilisé que dans un littéral, c'est-à-dire qu'il ne peut que précéder une variable. Par exemple, toutes les expressions suivantes sont en FNC:

Exemples de formules en FNC  :
  1. A \and B
  2. A\!
  3. (A \or B) \and C
  4. (A \or \neg B \or \neg C) \and (\neg D \or E \or F)

Cependant, les expressions suivantes ne sont pas en FNC:

Contre exemples de formules en FNC  :
  1. \neg(A \and B) — la négation s'applique à toute la parenthèse plutôt que directement à une variable
  2. A \and (B \or (C \and D)) — un et est imbriqué dans un ou

Conversions en FNC

Toute formule booléenne peut se réécrire sous la forme d'une formule en FNC qui possède la même valeur de vérité, donc logiquement équivalente.

D'autres transformations nécessitent l'introduction de variables (ou de propositions) supplémentaires, mais ont l'avantage de garantir que la taille de la formule résultante restera raisonnable.

Conversion équivalente

Convertir une expression vers une FNC requiert l'utilisation de règles de transformation logiques, comme l'élimination de double négations, les lois de De Morgan, et la loi de distributivité.

Transformation en FNC  :

(\lnot (X_1 \lor X_2) \lor (X_3 \land X_4) ) \land (\lnot X_1 \lor X_2)

\equiv

(\lnot X_1 \lor X_3 ) \land (\lnot X_1 \lor X_4) \land (\lnot X_2 \lor X_3) \land (\lnot X_2 \lor X_4) \land (\lnot X_1 \lor X_2)

L'application des lois de la distributivité peut dans certain cas faire grandir la formule de manière exponentielle.

Formule dont la CNF possède une taille exponentielle  :

la FNC d'une expression de la forme suivante, en Forme normale disjonctive, et qui comporte n termes :

(X_1 \and Y_1) \or (X_2 \and Y_2) \or \dots \or (X_n \and Y_n)

Dont la CNF, de taille 2n, est de la forme :

(X_1 \vee \cdots \vee X_{n-1} \vee X_n) \wedge (X_1 \vee \cdots \vee X_{n-1} \vee Y_n) \wedge \cdots \wedge (Y_1 \vee \cdots \vee Y_{n-1} \vee Y_n).

Transformations linéaires

Pour éviter les transformations exponentielles, il est possible d'appliquer des transformations en introduisant des variables supplémentaires[1]. De ce fait, ce type de transformation ne crée plus des formules logiquement équivalentes, comme la transformation précédente, mais des transformations qui préservent la satisfiabilité de la formule originale.

La formule de l' exemple 2, par exemple, peut être réécrites en introduisant les variables Z_1,\ldots,Z_n.

Exemple de transformation linéaire  :

Une formule de la forme suivante :

(X_1 \and Y_1) \or (X_2 \and Y_2) \or \dots \or (X_n \and Y_n)

Peut être réécrite en une formule équisatisfiable

(Z_1 \vee \cdots \vee Z_n) \wedge (\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge \cdots \wedge (\neg Z_n \vee X_n) \wedge (\neg Z_n \vee Y_n).

Intuitivement, dans cet exemple, les variables Zn imposent la vérité de la i-ème conjonction de la formule originale, et imposent par les implications Z_i \rightarrow X_i,Z_i\rightarrow Y_n dans le cas ou ces variables prennent la valeur vrai. Dit autrement, si Zn est vrai, alors Xi et Yi doivent être vrai aussi. La première clause de la transformation impose qu'au moins un des Zi soit vrai pour que la formule soit satisfaite, donc qu'au moins une des clause de la formule originale soit vraie.

On peut aussi baser des transformations sur des clauses de types Z_i \vee \neg X_i \vee \neg Y_i. Ces clauses impliquent l'équivalence, Z_i \equiv X_i \wedge Y_i; on peut voir dans ces formules la définition de Zi comme un alias pour la formule X_i \wedge Y_i.

De telles transformations permettent d'obtenir une formule en FNC dont la taille est linéaire par rapport à la taille de la formule originale[1].

Voir aussi

Notes et références

  1. ↑ a et b (fr)Jean Betrema, « Modèles de calcul », p. chapitre 9 : Problèmes NP-complets > SAT est NP-complet > CNF est NP-complet.
    Preuve et transformation linéaire d'une formule SAT quelconque en CNF équisatisfiable.

Wikimedia Foundation. 2010.

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

Игры ⚽ Поможем написать курсовую

Regardez d'autres dictionnaires:

  • Forme normale disjonctive — Article principal : Calcul des propositions. En logique booléenne ou en Calcul des propositions, une forme normale disjonctive (FND) est une normalisation d une expression logique qui est une disjonction de clauses conjonctives. Elle est… …   Wikipédia en Français

  • FND — Forme normale disjonctive Article principal : Calcul des propositions. En logique booléenne ou en Calcul des propositions, une forme normale disjonctive (FND) est une normalisation d une expression logique qui est une disjonction de clauses… …   Wikipédia en Français

  • Antilogie — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français

  • Calcul Des Propositions — Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C est aussi la première… …   Wikipédia en Français

  • Calcul des propositions — Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C est aussi la première… …   Wikipédia en Français

  • Calcul propositionnel — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français

  • Expression booléenne — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français

  • Logique des propositions — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français

  • Logique propositionnelle — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français

  • Proposition (logique mathématique) — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français

Share the article and excerpts

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