Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem
Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem
复制标题
罗宾斯代数是布尔值：麦库恩计算机生成的罗宾斯问题解决方案的修订版
DOI：
10.1006/jabr.1998.7467
复制
发表时间：
1998
影响因子：
0.9
通讯作者：
B. Dahn
中科院分区：
文献类型：
--
作者：
B. Dahn
摘要 20世纪30年代初，罗宾斯提出了一个问题：某个方程连同并运算的交换性和结合性是否足以表征布尔代数。 1992 年，Winker 将其简化为根据罗宾斯公理证明另一个方程的可解性问题。 1996年10月，William McCune在自动定理证明器EQP的帮助下证实了Winker的情况。在本文中，我们对 EQP 发现的证明进行了简化介绍。
Abstract In the early 1930s, Robbins asked whether a certain equation together with commutativity and associativity of the union operation was sufficient to characterize Boolean algebras. In 1992, Winker reduced this to the problem of proving the solvability of another equation from Robbins' axioms. In October 1996, William McCune confirmed Winker's condition with the help of the automated theorem prover EQP. In this paper we give a simplified presentation of the proof discovered by EQP.