布尔代数公理化在 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 完成的

以上内容由大学时代综合整理自互联网，实际情况请以官方资料为准。