Théorème du consensus

Pour les articles homonymes, voir Consensus (homonymie).

Variable d'entrée			Valeur des fonctions
${\displaystyle x}$	${\displaystyle y}$	${\displaystyle z}$	${\displaystyle xy\vee {\bar {x}}z\vee yz}$	${\displaystyle 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].

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

${\displaystyle 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 :

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

Le terme ${\displaystyle yz}$ est appelé le consensus ou résolvant des termes ${\displaystyle xy}$ et ${\displaystyle {\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 ${\displaystyle xy}$ et de ${\displaystyle {\bar {x}}z}$ est donc bien ${\displaystyle yz}$.

L'identité duale est :

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

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

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 :

${\displaystyle xy\vee {\bar {x}}z\vee yz}$

= ${\displaystyle xy\vee {\bar {x}}z\vee (x\vee {\bar {x}})yz}$ (neutre et complément)

= ${\displaystyle xy\vee {\bar {x}}z\vee xyz\vee {\bar {x}}yz}$ (distributivité)

= ${\displaystyle xy\vee xyz\vee {\bar {x}}z\vee {\bar {x}}yz}$ (associativité et commutativité)

= ${\displaystyle xy\vee {\bar {x}}z}$ (absorption, deux fois)

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 ${\displaystyle a}$ et comme deuxième membre l'autre conjonction à laquelle est ajoutée l'opposé du littéral, à savoir ${\displaystyle {\bar {a}}}$. La réduction du consensus est la conjonction des deux termes, sans les littéraux ${\displaystyle a}$ et ${\displaystyle {\bar {a}}}$ et sans les répétitions de littéraux. Par exemple, si le consensus est ${\displaystyle v{\bar {x}}yz\vee vw{\bar {y}}z}$, sa réduction est ${\displaystyle vw{\bar {x}}z}$^[3].

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].

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].

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

• Portail des mathématiques