In Boolean algebra, the consensus theorem or rule of consensus[1] is the identity:
The consensus or resolvent of the terms and is . 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 includes a term that is negated in (or vice versa), the consensus term is false; in other words, there is no consensus term.
The consensus or consensus term of two conjunctive terms of a disjunction is defined when one term contains the literal and the other the literal , an opposition. The consensus is the conjunction of the two terms, omitting both and , and repeated literals. For example, the consensus of and is .[2] The consensus is undefined if there is more than one opposition.
For the conjunctive dual of the rule, the consensus can be derived from and through the resolutioninference 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]