合意定理

ブール代数において、合意定理または合意規則^{[ 1 ]}は次の恒等式である。

${\displaystyle xy\vee {\bar {x}}z\vee yz=xy\vee {\bar {x}}z}$

条件の合意または解決${\displaystyle xy}$そして${\displaystyle {\bar {x}}z}$は${\displaystyle yz}$これは、一方の項では否定されず、もう一方の項では否定されるリテラルを除き、項のすべての固有のリテラルの論理積です。${\displaystyle y}$否定された項を含む${\displaystyle z}$（またはその逆）合意用語${\displaystyle yz}$これは誤りです。つまり、合意された用語は存在しません。

この等式の連言双対は次のとおりです。

${\displaystyle (x\vee y)({\bar {x}}\vee z)(y\vee z)=(x\vee y)({\bar {x}}\vee 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}}}$

選言の 2 つの連言項の合意または合意項は、一方の項がリテラルを含む場合に定義 されます。${\displaystyle a}$そしてもう一方の文字通り${\displaystyle {\bar {a}}}$反対意見。合意とは、両方の用語を省略した2つの用語の結合である。${\displaystyle a}$そして${\displaystyle {\bar {a}}}$、および繰り返しリテラル。たとえば、${\displaystyle {\bar {x}}yz}$そして${\displaystyle w{\bar {y}}z}$は${\displaystyle w{\bar {x}}z}$^{[ 2 ]}反対意見が複数ある場合、合意は定義されない。

規則の連言双対については、合意${\displaystyle y\vee z}$から導き出すことができる${\displaystyle (x\vee y)}$そして${\displaystyle ({\bar {x}}\vee z)}$分解推論規則を通して。これは、LHS が RHS から導出可能であることを示しています ( A → BならばA → AB ; A をRHS に、Bを( y ∨ z ) に置き換えます)。RHS は、論理積除去推論規則によって LHS から簡単に導出できます。RHS → LHS および LHS → RHS (命題論理) であるため、LHS = RHS (ブール代数) となります。

ブール代数では、繰り返し合意が、式のブレイク標準形を計算するアルゴリズムの中核を成している。^{[ 2 ]}

デジタルロジックでは、回路にコンセンサス項を含めることで、競合ハザードを排除できます。^{[ 3 ]}

コンセンサスの概念は、1937年にアーチー・ブレイクによってブレイクの正統形式に関連して導入されました。^{[ 4 ]}これは1954年にサムソンとミルズによって再発見され^{[ 5 ]} 、 1955年にはクワインによって再発見されました。 ^{[ 6 ]}クワインは「コンセンサス」という用語を作り出しました。ロビンソンは1965年にそれを節に適用し、彼の「解決原理」の基礎としました。^{[ 7 ] [ 8 ]}

• Roth, Charles H. Jr. および Kinney, Larry L. (2004、2010)。「論理設計の基礎」、第 6 版、p.  66 以降。