在 1933 年，美国数学家 edward vermilye huntington (1874-1952) 展示了对布尔代数的如下公理化：
交换律：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 完成的。