罗宾斯代数

在抽象代数中，罗宾斯代数是一个包含单一二元运算的代数，通常表示为∨{displaystyle{lor}，以及一个单项运算，通常用∨表示。和一个单项运算，通常用∨表示。¬{displaystyleneg}。.这些操作满足以下公理。对于所有元素a,b,和c:交换性：a∨b=b∨a{displaystylealorb=blora}。罗宾斯方程:¬{displaystyle＆left(neg＆left(alorbright)lor＆left(alor＆negbright)right)=a}。多年来，人们猜想，但没有证明，所有罗宾斯矩阵都是布尔矩阵。这一点在1996年被证明，所以罗宾斯代数这个词现在只是布尔代数的一个同义词。

1933年，爱德华-亨廷顿提出了一套新的布尔代数公理，包括上面的（1）和（2），另外。亨廷顿公式：¬(¬a∨b)∨¬(¬a∨¬b)=a。{displaystyleneg(negalorb)lorneg(negalornegb)=a.}。从这些公理中，亨廷顿得出了布尔代数的通常公理。此后不久，赫伯特-罗宾斯提出了罗宾斯猜想，即亨廷顿方程可以用后来被称为罗宾斯方程的东西代替，其结果仍然是布尔代数。∨{displaystyle{lor}将解释布尔连接和¬{displaystyle阴性}则解释为布尔连接，而¬{displaystyle阴性}则解释为布尔补充。布尔互补。

布尔满足和常数0和1很容易从罗宾斯代数的基元中定义。在验证该猜想之前，罗宾斯的系统被称为罗宾斯代数。验证罗宾斯猜想需要证明亨廷顿方程，或布尔代数的一些其他公理化，作为罗宾斯代数的定理。亨廷顿、罗宾斯、阿尔弗雷德-塔斯基和其他人都在研究这个问题，但都没有找到证明或反例。威廉-麦库恩在1996年用自动定理检验器EQP证明了这个猜想。关于罗宾斯猜想的完整证明，在一个一致的符号中并紧跟McCune，见Mann（2003）。Dahn（1998）简化了McCune的机器证明。