Consensus theorem

:$\backslash 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}

{{anchor|Consensus}}{{anchor|Opposition}}

The consensus or consensus term of two conjunctive terms of a disjunction is defined when one term contains the literal $a$ and the other the literal $\backslash bar\{a\}$, an opposition. The consensus is the conjunction of the two terms, omitting both $a$ and $\backslash bar\{a\}$, and repeated literals. For example, the consensus of $\backslash bar\{x\}yz$ and $w\backslash bar\{y\}z$ is $w\backslash bar\{x\}z$.Frank Markham Brown, Boolean Reasoning: The Logic of Boolean Equations, 2nd edition 2003, p. 81 The consensus is undefined if there is more than one opposition.

For the conjunctive dual of the rule, the consensus $y\; \backslash vee\; z$ can be derived from $(x\backslash vee\; y)$ and $(\backslash bar\{x\}\; \backslash vee\; z)$ 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).

In Boolean algebra, repeated consensus is the core of one algorithm for calculating the Blake canonical form of a formula.

In digital logic, including the consensus term in a circuit can eliminate race hazards.{{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}}

The concept of consensus was introduced by Archie Blake in 1937, related to the Blake canonical form."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 $\backslash sigma$ and defined on pp. 29–31. It was rediscovered by Samson and Mills in 1954Edward W. Samson, Burton E. Mills, Air Force Cambridge Research Center, Technical Report 54-21, April 1954 and by Quine in 1955.Willard van Orman Quine, "The problem of simplifying truth functions", American Mathematical Monthly 59:521-531, 1952 {{JSTOR|2308219}} Quine coined the term 'consensus'. Robinson used it for clauses in 1965 as the basis of his "resolution principle".John Alan Robinson, "A Machine-Oriented Logic Based on the Resolution Principle", Journal of the ACM 12:1: 23–41.Donald Ervin Knuth, The Art of Computer Programming 4A: Combinatorial Algorithms, part 1, p. 539

{{Reflist}}

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

{{DEFAULTSORT:Consensus Theorem}}

Category:Boolean algebra

Category:Theorems in lattice theory

Category:Theorems in propositional logic