Théorème du consensus

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

Énoncé

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

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

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

Applications

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

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

Histoire

Le concept de consensus a été introduit par Archie Blake en 1937 dans sa thèse, dont un compte-rendu d'une page est paru en juin 1938 . 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. Il est publié par Willard Quine en 1955. 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.

Références

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Consensus theorem » (voir la liste des auteurs).

Bibliographie

• (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).