布尔代数公理及其他常用逻辑运算

交换律：x y = y x。

结合律：(x y) z = x (y z)。

Huntington等式：n(n(x) y) n(n(x) n(y)) = x。

一元函数符号 n 可以读做‘补’。

Herbert Robbins 接着摆出下列问题： Huntington等式能否缩短为下述的等式，并且这个新等式与结合律和交换律一起成为布尔代数的基础? 通过一组叫做 Robbins 代数的公理，问题就变成了：是否所有的 Robbins 代数都是布尔代数?

Robbins 代数的公理化：

交换律： x y = y x。

结合律： (x y) z = x (y z)。

Robbins等式： n(n(x y') n(x n(y))) = x。

这个问题自从 1930 年代一直是公开的，并成为 Alfred Tarski 和他的学生最喜好的问题。

在 1996 年，William McCune 在 Argonne 国家实验室，建造在 Larry Wos、Steve Winker 和 Bob Veroff 的工作之上，肯定的回答了这个长期存在的问题： 所有的 Robbins 代数都是布尔代数。这项工作是使用 McCune 的自动推理程序 EQP 完成的。