交换律: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 完成的。