Английская Википедия:Consensus theorem
| Variable inputs | Function values | |||
| x | y | z | <math>xy \vee \bar{x}z \vee yz</math> | <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 |
In Boolean algebra, the consensus theorem or rule of consensus[1] 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Шаблон:Anchor 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>.[2] 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.[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]Шаблон:Page needed 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
Further reading
- Roth, Charles H. Jr. and Kinney, Larry L. (2004, 2010). "Fundamentals of Logic Design", 6th Ed., p. 66ff.
- ↑ Шаблон:Ill, 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
- ↑ Шаблон:Cite book
- ↑ "Canonical expressions in Boolean algebra", Dissertation, Department of Mathematics, University of Chicago, 1937, reviewed in J. C. C. McKinsey, The Journal of Symbolic Logic 3:2:93 (June 1938) Шаблон:Doi Шаблон:JSTOR
- ↑ 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
- ↑ 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
