在 1933 年，美國(guó)數(shù)學(xué)家 edward vermilye huntington (1874-1952) 展示了對(duì)布爾代數(shù)的如下公理化：
交換律：x + y = y + x。
結(jié)合律：(x + y) + z = x + (y + z)。
huntington等式：n(n(x) + y) + n(n(x) + n(y)) = x。
一元函數(shù)符號(hào) n 可以讀做‘補(bǔ)’。
herbert robbins 接著擺出下列問(wèn)題： huntington等式能否縮短為下述的等式，并且這個(gè)新等式與結(jié)合律和交換律一起成為布爾代數(shù)的基礎(chǔ)? 通過(guò)一組叫做 robbins 代數(shù)的公理，問(wèn)題就變成了：是否所有的 robbins 代數(shù)都是布爾代數(shù)?
robbins 代數(shù)的公理化：
交換律： x + y = y + x。
結(jié)合律： (x + y) + z = x + (y + z)。
robbins等式： n(n(x + y') + n(x + n(y))) = x。
這個(gè)問(wèn)題自從 1930 年代一直是公開(kāi)的，并成為 alfred tarski 和他的學(xué)生最喜好的問(wèn)題。
在 1996 年，william mccune 在 argonne 國(guó)家實(shí)驗(yàn)室，建造在 larry wos、steve winker 和 bob veroff 的工作之上，肯定的回答了這個(gè)長(zhǎng)期存在的問(wèn)題： 所有的 robbins 代數(shù)都是布爾代數(shù)。這項(xiàng)工作是使用 mccune 的自動(dòng)推理程序 eqp 完成的。