Using Mathematica 3.0 to Understand the Computer Proof of the Robbins Conjecture

Branden Fitelson
fitelson@facstaff.wisc.edu


Department of Philosophy
University of Wisconsin–Madison
600 North Park Street
Madison, WI  53706
 

January 20, 1997

Abstract:  In late 1996, Bill McCune et al at Argonne National Laboratory made national headlines (e.g., see Kolata (1996)) with their computer-proof of the long-standing Robbins conjecture.  The Robbins conjecture had stumped some of the world's best mathematicians for over 60 years (e.g., see Tarski et al (1971 Problem 1.1)).  The Argonne team's automated theorem proving program EQP took only 8 days to find a proof of the Robbins conjecture.  Unfortunately, the proof generated by EQP is quite cryptic.  Some of the steps of the EQP proof require highly complex and unintuitive paramodulations, demodulations, etc.  This is where the unique symbolic manipulation, simplification, and visualization capabilities of Mathematica 3.0 come in handy.  With the help of Mathematica 3.0, it is relatively easy to work-out and explain each step of the dense EQP proof in detail.  Presently, I use Mathematica 3.0 to provide a step-by-step explanation of the highly complex EQP proof of the Robbins conjecture.

Introduction
(NOTE:  This historical parts of this introduction were excerpted—almost verbatim—from McCune (1997).  See McCune (1997) for the full story on the recent computer proof of the Robbins conjecture.  Also, check-out Bill McCune’s home page at: http://www.mcs.anl.gov/home/mccune/ar/; and, especially, his “Robbins Algebras are Boolean” page at: http://www.mcs.anl.gov/home/mccune/ar/robbins/ for lots of fascinating information about the Robbins conjecture and automated reasoning in general.)

A Brief History of the Robbins Conjecture
(Excerpted from McCune (1997))

In 1933, E. V. Huntington (1933a and 1933b) presented the following basis for Boolean algebra: 

	x ⊕y = y ⊕x					[Commutativity of ⊕]
	(x ⊕y) ⊕z=x ⊕(y ⊕z)			[Associativity of ⊕]
	(OverBar[\(x\&_\) ⊕y])⊕(OverBar[\(x\&_\) ⊕\(y\&_\)]) =x 				[Huntington equation]

Shortly thereafter, Herbert Robbins (a student of Huntington's) conjectured that if the Huntington equation were replaced with the following equation (which, in algebraic jargon, is the dual of the Huntington equation): 

	(OverBar[(OverBar[x ⊕y])⊕(OverBar[x ⊕\(y\&_\)])]) =x				[Robbins equation]

then the resulting axiomatization would also be characteristic of Boolean algebra.  This is the Robbins conjecture.  Robbins and Huntington could not find a proof of the Robbins conjecture, and the problem was later studied by Tarski (1971) and his students. 

Algebras satisfying commutativity, associativity, and the Robbins equation are known as Robbins algebras.  It is easy to show that every Boolean algebra is a Robbins algebra, so the interesting question is, “Are all Robbins algebras Boolean?”. In other words, can the Huntington equation be derived from commutativity, associativity, and the Robbins equation? 

In 1979, S. Winker learned of the problem from his advisor J. Berman. L. Wos suggested that Winker attack the problem by studying Boolean conditions, such as idempotence or existence of a zero, that might make a Robbins algebra Boolean.  Many such conditions were found.  Several, such as each of:

	(∀ x)  \(\(x\&_\)\&_\)=x					[Double negation]
	(∃ 𝕫) (∀ x)  x ⊕𝕫=x			[Existence of a zero]
	(∀ x)  x ⊕x=x				[Universal idempotence]

were easily shown by Argonne’s theorem provers to make a Robbins algebra Boolean.  Winker (1992) then showed that each of the conditions:

	(∃ C) (∃ D)  C ⊕D = C			[First Winker condition]
	(∃ C) (∃ D)  (OverBar[C ⊕D])=(OverBar[C])			[Second Winker condition]

also suffices, with proofs by hand using insight from theorem prover searches. In 1992 and 1996, respectively, the two Winker conditions were shown automatically (by the Argonne team) to be sufficient. 

Since the early 1980s, the problem has received continued attention from mathematicians and computer scientists, but until now there has been no significant mathematical progress on the problem. (Winker’s work was done in the early 1980s but not published until the early 1990s)

The Computer Proof of the Robbins Conjecture
(Excerpted from McCune (1997))

The proof that solves the Robbins problem was found October 10, 1996, by Bill McCune et al at Argonne (see McCune (1997) for details), using their mechanical theorem prover EQP.   EQP is similar in many ways to the more well known Argonne theorem prover Otter. The main differences are that EQP has associative-commutative (AC) unification, is restricted to equational logic, and offers more paramodulation strategies. (See Argonne’s automated reasoning page at: http://www.mcs.anl.gov/home/mccune/ar/ for more about EQP and Otter. See, also, Wos et al (1992) for a general introduction to the theory and practice of automated reasoning). 

EQP proved that every Robbins algebra satisfies the second Winker condition, by refuting (with built in AC unification) the following pair of assumptions: 

	\(\(\(x⊕y\)\&_⊕\(x⊕y\&_\)\&_
                  \)\&_\  = x\)				[Robbins equation]
	(OverBar[x ⊕y])≠(OverBar[x]) 					[Denial of Second Winker condition]

It follows immediately from this and the Winker (1992) lemma that all Robbins algebras are Boolean (i.e., that the Robbins conjecture is true).  The successful proof search took about 8 days on an RS/6000 processor and used about 30 megabytes of memory.

How Mathematica 3.0 Can Help Us Understand the EQP Proof of the Robbins Conjecture

The original EQP proof of the Second Winker Condition (which, together with lemmas due to Winker (1992), entails the Robbins conjecture) is an extrememly cryptic 16-line proof.  As you'll see in the next section, EQP provides very little information about exactly how each step of the proof is supposed to follow from previous steps.  Moreover, some of the paramodulations, demodulations, simplifications, etc. required to go from one step to another are extrememly complex.  Indeed, many of the steps are far too complex for an average human to ever work-out by hand.  This is where the unique capabilities of Mathematica 3.0 come into play.

Mathematica 3.0, with its unique powers of symbolic manipulation, makes it possible for a human being to work-out the details of the EQP proof of the Robbins conjecture in finite time.  Using Mathematica 3.0, I was able to work through the EQP proof in only a couple of days.  Below, I present my detailed version of the EQP proof of the Robbins conjecture. As you will see, Mathematica’s combination of sophistcated symbolic manipulation/visualization features and traditional mathematical notation input/ouput capability make it almost easy to see how the highly complex EQP proof works.

The Original 16-line Proof of the Robbins Conjecture found by EQP
(translated into Mathematica 3.0 Notation)

Below, I have included a Mathematica 3.0 translation of the entire EQP proof output (the actual EQP ouput of this proof can be obtained from the following URL: http://www.mcs.anl.gov/home/mccune/ar/robbins/eqp-theorem.proof.txt).  The bracketed remarks are the only information EQP gives us concerning how each line can be obtained from previous lines in the proof.  As you will see in the next section, these “hints” are very sketchy, indeed (but, with Mathematica’s help, these sketchy “hints” provide sufficient information for us to reconstruct the details of the proof).

LINE1.  \(TraditionalForm
      \`\(\(x\ ⊕y\)\&_\ 
            ⊕\(y\ ⊕x\&_\)\&_\)\&_ == y\)
			[Assumption:  the Robbins Equation (commutativity and associativity of ⊕ 
			are tacitly assumed throughout)]
			
LINE2.  \(TraditionalForm
      \`\(y\ ⊕\(y\ ⊕\ x\&_\ ⊕\ 
                \(x\ ⊕y\)\&_\)\&_\)\&_ == 
        \(x\ ⊕y\)\&_\)
			[Obtained via some paramodulation from LINE1 into itself]
			
LINE3.  \(TraditionalForm
      \`\(y\ ⊕\(x\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ == 
        \(y\ ⊕x\&_\)\&_\)
			[Obtained via some paramodulation from LINE1 into itself]

LINE4.  \(TraditionalForm
      \`\(\(y\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕y\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ == y\)
			[Obtained via some paramodulation from LINE3 into LINE1]

LINE5.  \(TraditionalForm
      \`\(\(y\ ⊕z\)\&_\ 
            ⊕\(z\ ⊕\(y\ ⊕x\&_\)\&_\ 
                ⊕\(x\ ⊕y\ ⊕y\ 
                    ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
           == z\)
			[Obtained via some paramodulation from LINE4 into LINE1]

LINE6.  \(TraditionalForm
      \`\(y\ ⊕\(x\ ⊕y\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\ 
                ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ == 
        \(y\ ⊕x\&_\)\&_\)
			[Obtained via some paramodulation from LINE4 into LINE1]

LINE7.  \(TraditionalForm
      \`\(\(y\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕y\ ⊕y\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\ 
                ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ == y\)
			[Obtained via some paramodulation from LINE6 into LINE1]

LINE8.  \(TraditionalForm
      \`\(z\ ⊕\(z\ ⊕\(y\ ⊕z\)\&_\ 
                ⊕\(y\ ⊕x\&_\)\&_\ 
                ⊕\(x\ ⊕y\ ⊕y\ 
                    ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
           == \(y\ ⊕z\)\&_\)
			[Obtained via some paramodulation from LINE5 into LINE1]

LINE9.  \(TraditionalForm
      \`\(\(u\ ⊕\(y\ ⊕z\)\&_\)\&_\ 
            ⊕\(\ 
              u\ ⊕z\ 
                ⊕\(z\ ⊕\(y\ ⊕z\)\&_\ 
                    ⊕\(y\ ⊕x\&_\)\&_\ 
                    ⊕\(x\ ⊕y\ ⊕y\ 
                        ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_
                  \)\&_\)\&_ == u\)
			[Obtained via some paramodulation from LINE8 into LINE1]

LINE10.  \(TraditionalForm
      \`\(x\ ⊕\(x\ ⊕x\ ⊕x\ 
                ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ == 
        \(x\ ⊕x\&_\)\&_\)
			[Obtained via (1) some paramodulation from LINE2 into LINE9, in conjunction
			with (2) some demodulation using LINE1]

LINE11.  \(TraditionalForm
      \`\(\(y\ ⊕\(x\ ⊕x\&_\)\&_\)\&_\ 
            ⊕\(x\ ⊕y\ 
                ⊕\(x\ ⊕x\ ⊕x\ 
                    ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
           == y\)
			[Obtained via some paramodulation from LINE10 into LINE1]

LINE12.  \(TraditionalForm
      \`\(\(x\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕x\ ⊕x\ ⊕x\ 
                ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ == x\)
			[Obtained via some paramodulation from LINE10 into LINE1]

LINE13.  \(TraditionalForm
      \`\(x\ ⊕\(x\ ⊕x\ ⊕x\ ⊕x
                \ ⊕\(x\ ⊕x\&_\)\&_\ 
                ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ == 
        \(x\ ⊕x\&_\)\&_\)
			[Obtained via some paramodulation from LINE12 into LINE1]

LINE14.  \(TraditionalForm
      \`\(\(y\ ⊕\(x\ ⊕x\&_\)\&_\)\&_\ 
            ⊕\(x\ ⊕y\ 
                ⊕\(x\ ⊕x\ ⊕x\ 
                    ⊕x\ ⊕\(x\ ⊕x\&_\)\&_\ 
                    ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
           == y\)
			[Obtained via some paramodulation from LINE13 into LINE1]

LINE15.  \(TraditionalForm
      \`\(x\ ⊕\(x\ 
                ⊕\(x\ ⊕x\ ⊕x\ 
                    ⊕\(x\ ⊕x\&_\)\&_\)\&_\ 
                ⊕\(x\ ⊕x\ ⊕x\ 
                    ⊕x\ ⊕\(x\ ⊕x\&_\)\&_\ 
                    ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
           == \(x\ ⊕x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_\)
			[Obtained via some paramodulation from LINE7 into LINE11]

LINE16.  \(TraditionalForm
      \`\(x\ ⊕x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_ == 
        \(x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_\)
			[Obtained via (1) some paramodulation from LINE4 into LINE14, in conjunction
			with (2) some demodulation using LINE15]

Using Mathematica 3.0 to Decipher the EQP Proof of the Robbins Conjecture

Encoding The Robbins Axioms in Mathematica 3.0

Encoding the Commutativity and Associativity of ⊕

We can tell Mathematica to assume only that ⊕ is commutative (or, in Mathematica-ese, Orderless) and associative (or, in Mathematica-ese, Flat), as follows:

\(\(\(Attributes[CirclePlus]\  = \ {Orderless, \ Flat}; \)
\)\)

Below, I will just let Mathematica automatically make use of the commutativity and associativity of ⊕.  I will not explicitly announce which steps depend on these two basic properties of ⊕.

Encoding the Robbins Equation—Two Handy Mathematica Constructs

The two-place function RF[x,y]  allows us to re-write x in an equivalent way, as permitted by the Robbins equation (i.e., RF[x,y] =  \(\(\(x⊕y\)\&_⊕\(x⊕y\&_\)\&_
                    \)\&_\)  (= x), for any y).  The replacement rule RR allows us to replace all occurrences of the pattern \(\(\(x⊕y\)\&_⊕\(x⊕y\&_\)\&_
                  \)\&_\) with x, in any Mathematica expression ℰ.

RF[x_, y_]:=(OverBar[(OverBar[x⊕y])⊕ (OverBar[x⊕\(y\&_\)])]);
RR:={(OverBar[(OverBar[x__⊕y__])⊕ (OverBar[x__⊕\(y__\&_\)])])->x};

Here is an example which illustrates how RF and RR allow us to expand/simplify Mathematica expressions in accordance with the Robbins equation.

testRF =RF[a, b]⊕ RF[b, a]

testRR =( testRF //. RR)

In this sense, RR can be used as a sort of “inverse” of RF.  These two Mathematica constructs will prove quite useful, as you will see below.

Now that we have properly encoded commutativity, associatvity and the Robbins equation in Mathematica 3.0, we are ready to tackle the EQP proof of The Second Winker Condition, line-by-line.

Deciphering the EQP Proof of The Second Winker Condition: Line–By–Line

Line 1 of the EQP Proof—The Robbins Equation

Line 1 of the EQP proof is just the Robbins equation, as discussed above:

LINE1=\(\(\(x⊕y\)\&_⊕\(y⊕x\&_\)\&_\)\&_
             == y\)

Line 2 of the EQP Proof—The first (of many) cryptic paramodulations

Line 2 of the EQP proof is:

LINE2=\(\(y⊕\(y
                  ⊕x\&_⊕\(x⊕y\)\&_\)\&_
                \)\&_ == \(x⊕y\)\&_\)

All the EQP proof tells us is that LINE2 can be obtained via some paramodulation from LINE1 into itself.  Using RF and RR, we can straightforwardly verify that LINE2 is the following paramodulation from the Robbins equation into itself.

\(LINE2 == 
        \((RF[\(x⊕y\)\&_, x\&_⊕y] == 
            \(x⊕y\)\&_)\) //. RR\)

Or, equivalently, we can use RR alone to verify that LINE2 is the following substitution instance of LINE1.

\(LINE2 == 
        \((LINE1 /. {x -> x\&_⊕y, 
              y -> \(x⊕y\)\&_})\) //. RR\)

In other words, LINE2 can be obtained by representing (i.e., logically expanding) \(TraditionalForm\`\(x\ ⊕y\)\&_\) in terms of \(TraditionalForm\`x\&_\ ⊕y\), in accordance with the Robbins equation.     □

Line 3 of the EQP Proof

Line 3 of the EQP proof is:

LINE3=\(\(y⊕\(x⊕y
                  ⊕\(y⊕x\&_\)\&_\)\&_\)\&_ == 
          \(y⊕x\&_\)\&_\)

Again the EQP proof says only that LINE3 can be obtained via some paramodulation from LINE1 into itself.  Using RF and RR, it is relatively easy to see that LINE3 is the following paramodulation from the Robbins equation into itself.

\(LINE3 == 
        \((RF[\(y⊕x\&_\)\&_, y⊕x] == 
            \(y⊕x\&_\)\&_)\) //. RR\)

Or, equivalently, we can use RR alone to verify that LINE3 is the following substitution instance of LINE1.

\(LINE3 == 
        \((LINE1 /. {x -> y⊕x, 
              y -> \(y⊕x\&_\)\&_})\) //. RR\)

In other words, LINE3 can be obtained by representing (i.e., logically expanding) \(TraditionalForm\`\(y\ ⊕x\&_\)\&_\) in terms of y ⊕x, in accordance with the Robbins equation.     □

The function L3F allows us to re-write expressions of the form \(TraditionalForm\`\(y\ ⊕x\&_\)\&_\) in the more complex (but, as we just proved, equivalent) form \(TraditionalForm
      \`\(y\ ⊕\(x\ ⊕y\ 
              ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\).  L3F will come in handy in our proof of LINE4, below.

\(\(L3F[\(y__⊕x__\&_\)\&_] := 
      \(y⊕\(x⊕y
              ⊕\(y⊕x\&_\)\&_\)\&_\)\&_; \)\)

Line 4 of the EQP Proof

Line 4 of the EQP proof is:

LINE4 = \(\(\(y⊕x\&_\)\&_
                ⊕\(x⊕y⊕y
                  ⊕\(y⊕x\&_\)\&_\)\&_\)\&_ == y\)

The EQP proof says only that LINE4 can be obtained via some paramodulation from LINE3 into LINE1.  With L3F, RF, and RR in hand, it is easy to verify that LINE4 is the following paramodulation from LINE3 into LINE1.

LINE4 == (L3F[RF[y, x]] == y) //. RR

The trick here is to recognize that the left-hand side of LINE1 (i.e., \(TraditionalForm
      \`\(\(x\ ⊕y\)\&_\ 
          ⊕\(y\ ⊕x\&_\)\&_\)\&_\)) is itself an instance of the right-hand side of LINE3 (i.e., \(TraditionalForm
      \`\(𝕪\ ⊕𝕩\&_\)\&_\), where \(TraditionalForm\`𝕪 = \(y\ ⊕x\&_\)\&_\), and 𝕩 = x ⊕y).  This allows us to re-write \(TraditionalForm
      \`\(\(x\ ⊕y\)\&_\ 
            ⊕\(y\ ⊕x\&_\)\&_\)\&_ = y\) equivalently as \(TraditionalForm
      \`\(\(y\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\ 
                ⊕\(\(x\ ⊕y\)\&_\ 
                    ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_ = 
        y\), in accordance with LINE3.  Finally, the Robbins equation allows us to transform \(TraditionalForm
      \`\(\(y\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\ 
                ⊕\(\(x\ ⊕y\)\&_\ 
                    ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_ = 
        y\) into the desired identity \(TraditionalForm
      \`\(\(y\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕y\ ⊕y\ 
                ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ = y\) (we did this automatically using RR).     □

Line 5 of the EQP Proof

Line 5 of the EQP proof is:

LINE5 = \(\(\(y⊕z\)\&_
                ⊕\(z
                  ⊕\(y⊕x\&_\)\&_
                    ⊕\(x⊕y⊕y
                      ⊕\(y⊕x\&_\)\&_\)\&_\)\&_\)\&_
             == z\)

The EQP proof says only that LINE5 can be obtained via some paramodulation from LINE4 into LINE1.  To see the relevant paramodulation, let 𝕒 = \(TraditionalForm
      \`\(y\ ⊕x\&_\)\&_\ 
        ⊕\(x\ ⊕y\ ⊕y\ 
            ⊕\(y\ ⊕x\&_\)\&_\)\&_\).  Then, LINE5 becomes LINE5†:

\(LINE5† = 
      LINE5 //. {
          \(y⊕x\&_\)\&_
                ⊕\(x⊕y⊕y
                  ⊕\(y⊕x\&_\)\&_\)\&_ -> 
            𝕒}\)

From LINE4, we know that \(TraditionalForm
      \`y = \(\(\(y\ ⊕x\&_\)\&_\ 
              ⊕\(x\ ⊕y\ ⊕y\ 
                  ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          𝕒\&_\)\).  Substituting \(TraditionalForm\`𝕒\&_\) for y in LINE5† yields:

\(LINE5†† = 
      LINE5† //. {y -> 𝕒\&_}\)

Which is an obvious instance of LINE1 (i.e., the Robbins equation).     □

Line 6 of the EQP Proof

Line 6 of the EQP proof is:

\(LINE6\  = 
      \(y⊕\(x⊕y⊕y
                ⊕\(y⊕x\&_\)\&_
                  ⊕\(y⊕x\&_\)\&_\)\&_\)\&_ == 
        \(y⊕x\&_\)\&_\)

The EQP proof says only that LINE6 can be obtained via some paramodulation from LINE4 into LINE1.  To see the relevant paramodulation here, let 𝕓 = \(TraditionalForm
      \`x\ ⊕y\ ⊕y\ 
        ⊕\(y\ ⊕x\&_\)\&_\).  Then, LINE6 becomes LINE6†:

\(LINE6† = 
      LINE6 //. {
          x⊕y⊕y⊕\(y⊕x\&_\)\&_ 
            -> 𝕓}\)

From LINE4, we know that \(TraditionalForm
      \`y = \(\(\(y\ ⊕x\&_\)\&_\ 
              ⊕\(x\ ⊕y\ ⊕y\ 
                  ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(𝕓\&_⊕\(y⊕x\&_\)\&_\)\&_
            \)\).  Substituting \(TraditionalForm
      \`\(𝕓\&_\ ⊕\(y\ ⊕x\&_\)\&_\)\&_
        \) for the first occurrence of y in LINE6† yields:

\(LINE6†† = 
      \(\(𝕓\&_⊕\(y⊕x\&_\)\&_\)\&_
              ⊕\(𝕓⊕\(y
                    ⊕x\&_\)\&_\)\&_\)\&_ == 
        \(y⊕x\&_\)\&_\)

Which is a relatively obvious instance of LINE1, as the test below confirms.

LINE6†† //. RR

True       \[Square]

Line 7 of the EQP Proof

Line 7 of the EQP proof is:

\(LINE7\  = \ 
      \(\(y⊕x\&_\)\&_
              ⊕\(x⊕y⊕y⊕y
                ⊕\(y⊕x\&_\)\&_
                  ⊕\(y⊕x\&_\)\&_\)\&_\)\&_ == y\)

The EQP proof says only that LINE7 can be obtained via some paramodulation from LINE6 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕔 = 
        x\ ⊕y\ ⊕y\ 
          ⊕\(y\ ⊕x\&_\)\&_\ 
          ⊕\(y\ ⊕x\&_\)\&_\).  Then, LINE7 becomes:

\(LINE7† = 
      LINE7 //. {
          x⊕y⊕y
              ⊕\(y⊕x\&_\)\&_
                ⊕\(y⊕x\&_\)\&_ -> 
            𝕔}\)

And, from LINE6, we know that \(TraditionalForm
      \`\(y\ ⊕x\&_\)\&_ = 
        \(\(y\ ⊕\(x\ ⊕y\ ⊕y\ 
                  ⊕\(y\ ⊕x\&_\)\&_\ 
                  ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(y\ ⊕𝕔\&_\)\&_\)\).  Substituting \(TraditionalForm\`\(y\ ⊕𝕔\&_\)\&_\) for \(TraditionalForm\`\(y\ ⊕x\&_\)\&_\)  in LINE7† yields:

\(LINE7†† = 
      LINE7† //. {
          \(y⊕x\&_\)\&_ -> 
            \(y⊕𝕔\&_\)\&_}\)

Which is an obvious instance of LINE1.     □

Line 8 of the EQP Proof

Line 8 of the EQP proof is:

\(LINE8\  = 
      \(z⊕\(z
                ⊕\(y⊕z\)\&_
                  ⊕\(y⊕x\&_\)\&_
                  ⊕\(x⊕y⊕y
                    ⊕\(y⊕x\&_\)\&_\)\&_\)\&_\)\&_ == 
        \(y⊕z\)\&_\)

The EQP proof says only that LINE8 can be obtained via some paramodulation from LINE5 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕕 = 
        \(y\ ⊕x\&_\)\&_\ 
          ⊕\(x\ ⊕y\ ⊕y\ 
              ⊕\(y\ ⊕x\&_\)\&_\)\&_\).  Then, LINE8 becomes LINE8†:

\(LINE8† = 
      LINE8 //. {
          \(y⊕x\&_\)\&_
                ⊕\(x⊕y⊕y
                  ⊕\(y⊕x\&_\)\&_\)\&_ -> 
            𝕕}\)

And, from LINE5, we know that \(TraditionalForm
      \`z = \(\(\(y\ ⊕z\)\&_\ 
              ⊕\(z\ ⊕\(y\ ⊕x\&_\)\&_\ 
                  ⊕\(x\ ⊕y\ ⊕y\ 
                      ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
             = \(\(y\ ⊕z\)\&_\ 
              ⊕\(z\ ⊕𝕕\)\&_\)\&_\)\).  Substituting \(TraditionalForm
      \`\(\(y\ ⊕z\)\&_\ 
          ⊕\(z\ ⊕𝕕\)\&_\)\&_\)  for the first instance of z in  LINE8† yields:

\(LINE8†† = 
      \(\(\(y⊕z\)\&_
                  ⊕\(z⊕𝕕\)\&_\)\&_
              ⊕\(z
                ⊕𝕕⊕\(y⊕z
                    \)\&_\)\&_\)\&_ == \(y⊕z\)\&_\)

Which is the following substitution instance of LINE1.     □

\(LINE1
       /. {y -> \(y⊕z\)\&_, 
        x -> z⊕𝕕}\)

Line 9 of the EQP Proof

Line 9 of the EQP proof is:

LINE9 = \(\(\(u⊕\(y⊕z\)\&_\)\&_
                ⊕\(u⊕z
                  ⊕\(z
                      ⊕\(y⊕z\)\&_
                        ⊕\(y⊕x\&_\)\&_
                        ⊕\(x⊕y⊕y
                          ⊕\(y⊕x\&_\)\&_\)\&_\)\&_
                    \)\&_\)\&_ == u\)

The EQP proof says only that LINE9 can be obtained via some paramodulation from LINE8 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕖 = 
        \(y\ ⊕z\)\&_\ ⊕\(y\ ⊕x\&_\)\&_\ 
          ⊕\(x\ ⊕y\ ⊕y\ 
              ⊕\(y\ ⊕x\&_\)\&_\)\&_\).  Then, LINE9 becomes:

\(LINE9† = 
      LINE9 //. {
          \(y⊕z\)\&_⊕\(y⊕x\&_\)\&_
                ⊕\(x⊕y⊕y
                  ⊕\(y⊕x\&_\)\&_\)\&_ -> 
            𝕖}\)

From LINE8, we know that \(TraditionalForm
      \`\(y\ ⊕z\)\&_ = 
        \(\(z\ ⊕\(z\ ⊕\(y\ ⊕z\)\&_\ 
                  ⊕\(y\ ⊕x\&_\)\&_\ 
                  ⊕\(x\ ⊕y\ ⊕y\ 
                      ⊕\(y\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
             = \(z\ ⊕\(z\ ⊕𝕖\)\&_\)\&_
            \)\).  Substituting \(TraditionalForm
      \`\(z\ ⊕\(z\ ⊕𝕖\)\&_\)\&_\)  for  \(TraditionalForm\`\(y\ ⊕z\)\&_\)  in  LINE9† yields:

\(LINE9†† = 
      LINE9† //. {
          \(y⊕z\)\&_ -> 
            \(z⊕\(z⊕𝕖\)\&_\)\&_}\)

Which is the following substitution instance of LINE1.     □

\(LINE1
       /. {y -> u, 
        x -> z⊕\(z⊕𝕖\)\&_}\)

Line 10 of the EQP Proof

Line 10 of the EQP proof is:

\(LINE10\  = 
      \(x⊕\(x⊕x⊕x
                ⊕\(x⊕x\&_\)\&_\)\&_\)\&_ == 
        \(x⊕x\&_\)\&_\)

The EQP proof tells us only that LINE10 can be obtained via (1) some paramodulation from LINE2 into LINE9, in conjunction with (2) some Demodulation, using LINE1 (i.e., the Robbins equation).  To see the relevant paramodulations and demodulations, let \(TraditionalForm\`𝕗 = \(x\ ⊕x\&_\)\&_\).  Then, LINE10 becomes:

\(LINE10† = 
      LINE10 /. {\(x⊕x\&_\)\&_ -> \ 𝕗}\)

And, from LINE2, we know that \(TraditionalForm
      \`\(x\ ⊕x\ ⊕x\ 
            ⊕𝕗\)\&_ = 
        \(x\ ⊕𝕗⊕\(x\ 
                ⊕𝕗⊕\(x\ ⊕x
                    \)\&_\ ⊕\(x\ ⊕x\ ⊕x\ 
                    ⊕𝕗\)\&_\)\&_\)\&_\).  To see this, perform the following pair of substitutions on LINE2:

LINE2† = 
      LINE2 /. {x -> x⊕x, 
          y -> x⊕𝕗}

Substituting \(TraditionalForm
      \`\(x\ ⊕𝕗⊕\(x\ 
              ⊕𝕗⊕\(x\ ⊕x
                  \)\&_\ ⊕\(x\ ⊕x\ ⊕x\ 
                  ⊕𝕗\)\&_\)\&_\)\&_\)  for  \(TraditionalForm
      \`\(x\ ⊕x\ ⊕x\ 
          ⊕𝕗\)\&_\)  in LINE10† yields:

\(LINE10†† = 
      LINE10† /. {
          \(x⊕x⊕x⊕𝕗\)\&_ 
            -> \(x
                ⊕𝕗⊕\(x
                    ⊕𝕗⊕\(x
                        ⊕x\)\&_
                      ⊕\(x⊕x⊕x
                        ⊕𝕗\)\&_\)\&_\)\&_}\)

It is not terribly obvious to the naked-eye; but, LINE10†† is a substitution instance of LINE9.  To see this, perform the following quadruple of substitutions on LINE9:

\(LINE9† = 
      LINE9 //. {u -> \(x⊕x\&_\)\&_, x -> x, 
          y -> x, z -> x}\)

Now, if we replace \(TraditionalForm\`\(x\ ⊕x\&_\)\&_\) with 𝕗 (as assumed above) throughout LINE9†, we get:

\(LINE9†† = 
      LINE9† //. {
          \(x⊕x\&_\)\&_ -> \ 𝕗}\)

Moreover, from LINE1 and the definition of 𝕗, we know that \(TraditionalForm
      \`\(𝕗⊕\(x\ ⊕x\)\&_\)\&_ = 
        \(\(\(x\ ⊕x\)\&_\ 
              ⊕\(x\ ⊕x\&_\)\&_\)\&_ = x\)\).  Finally, substituting x for \(TraditionalForm
      \`\(𝕗⊕\(x\ ⊕x\)\&_\)\&_\) in LINE9†† yields:

\(LINE9††† = 
      LINE9†† //. {
          \(𝕗⊕\(x⊕x\)\&_\)\&_ -> 
            x}\)

To complete the proof of LINE10, we verify that LINE10†† = LINE9†††:

LINE10†† == LINE9†††

True      \[Square]

Line 11 of the EQP Proof

Line 11 of the EQP proof is:

LINE11 =\(\(\(y⊕\(x⊕x\&_\)\&_\)\&_
                ⊕\(x⊕y
                  ⊕\(x⊕x⊕x
                      ⊕\(x⊕x\&_\)\&_\)\&_\)\&_\)\&_
             == y\)

The EQP proof says only that LINE11 can be obtained via some paramodulation from LINE10 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕘 = 
        \(x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_\).  Then, LINE11 becomes:

\(LINE11† = 
      LINE11 //. {
          \(x⊕x⊕x
                ⊕\(x⊕x\&_\)\&_\)\&_ -> 
            𝕘}\)

\(\(x⊕\(x⊕x⊕x
                ⊕\(x⊕x\&_\)\&_\)\&_\)\&_ == 
        \(x⊕x\&_\)\&_ //. {
        \(x⊕x⊕x
              ⊕\(x⊕x\&_\)\&_\)\&_ -> 
          𝕘}\)

Furthermore, from LINE10, we know that \(TraditionalForm
      \`\(x\ ⊕x\&_\)\&_ = 
        \(\(x\ ⊕\(x\ ⊕x\ ⊕x\ 
                  ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(x\ ⊕𝕘\)\&_\)\).  Substituting \(TraditionalForm\`\(x\ ⊕𝕘\)\&_\) for \(TraditionalForm\`\(x\ ⊕x\&_\)\&_\) in  LINE11† yields:

\(LINE11†† = 
      LINE11† //. {
          \(x⊕x\&_\)\&_ -> 
            \(x⊕𝕘\)\&_}\)

Which is the following substitution instance of LINE1.     □

LINE1 /. {y -> y, x -> x⊕𝕘}

Line 12 of the EQP Proof

Line 12 of the EQP proof is:

LINE12 =\(\(\(x⊕x\&_\)\&_
                ⊕\(x⊕x⊕x⊕x
                  ⊕\(x⊕x\&_\)\&_\)\&_\)\&_ == x\)

The EQP proof says only that LINE12 can be obtained via some paramodulation from LINE10 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕙 = 
        x\ ⊕x\ ⊕x\ 
          ⊕\(x\ ⊕x\&_\)\&_\).  Then, LINE12 becomes:

\(LINE12† = 
      LINE12 //. {
          x⊕x⊕x⊕\(x⊕x\&_\)\&_ 
            -> 𝕙}\)

But, from LINE10, we know that \(TraditionalForm
      \`\(x\ ⊕x\&_\)\&_ = 
        \(\(x\ ⊕\(x\ ⊕x\ ⊕x\ 
                  ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(x\ ⊕𝕙\&_\)\&_\)\).  Substituting \(TraditionalForm\`\(x\ ⊕𝕙\&_\)\&_\) for \(TraditionalForm\`\(x\ ⊕x\&_\)\&_\) in  LINE12† yields:

LINE12††=LINE12†//.{\(\(x⊕x\&_\)\&_ -> 
            \(x⊕𝕙\&_\)\&_\)}

Which is an obvious instance of LINE1.  □

Line 13 of the EQP Proof

Line 13 of the EQP proof is:

LINE13 =\(\(x⊕\(x⊕x⊕x⊕x
                  ⊕\(x⊕x\&_\)\&_
                    ⊕\(x⊕x\&_\)\&_\)\&_\)\&_ == 
          \(x⊕x\&_\)\&_\)

The EQP proof says only that LINE13 can be obtained via some paramodulation from LINE12 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕚 = 
        x\ ⊕x\ ⊕x\ ⊕x\ 
          ⊕\(x\ ⊕x\&_\)\&_\).  Then, LINE13 becomes:

\(LINE13† = 
      LINE13 //. {
          x⊕x⊕x⊕x
              ⊕\(x⊕x\&_\)\&_ -> 𝕚}
          \)

From LINE12, we know that \(TraditionalForm
      \`x = \(\(\(x\ ⊕x\&_\)\&_\ 
              ⊕\(x\ ⊕x\ ⊕x\ ⊕x
                  \ ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(𝕚\&_\ ⊕\(x\ ⊕x\&_\)\&_\)\&_
            \)\).  Substituting \(TraditionalForm
      \`\(𝕚\&_\ ⊕\(x\ ⊕x\&_\)\&_\)\&_
        \) for the first occurrence of x in LINE13† yields:

\(LINE13†† = 
      \(\(𝕚\&_⊕\(x⊕x\&_\)\&_\)\&_
              ⊕\(𝕚⊕\(x
                    ⊕x\&_\)\&_\)\&_\)\&_ == 
        \(x⊕x\&_\)\&_\)

Which is the following substitution instance of LINE1.     □

\(LINE1
       /. {y -> \(x⊕x\&_\)\&_, x -> 𝕚}
        \)

Line 14 of the EQP Proof

Line 14 of the EQP proof is:

LINE14 =\(\(\(y⊕\(x⊕x\&_\)\&_\)\&_
                ⊕\(x⊕y
                  ⊕\(x⊕x⊕x⊕x
                      ⊕\(x⊕x\&_\)\&_
                        ⊕\(x⊕x\&_\)\&_\)\&_\)\&_\)\&_
             == y\)

The EQP proof says only that LINE14 can be obtained via some paramodulation from LINE13 into LINE1.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕛 = 
        \(x\ ⊕x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_
              ⊕\(x\ ⊕x\&_\)\&_\)\&_\).  Then, LINE14 becomes:

\(LINE14† = 
      LINE14 //. {
          \(x⊕x⊕x⊕x
                ⊕\(x⊕x\&_\)\&_
                  ⊕\(x⊕x\&_\)\&_\)\&_ -> 
            𝕛}\)

From LINE13, we know that \(TraditionalForm
      \`\(x\ ⊕x\&_\)\&_ = 
        \(\(x\ ⊕\(x\ ⊕x\ ⊕x\ 
                  ⊕x\ ⊕\(x\ ⊕x\&_\)\&_\ 
                  ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(x\ ⊕𝕛\)\&_\)\).  Substituting \(TraditionalForm\`\(x\ ⊕𝕛\)\&_\) for \(TraditionalForm\`\(x\ ⊕x\&_\)\&_\) in  LINE14† yields:

\(LINE14†† = 
      LINE14† //. {
          \(x⊕x\&_\)\&_ -> 
            \(x⊕𝕛\)\&_}\)

Which is the following instance of LINE1.     □

LINE1 /. {y -> y, x -> x⊕𝕛}

Line 15 of the EQP Proof

Line 15 of the EQP proof is:

LINE15 =\(\(x⊕\(x
                  ⊕\(x⊕x⊕x
                      ⊕\(x⊕x\&_\)\&_\)\&_
                    ⊕\(x⊕x⊕x⊕x
                      ⊕\(x⊕x\&_\)\&_
                        ⊕\(x⊕x\&_\)\&_\)\&_\)\&_\)\&_
             == \(x⊕x⊕x⊕x
              ⊕\(x⊕x\&_\)\&_
                ⊕\(x⊕x\&_\)\&_\)\&_\)

The EQP proof says only that LINE15 can be obtained via some paramodulation from LINE7 into LINE11.  To see the relevant paramodulation, let \(TraditionalForm
      \`𝕜 = 
        \(x\ ⊕x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_
              ⊕\(x\ ⊕x\&_\)\&_\)\&_\).  Then, LINE15 becomes:

\(LINE15† = 
      LINE15 //. {
          \(x⊕x⊕x⊕x
                ⊕\(x⊕x\&_\)\&_
                  ⊕\(x⊕x\&_\)\&_\)\&_ -> 
            𝕜}\)

And, from LINE7, we know that \(TraditionalForm
      \`x = \(\(\(x\ ⊕x\&_\)\&_\ 
              ⊕\(x\ ⊕x\ ⊕x\ ⊕x
                  \ ⊕\(x\ ⊕x\&_\)\&_\ 
                  ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(𝕜⊕\(x\ ⊕x\&_\)\&_\)\&_
            \)\).  Substituting \(TraditionalForm
      \`\(𝕜\ ⊕\(x\ ⊕x\&_\)\&_\)\&_\) for the first occurrence of x in  LINE15† yields:

\(LINE15†† = 
      \(\(𝕜⊕\(x⊕x\&_\)\&_\)\&_
              ⊕\(x
                ⊕𝕜⊕\(x⊕x
                    ⊕x⊕\(x⊕x\&_\)\&_\)\&_
                  \)\&_\)\&_ == 𝕜\)

Which is an instance of LINE11.  To see this, perform the following substitution on LINE11.

LINE11†††  =  
      LINE11 //. {y -> 𝕜}

Then, check to see that LINE15†† is equivalent to LINE11†††.

LINE15†† == LINE11†††

True         \[Square]

Line 16 of the EQP Proof—The last line of the proof, finally!!

Line 16 (the last line!) of the EQP proof is:

\(LINE16\  = 
      \(x⊕x⊕x⊕x
            ⊕\(x⊕x\&_\)\&_
              ⊕\(x⊕x\&_\)\&_\)\&_ == 
        \(x⊕x⊕x
            ⊕\(x⊕x\&_\)\&_\)\&_\)

The EQP proof says only that LINE16 can be obtained via (1) some paramodulation from LINE4 into LINE14, in conjunction with (2) some Demodulation, using LINE15.  To see the relevant paramodulations and demodulations, let \(TraditionalForm
      \`𝕝 = 
        x\ ⊕x\ ⊕x\ 
          ⊕\(x\ ⊕x\&_\)\&_\).  Then, LINE16 becomes:

\(LINE16† = 
      LINE16 //. {
          x⊕x⊕x⊕\(x⊕x\&_\)\&_ 
            -> 𝕝\ }\)

From LINE15, we know that \(TraditionalForm
      \`\(x\ ⊕𝕝\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_ = 
        \(x\ ⊕\(x\ ⊕𝕝\&_\ 
                ⊕\(x\ ⊕𝕝\ 
                    ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
          \).  To see this, perform the following substitution on LINE15:

\(LINE15
       //. {x⊕x⊕x
            ⊕\(x⊕x\&_\)\&_ -> 𝕝\ }
        \)

Substituting \(TraditionalForm\`\(\ 
      \(x\ ⊕\(x\ ⊕𝕝\&_\ 
              ⊕\(x\ ⊕𝕝\ 
                  ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_\)\&_
        \)\)  for  \(TraditionalForm
      \`\(x\ ⊕𝕝\ 
          ⊕\(x\ ⊕x\&_\)\&_\)\&_\)  in LINE16† yields:

\(LINE16†† = 
      LINE16† /. {
          \(x⊕𝕝⊕\(x
                    ⊕x\&_\)\&_\)\&_ -> 
            \(x⊕\(x
                    ⊕𝕝\&_
                      ⊕\(x
                        ⊕𝕝⊕\(x
                            ⊕x\&_\)\&_\)\&_\)\&_\)\&_}\)

Moreover, from LINE4, we know that \(TraditionalForm
      \`x = \(\(\(x\ ⊕x\&_\)\&_\ 
              ⊕\(x\ ⊕x\ ⊕x\ 
                  ⊕\(x\ ⊕x\&_\)\&_\)\&_\)\&_ = 
          \(𝕝\&_\ ⊕\(x\ ⊕x\&_\)\&_\)\&_
            \)\).  Substituting \(TraditionalForm
      \`\(𝕝\&_\ ⊕\(x\ ⊕x\&_\)\&_\)\&_
        \) for the first occurrence of x in  LINE16†† yields:

\(LINE16††† = 
      \(\(𝕝\&_⊕\(x⊕x\&_\)\&_\)\&_
              ⊕\(x
                ⊕𝕝\&_
                  ⊕\(x
                    ⊕𝕝⊕\(x
                        ⊕x\&_\)\&_\)\&_\)\&_\)\&_ == 
        𝕝\&_\)

It may not be very obvious to the un-aided observer; but, LINE16††† is a substitution instance of LINE14.  To see this, perform the following pair of substitutions on LINE14.

\(LINE14†††\  = \ 
      LINE14 //. {y -> 𝕝\&_\ , 
          x⊕x⊕x⊕\(x⊕x\&_\)\&_ 
            -> 𝕝}\)

Finally, verify that LINE16††† = LINE14†††.

LINE16††† == 
      LINE14†††

True         \[Square]

What have we just proved?

We have just proved that \(TraditionalForm
      \`\(x\ ⊕x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_ = 
        \(x\ ⊕x\ ⊕x\ 
            ⊕\(x\ ⊕x\&_\)\&_\)\&_\).  To see that The Second Winker Condition (as defined above) follows from this, let \(TraditionalForm
      \`C = x\ ⊕x\ ⊕x\ 
          ⊕\(x\ ⊕x\&_\)\&_\), and \(TraditionalForm\`D = x\ ⊕\(x\ ⊕x\&_\)\&_\).  Then, it is straightforward to verify that LINE16 enatils: \(TraditionalForm\`\(C\ ⊕D\)\&_ = C\&_\), which implies The Second Winker Condition.

\(LINE16
       //. {x⊕x⊕x
            ⊕\(x⊕x\&_\)\&_ -> C, \ 
        x⊕\(x⊕x\&_\)\&_ -> D}\)

\(\(C⊕D\)\&_ == C\&_\)

This concludes our (Mathematica 3.0–aided) deciphering of the EQP proof of the Second Winker Condition. In conjunction with the results previously reported in Winker (1992), this proof establishes that all Robbins algebras are Boolean algebras (i.e., that the Robbins conjecture is correct).        □

References

Huntington, E.V., 1933a, “New sets of independent postulates for the algebra of logic”, Transactions of the American Mathematical Society 35, pages 274–304
       
Huntington, E.V., 1933b, “Boolean algebra: A correction”, Transactions of the American Mathematical Society 35, pages 557–558. 

Kolata, G., 1996, “Computer Math Proof Shows Reasoning Power”, The New York Times, December 10, 1996.

McCune, W., 1997 (in preparation), “Solution of the Robbins Problem”, unpublished manuscript.

Tarski, A., et al, 1971, Cylindric Algebras: Part I, North-Holland.

Winker, S., 1992, “Absorption and idempotency criteria for a problem in near-Boolean algebras”, Journal of Algebra 153(2), pages 414–423.

Wos, L., et al, 1992, Automated Reasoning: Introduction and Applications, Second Edition, McGraw Hill.