Consensus theorem

Theorem in Boolean algebra
Variable inputs Function values
x y z x y x ¯ z y z {\displaystyle xy\vee {\bar {x}}z\vee yz} x y x ¯ z {\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
Karnaugh map of ABACBC. Omitting the red rectangle does not change the covered area.

In Boolean algebra, the consensus theorem or rule of consensus[1] is the identity:

x y x ¯ z y z = x y x ¯ z {\displaystyle xy\vee {\bar {x}}z\vee yz=xy\vee {\bar {x}}z}

The consensus or resolvent of the terms x y {\displaystyle xy} and x ¯ z {\displaystyle {\bar {x}}z} is y z {\displaystyle yz} . 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 y {\displaystyle y} includes a term that is negated in z {\displaystyle z} (or vice versa), the consensus term y z {\displaystyle yz} is false; in other words, there is no consensus term.

The conjunctive dual of this equation is:

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

Proof

x y x ¯ z y z = x y x ¯ z ( x x ¯ ) y z = x y x ¯ z x y z x ¯ y z = ( x y x y z ) ( x ¯ z x ¯ y z ) = x y ( 1 z ) x ¯ z ( 1 y ) = x y x ¯ z {\displaystyle {\begin{aligned}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{aligned}}}

Consensus

The consensus or consensus term of two conjunctive terms of a disjunction is defined when one term contains the literal a {\displaystyle a} and the other the literal a ¯ {\displaystyle {\bar {a}}} , an opposition. The consensus is the conjunction of the two terms, omitting both a {\displaystyle a} and a ¯ {\displaystyle {\bar {a}}} , and repeated literals. For example, the consensus of x ¯ y z {\displaystyle {\bar {x}}yz} and w y ¯ z {\displaystyle w{\bar {y}}z} is w x ¯ z {\displaystyle w{\bar {x}}z} .[2] The consensus is undefined if there is more than one opposition.

For the conjunctive dual of the rule, the consensus y z {\displaystyle y\vee z} can be derived from ( x y ) {\displaystyle (x\vee y)} and ( x ¯ z ) {\displaystyle ({\bar {x}}\vee z)} through the resolution inference rule. This shows that the LHS is derivable from the RHS (if AB then AAB; replacing A with RHS and B with (yz) ). 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.[2]

In digital logic, including the consensus term in a circuit can eliminate race hazards.[3]

History

The concept of consensus was introduced by Archie Blake in 1937, related to the Blake canonical form.[4] It was rediscovered by Samson and Mills in 1954[5] and by Quine in 1955.[6] Quine coined the term 'consensus'. Robinson used it for clauses in 1965 as the basis of his "resolution principle".[7][8]

References

  1. ^ Frank Markham Brown [d], Boolean Reasoning: The Logic of Boolean Equations, 2nd edition 2003, p. 44
  2. ^ a b Frank Markham Brown, Boolean Reasoning: The Logic of Boolean Equations, 2nd edition 2003, p. 81
  3. ^ Rafiquzzaman, Mohamed (2014). Fundamentals of Digital Logic and Microcontrollers (6 ed.). p. 65. ISBN 1118855795.
  4. ^ "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 σ {\displaystyle \sigma } and defined on pp. 29–31.
  5. ^ Edward W. Samson, Burton E. Mills, Air Force Cambridge Research Center, Technical Report 54-21, April 1954
  6. ^ Willard van Orman Quine, "The problem of simplifying truth functions", American Mathematical Monthly 59:521-531, 1952 JSTOR 2308219
  7. ^ John Alan Robinson, "A Machine-Oriented Logic Based on the Resolution Principle", Journal of the ACM 12:1: 23–41.
  8. ^ Donald Ervin Knuth, The Art of Computer Programming 4A: Combinatorial Algorithms, part 1, p. 539

Further reading

  • Roth, Charles H. Jr. and Kinney, Larry L. (2004, 2010). "Fundamentals of Logic Design", 6th Ed., p. 66ff.