Théorème du consensus

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Consensus (homonymie).
Variable d'entrée Valeur des fonctions
x y z xy \vee \bar{x}z \vee yz xy \vee \bar{x}z
0 0 0 0 0
0 0 1 1 1
0 1 0 0 0
0 1 1 1 1
1 0 0 0 0
1 0 1 0 0
1 1 0 1 1
1 1 1 1 1

En algèbre de Boole, le théorème du consensus ou règle du consensus[1] est une identité booléenne (qui correspond à une équivalence de la logique propositionnelle). C'est une règle de simplification des expressions booléennes, avec d'autres comme la règle d'absorption ou celle d'élimination[2].

Énoncé[modifier | modifier le code]

Le théorème du consensus ou la règle du consensus est l'identité :

xy \vee \bar{x}z \vee yz = xy \vee \bar{x}z

Dans la simplification de formules booléennes, on réduit la partie gauche en la partie droite par la règle :

xy \vee \bar{x}z \vee yz \rightarrow xy \vee \overline{x}z.

Le terme yz est appelé le consensus ou résolvant des termes xy et \overline{x}z. Le consensus de deux conjonctions de littéraux est la conjonction obtenue à partir de tous les littéraux figurant dans celles-ci, en éliminant l'un d'entre eux qui apparaît à la fois sous forme niée dans l'une et non niée dans l'autre. Dans l'identité indiquée, si x est un littéral, et si y et z représentent des conjonctions de littéraux, le consensus de xy et de \bar{x}z est donc bien yz.

L'identité duale est :

(x \vee y)(\bar{x} \vee z)(y \vee z) = (x \vee y)(\bar{x} \vee z)

Le résolvant (y \vee z) se déduit des deux disjonctions (x \vee y) et (\bar{x} \vee z) par la règle dite de coupure ou de résolution, d'où la simplification.

Démonstration[modifier | modifier le code]

L'identité peut être vérifiée par sa table de vérité (donnée ci-dessus). On peut également la démontrer à partir des axiomes d'algèbre de Boole :

xy \vee \bar{x}z \vee yz
= xy \vee \bar{x}z \vee (x \vee \bar{x})yz (neutre et complément)
= xy \vee \bar{x}z \vee xyz \vee \bar{x}yz (distributivité)
= xy \vee xyz \vee \bar{x}z \vee \bar{x}yz (associativité et commutativité)
= xy \vee \bar{x}z (absorption, deux fois)

Consensus et réduction de consensus[modifier | modifier le code]

Le consensus de deux conjonctions de littéraux est une disjonction, cette disjonction contient comme premier membre l'une des conjonctions à laquelle est ajoutée un littéral a et comme deuxième membre l'autre conjonction à laquelle est ajoutée l'opposé du littéral, à savoir \bar{a}. La réduction du consensus est la conjonction des deux termes, sans les littéraux a et \bar{a} et sans les répétitions de littéraux. Par exemple, si le consensus est v\bar{x}yz \vee vw\bar{y}z, sa réduction est vw\bar{x}z[3].

Applications[modifier | modifier le code]

En simplification des expressions booléennes, l'application répétitive de la règle de consensus est au cœur du calcul de la forme canonique de Blake (en)[3].

En conception de circuits digitaux, la simplification par consensus d'un circuit élimine les risques de compétition[4].

Histoire[modifier | modifier le code]

Le concept de consensus a été introduit[5] par Archie Blake en 1937 dans sa thèse[6], dont un compte-rendu d'une page est paru en juin 1938 [7]. Le concept est redécouvert par Edward W. Samson et Burton E. Mills en 1954, et publié dans un rapport de l’Armée de l'Air américaine[8]. Il est publié par Willard Quine en 1955[9],[10]. C'est Quine qui introduit le terme de « consensus ». L’opération est aussi appelée parfois « résolvant » depuis que J. A. Robinson l’a utilisé, dans une forme plus générale, mais pour des clauses plutôt que pour des impliquants, comme base de son « principe de résolution » en preuve de théorèmes[11].

Références[modifier | modifier le code]

  1. Brown 2003, p. 44.
  2. Roth Jr. et Kinney 2014, 2.6 Simplification theorems p. 46-47 et 3.3 The Consensus Theorem, p. 70 et suiv..
  3. a et b Brown 2003, p. 81.
  4. Mohamed Rafiquzzaman, Fundamentals of Digital Logic and Microcontrollers, Hoboken, N.J., Wiley,‎ , 6e éd. (ISBN 1118855795), p. 75
  5. Donald E. Knuth (2011), The Art of Computer Programming, vol. 4A : Combinatorial Algorithms, Part 1, Addison-Wesley,‎ (ISBN 0-201-03804-8, présentation en ligne), p. 539 ; solution de l'exercice 7.1.1.31, section References..
  6. Archie Blake, Canonical expressions in Boolean algebra, éditeur=Dept. of Mathematics, University of Chicago,‎
  7. J. C. C. McKinsey, « Archie Blake. Canonical expressions in Boolean algebra », The Journal of Symbolic Logic, vol. 3, no 2,‎ , p. 93 (DOI 10.2307/2267634, JSTOR 2267634), accèès libre.
  8. Edward W. Samson, Burton E. Mills, Air Force Cambridge Research Center Technical Report 54-21, Avril 1954
  9. Willard Quine, « A way to simplify truth functions », Amer. Math. Monthly, vol. 62, no 9,‎ , p. 627-631 (DOI 10.2307/2307285, JSTOR 2307285, Math Reviews MR75886, lire en ligne).
  10. Quine reconnaît l'antériorité du travail de Samson et Mills dans une note en bas de page de son article.
  11. J. Alan Robinson, « A Machine-Oriented Logic Based on the Resolution Principle », Journal of the ACM, vol. 12, no 1,‎ , p. 23-41.

Bibliographie[modifier | modifier le code]

  • Frank Markham Brown, Boolean Reasoning: The Logic of Boolean Equations, Mineola, N.Y., Dover Publications,‎ , 2e éd. (ISBN 978-0486427850)
  • Charles H. Roth Jr. et Larry L. Kinney, Fundamentals of Logic Design, Stamford, CT, Cengage Learning,‎ , 7e éd. (1re éd. 2004) (ISBN 978-1-133-62847-7, lire en ligne).