View source for Robbins equation

{{TEX|done}}
Researchers have long been interested in finding simple axiomatizations of theories, including [[Boolean algebra|Boolean algebra]]. Boolean algebra can be axiomatized in many different ways using various sets of operations. The ordinary operations of Boolean algebra are disjunction ($+$), conjunction ($*$), negation ($'$), zero ($0$), and one ($1$). One of the first simple axiomatizations was presented by E.V. Huntington in 1933 [[#References|[a3]]]:

(Commutativity) $x+y=y+x$;

(Associativity) $(x+y)+z=x+(y+z)$;

(Huntington) $((x'+y)'+(x'+y')')=x$. From these three equations, one can prove the existence of a zero and a one, and when conjunction is defined (as $x*y\doteq(x'+y')'$), one can prove all of the properties of Boolean algebra.

Shortly thereafter, Huntington's student H. Robbins conjectured that the Huntington equation can be replaced by the following equation, which is simpler by one occurrence of the negation symbol:

(Robbins) $((x+y)'+(x'+y)')'=y$. Neither Robbins nor Huntington could find a proof or a counterexample. The theory given by the three equations $\{\mathrm{Commutativity},\mathrm{Associativity},\mathrm{Robbins}\}$ became known as Robbins algebra, and the question whether $\{\mathrm{Commutativity},\mathrm{Associativity},\mathrm{Robbins}\}$ would imply Huntington became known as the Robbins problem. The problem became a favourite of A. Tarski, who gave it to many of his students and colleagues, but it remained unsolved until 1996.

It is not difficult to show that every finite Robbins algebra satisfies the Huntington equation and that every Robbins algebra satisfying $x''=x$ satisfies the Huntington equation. A bit more difficult is showing that any of the following properties of Boolean algebra is also sufficient:

$x+x=x$;

$\exists0(x+0=x)$;

$\exists1(x+1=1)$. An important step was taken in 1982, when S. Winker showed (by hand) that every Robbins algebra satisfying the (very weak) condition $\exists c\exists d(c+d)'=c'$ also satisfies the Huntington equation [[#References|[a6]]].

From 1980 through 1996, many attempts were made, with and without computers, to solve the problem. The attempts with computers relied on automated theorem-proving programs, such as OTTER, for first-order logic with equality. A new theorem prover EQP [[#References|[a2]]] featuring associative-commutative unification was written in the early 1990s. Associative-commutative unification (AC unification) [[#References|[a5]]] builds the properties of associativity and commutativity of binary functions into the inference processes so that those properties need not be used explicitly to make inferences. The main advantage of AC unification is that expressions can be stored and used in a canonical form rather than in various commuted and associated forms. The main disadvantage is that a pair of expressions can be AC-unified in an enormous number of ways. To address this particular problem, a heuristic was developed that uses only the simplest AC unifiers, reducing the number of inferences from a pair of equations, in some cases from millions to tens. The heuristic is incomplete (i.e., it can block all paths to a proof), but it is valuable in practice. A second important feature of EQP is the  "basic"  restriction on paramodulation [[#References|[a1]]], which reduces redundancy in the search for a proof.

In 1996, a series of experiments was designed to attack the Robbins problem with EQP. Proof searches were conducted with various combinations of parameters to the program, including use of the AC heuristic and the  "basic"  restriction, limits on the size of equations, and strategies for selecting the next equations for making inferences. After fourteen multi-day searches, using a total of about five CPU-weeks of computer time, a proof was found. The successful search, which took about eight CPU-days, produced a proof of Winker's condition $\exists c\exists d(c+d)'=c'$ from $\{\mathrm{Commutativity},\mathrm{Associativity},\mathrm{Robbins}\}$. Because Winker's condition is sufficient to derive the Huntington equation, the Robbins problem had been solved. In subsequent searches, EQP was able to derive the Huntington equation directly. Details of the work and a proof can be found in [[#References|[a4]]].

The proof was accepted as correct after being checked by hand and by several independent proof-checking programs. Mathematicians and logicians have carefully studied EQPs proofs, but little insight into the nature of the problem has been gained. All presently known proofs (as of 2000) of the Robbins conjecture are based on EQPs proofs.

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  L. Bachmair,   H. Ganzinger,   C. Lynch,   W. Snyder,   "Basic paramodulation and superposition"  D. Kapur (ed.) , ''Proc. 11th Internat. Conf. Automated Deduction'' , ''Lecture Notes in Artificial Intelligence'' , '''607''' , Springer  (1992)  pp. 462–476</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  W. McCune,   "33 basic test problems: A practical evaluation of some paramodulation strategies"  R. Veroff (ed.) , ''Automated Reasoning and its Applications: Essays in Honor of Larry Wos'' , MIT  (1997)  pp. 71–114</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  E.V. Huntington,   "New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell's Principia Mathematica"  ''Trans. Amer. Math. Soc.'' , '''35'''  (1933)  pp. 274–304</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  W. McCune,   "Solution of the Robbins problem"  ''J. Automated Reasoning'' , '''19''' :  3  (1997)  pp. 263–276</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  M. Stickel,   "A unification algorithm for associative-commutative functions."  ''J. ACM'' , '''28''' :  3  (1981)  pp. 423–434</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  S. Winker,   "Absorption and idempotency criteria for a problem in near-Boolean algebras"  ''J. Algebra'' , '''153''' :  2  (1992)  pp. 414–423</TD></TR></table>