{{Short description|Theorem in Boolean algebra}} <!-- This is the truth table shown on the right. Scroll down to edit the rest of the article. !--> {| class="wikitable floatright" style="text-align: center;" |- ! scope="colgroup" colspan=3| Variable inputs ! scope="colgroup" colspan=2| Function values |- ! scope="col" style="font-weight: normal;"| ''x'' ! scope="col" style="font-weight: normal;"| ''y'' ! scope="col" style="font-weight: normal;"| ''z'' ! scope="col" | <math>xy \vee \bar{x}z \vee yz</math> ! scope="col" | <math>xy \vee \bar{x}z</math> |- | 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 |} [[File:Karnaugh map KV Race Hazard 10.svg|thumb|Karnaugh map of ''AB'' ∨ {{color|#00bd72|''{{overline|A}}C''}} ∨ {{color|#ff0000|''BC''}}. Omitting the red rectangle does not change the covered area.]] In Boolean algebra, the '''consensus theorem''' or '''rule of consensus'''<ref>{{ill|Frank Markham Brown|d|Q112500339}}, ''Boolean Reasoning: The Logic of Boolean Equations'', 2nd edition 2003, p. 44</ref> is the identity:

:<math>xy \vee \bar{x}z \vee yz = xy \vee \bar{x}z</math>

The '''consensus''' or '''resolvent''' of the terms <math>xy</math> and <math>\bar{x}z</math> is <math>yz</math>. It is the conjunction of all the unique literals of the terms, excluding the literal that appears unnegated in one term and negated in the other. If <math>y</math> includes a term that is negated in <math>z</math> (or vice versa), the consensus term <math>yz</math> is false; in other words, there is no consensus term.

The conjunctive dual of this equation is:

:<math>(x \vee y)(\bar{x} \vee z)(y \vee z) = (x \vee y)(\bar{x} \vee z)</math>

==Proof== :<math> \begin{align} xy \vee \bar{x}z \vee yz &= xy \vee \bar{x}z \vee (x \vee \bar{x})yz \\ &= xy \vee \bar{x}z \vee xyz \vee \bar{x}yz \\ &= (xy \vee xyz) \vee (\bar{x}z \vee \bar{x}yz) \\ &= xy(1\vee z)\vee\bar{x}z(1\vee y) \\ &= xy \vee \bar{x}z \end{align} </math>

==Consensus== {{anchor|Consensus}}{{anchor|Opposition}} The '''consensus''' or '''consensus term''' of two conjunctive terms of a disjunction is defined when one term contains the literal <math>a</math> and the other the literal <math>\bar{a}</math>, an '''opposition'''. The consensus is the conjunction of the two terms, omitting both <math>a</math> and <math>\bar{a}</math>, and repeated literals. For example, the consensus of <math>\bar{x}yz</math> and <math>w\bar{y}z</math> is <math>w\bar{x}z</math>.<ref name="brown81">Frank Markham Brown, ''Boolean Reasoning: The Logic of Boolean Equations'', 2nd edition 2003, p. 81</ref> The consensus is undefined if there is more than one opposition.

For the conjunctive dual of the rule, the consensus <math>y \vee z</math> can be derived from <math>(x\vee y)</math> and <math>(\bar{x} \vee z)</math> through the resolution inference rule. This shows that the LHS is derivable from the RHS (if ''A'' → ''B'' then ''A'' → ''AB''; replacing ''A'' with RHS and ''B'' with (''y'' ∨ ''z'') ). The RHS can be derived from the LHS simply through the conjunction elimination inference rule. Since RHS → LHS and LHS → RHS (in propositional calculus), then LHS = RHS (in Boolean algebra).

==Applications== In Boolean algebra, repeated consensus is the core of one algorithm for calculating the Blake canonical form of a formula.<ref name="brown81"/>

In digital logic, including the consensus term in a circuit can eliminate race hazards.<ref>{{cite book |last1=Rafiquzzaman |first1=Mohamed |author1-link=Mohamed Rafiquzzaman |title=Fundamentals of Digital Logic and Microcontrollers |date=2014 |isbn=978-1118855799 |page=65 |publisher=John Wiley & Sons |edition=6}}</ref>

==History== The concept of consensus was introduced by Archie Blake in 1937, related to the Blake canonical form.<ref name="blake">"Canonical expressions in Boolean algebra", Dissertation, Department of Mathematics, University of Chicago, 1937, {{ProQuest|301838818}}, reviewed in J. C. C. McKinsey, ''The Journal of Symbolic Logic'' '''3''':2:93 (June 1938) {{doi|10.2307/2267634}} {{JSTOR|2267634}}. The consensus function is denoted <math>\sigma</math> and defined on pp. 29–31.</ref> It was rediscovered by Samson and Mills in 1954<ref>Edward W. Samson, Burton E. Mills, Air Force Cambridge Research Center, Technical Report 54-21, April 1954</ref> and by Quine in 1955.<ref>Willard van Orman Quine, "The problem of simplifying truth functions", ''American Mathematical Monthly'' '''59''':521-531, 1952 {{JSTOR|2308219}}</ref> Quine coined the term 'consensus'. Robinson used it for clauses in 1965 as the basis of his "resolution principle".<ref>John Alan Robinson, "A Machine-Oriented Logic Based on the Resolution Principle", ''Journal of the ACM'' '''12''':1: 23–41.</ref><ref>Donald Ervin Knuth, ''The Art of Computer Programming'' '''4A''': ''Combinatorial Algorithms'', part 1, p. 539</ref>

==References== {{Reflist}}

==Further reading== * Roth, Charles H. Jr. and Kinney, Larry L. (2004, 2010). "Fundamentals of Logic Design", 6th Ed., p.&nbsp;66ff.

{{DEFAULTSORT:Consensus Theorem}} Category:Boolean algebra Category:Theorems in lattice theory Category:Theorems in propositional logic