Théorème du consensus
![Page d’aide sur l’homonymie](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a9/Logo_disambig.svg/20px-Logo_disambig.svg.png)
Pour les articles homonymes, voir Consensus (homonymie).
Variable d'entrée | Valeur des fonctions | |||
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é
Le théorème du consensus ou la règle du consensus est l'identité :
Dans la simplification de formules booléennes, on réduit la partie gauche en la partie droite par la règle :
- .
Le terme est appelé le consensus ou résolvant des termes et . 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 et de est donc bien .
L'identité duale est :
Le résolvant se déduit des deux disjonctions et 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 :
- = (neutre et complément)
- = (distributivité)
- = (associativité et commutativité)
- = (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 et comme deuxième membre l'autre conjonction à laquelle est ajoutée l'opposé du littéral, à savoir . La réduction du consensus est la conjonction des deux termes, sans les littéraux et et sans les répétitions de littéraux. Par exemple, si le consensus est , sa réduction est [3].
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)[3].
En conception de circuits digitaux, la simplification par consensus d'un circuit élimine les risques de compétition[4].
Histoire
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 [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
- ↑ Brown 2003, p. 44.
- ↑ Roth et Kinney 2014, 2.6 Simplification theorems p. 46-47 et 3.3 The Consensus Theorem, p. 70 et suiv..
- ↑ a et b Brown 2003, p. 81.
- ↑ (en) Mohamed Rafiquzzaman, Fundamentals of Digital Logic and Microcontrollers, Hoboken, N.J., Wiley, , 6e éd., 512 p. (ISBN 978-1-118-85579-9 et 1-118-85579-5, lire en ligne), p. 75
- ↑ (en) Donald E. Knuth, The Art of Computer Programming, vol. 4A : Combinatorial Algorithms, Part 1, Addison-Wesley, (ISBN 978-0-201-03804-0 et 0-201-03804-8, présentation en ligne), p. 539 ; solution de l'exercice 7.1.1.31, section References.
- ↑ (en) Archie Blake, Canonical expressions in Boolean algebra, University of Chicago, Dept. of Mathematics, .
- ↑ J. C. C. McKinsey, « Archie Blake. Canonical expressions in Boolean algebra », J. Symb. Logic, vol. 3, no 2, , p. 93 (DOI 10.2307/2267634, JSTOR 2267634), accès libre.
- ↑ (en) Edward W. Samson et Burton E. Mills, Air Force Cambridge Research Center Technical Report 54-21, avril 1954.
- ↑ (en) Willard Quine, « A way to simplify truth functions », Amer. Math. Monthly, vol. 62, no 9, , p. 627-631 (DOI 10.2307/2307285, JSTOR 2307285, MR MR75886).
- ↑ Quine reconnaît l'antériorité du travail de Samson et Mills dans une note en bas de page de son article.
- ↑ (en) J. Alan Robinson, « A Machine-Oriented Logic Based on the Resolution Principle », Journal of the ACM, vol. 12, no 1, , p. 23-41.
Bibliographie
- (en) Frank Markham Brown, Boolean Reasoning : The Logic of Boolean Equations, Mineola, N.Y., Dover Publications, , 2e é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, , 7e éd. (1re éd. 2004), 816 p. (ISBN 978-1-133-62847-7, lire en ligne).
Portail des mathématiques