Consensus theorem

Variable inputs			Function values
x	y	z	Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle xy \vee \bar{x}z \vee yz}	Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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

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

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle xy \vee \bar{x}z \vee yz = xy \vee \bar{x}z}

The consensus or resolvent of the terms $xy$ and ${\bar {x}}z$ is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\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$ includes a term that is negated in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle z} (or vice versa), the consensus term Failed to parse (Conversion error. Server ("https://wikimedia.org/api/rest_") reported: "Cannot get mml. Server problem."): {\displaystyle yz} is false; in other words, there is no consensus term.

The conjunctive dual of this equation is:

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

Proof

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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} }

Consensus

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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \bar{a}} , an opposition. The consensus is the conjunction of the two terms, omitting both $a$ and ${\bar {a}}$ , and repeated literals. For example, the consensus of ${\bar {x}}yz$ and Failed to parse (Conversion error. Server ("https://wikimedia.org/api/rest_") reported: "Cannot get mml. Server problem."): {\displaystyle w{\bar {y}}z} is $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 Failed to parse (Conversion error. Server ("https://wikimedia.org/api/rest_") reported: "Cannot get mml. Server problem."): {\displaystyle y\vee z} can be derived from $(x\vee y)$ and $({\bar {x}}\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).

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

^ Frank Markham Brown [d], Boolean Reasoning: The Logic of Boolean Equations, 2nd edition 2003, p. 44
^ ^2.0 ^2.1 Frank Markham Brown, Boolean Reasoning: The Logic of Boolean Equations, 2nd edition 2003, p. 81
^ Rafiquzzaman, Mohamed (2014). Fundamentals of Digital Logic and Microcontrollers (6 ed.). p. 65. ISBN 1118855795.
^ "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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \sigma} and defined on pp. 29–31.
^ Edward W. Samson, Burton E. Mills, Air Force Cambridge Research Center, Technical Report 54-21, April 1954
^ Willard van Orman Quine, "The problem of simplifying truth functions", American Mathematical Monthly 59:521-531, 1952 JSTOR 2308219
^ 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