摘要: In this article we show that the three equations known as commutativity, associativity, and Robbins equation are a basis for variety of Boolean algebras. The problem was posed by Herbert in 1930s. proof found automatically EQP, theorem-proving program equational logic. We present search strategies enabled to find proof.
springer.com
acm.org
sci-hub.se 参考文章(15)
Ewing Lusk, Larry Wos, Jim Boyle, Ross Overbeek, Automated reasoning (2nd ed.): introduction and applications McGraw-Hill, Inc.. ,(1992)
William McCune, 33 basic test problems: a practical evaluation of some paramodulation strategies Automated reasoning and its applications. pp. 71- 114 ,(1997)
Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder, Basic Paramodulation and Superposition conference on automated deduction. pp. 462- 476 ,(1992) , 10.1007/3-540-55602-8_185
W.W. McCune, OTTER 3.0 Reference Manual and Guide Argonne National Laboratory. ,(1994) , 10.2172/10129052
Jean-Marie Hullot, Canonical forms and unification 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. pp. 318- 334 ,(1980) , 10.1007/3-540-10009-1_25
Deepak Kapur, David R Musser, Paliath Narendran, None, Only prime superpositions need be considered in the Knuth-Bendix completion procedure Journal of Symbolic Computation. ,vol. 6, pp. 19- 36 ,(1988) , 10.1016/S0747-7171(88)80019-1
D. E. Knuth, P. B. Bendix, Simple Word Problems in Universal Algebras Computational Problems in Abstract Algebra#R##N#Proceedings of a Conference Held at Oxford Under the Auspices of the Science Research Council Atlas Computer Laboratory, 29th August to 2nd September 1967. pp. 342- 376 ,(1983) , 10.1007/978-3-642-81955-1_23
George F. McNulty, UNDECIDABLE PROPERTIES OF FINITE SETS OF EQUATIONS Journal of Symbolic Logic. ,vol. 41, pp. 589- 604 ,(1976) , 10.1017/S0022481200051161
Edward V. Huntington, New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell’s Principia mathematica Transactions of the American Mathematical Society. ,vol. 35, pp. 274- 304 ,(1933) , 10.1090/S0002-9947-1933-1501684-X
S. Winker, Robbins algebra: conditions that make a near-boolean algebra boolean Journal of Automated Reasoning. ,vol. 6, pp. 465- 489 ,(1990) , 10.1007/BF00244359