Robbins Redux: Using Definitions to Help the Search

This page was written for an informal presentation at ADAM-2007.

The Robbins Problem

formulas(assumptions).

  x + y = y + x                 # label(Commutativity).
  (x + y) + z = x + (y + z)     # label(Associativity).
  ((x + y)' + (x + y')')' = x   # label(Robbins).

end_of_list.

formulas(goals).

  (x + y')' + (x' + y')' = y           # answer(Huntington).

end_of_list.

formulas(goals).  % either of these is sufficient (Steve Winker)

  (exists a exists b (a + b = a))      # answer(Winker1).
  (exists a exists b ((a + b)' = a'))  # answer(Winker2).

end_of_list.

1996: Proof with EQP

EQP Proof (edited: "n" operation changed to " ' ", terms rearranged)

----- EQP 0.9, June 1996 -----
The job began on eyas09.mcs.anl.gov, Wed Oct  2 12:25:37 1996
UNIT CONFLICT from 17666 and 2 at 678232.20 seconds.

---------------- PROOF ----------------

2 (wt=7) []                              (x + y)' != x'.                   % denial of Winker2
3 (wt=13) []                             ((x + y)' + (y + x')')' = y.      % Robbins

5 (wt=18) [para(3,3)]                    (x + (x + y' + (x + y)')')' = (x + y)'.
6 (wt=19) [para(3,3)]                    (x + (x + y + (x + y')')')' = (x + y')'.
24 (wt=21) [para(6,3)]                   ((x + y')' + (x + x + y + (x + y')')')' = x.
47 (wt=29) [para(24,3)]                  ((x + y)' + (y + (x + z')' + (x + x + z + (x + z')')')')' = y.
48 (wt=27) [para(24,3)]                  (x + (x + x + y + (x + y')' + (x + y')')')' = (x + y')'.
146 (wt=29) [para(48,3)]                 ((x + y')' + (x + x + x + y + (x + y')' + (x + y')')')' = x.
250 (wt=34) [para(47,3)]                 (x + (x + (x + y)' + (y + z')' + (y + y + z + (y + z')')')')' = (x + y)'.
996 (wt=42) [para(250,3)]                ((x + (y + z)')' + (x + z + (z + (y + z)' + (y + u')' + (y + y + u + (y + u')')')')')' = x.
16379 (wt=21) [para(5,996),demod([3])]   (x + (x + x + x + (x + x')')')' = (x + x')'.
16387 (wt=29) [para(16379,3)]            ((y + (x + x')')' + (y + x + (x + x + x + (x + x')')')')' = y.
16388 (wt=23) [para(16379,3)]            ((x + x')' + (x + x + x + x + (x + x')')')' = x.
16393 (wt=29) [para(16388,3)]            (x + (x + x + x + x + (x + x')' + (x + x')')')' = (x + x')'.
16426 (wt=37) [para(16393,3)]            ((y + (x + x')')' + (y + x + (x + x + x + x + (x + x')' + (x + x')')')')' = y.
17547 (wt=60) [para(146,16387)]          (x + (x + (x + x + x + (x + x')')' + (x + x + x + x + (x + x')' + (x + x')')')')' = (x + x + x + x + (x + x')' + (x + x')')'.
17666 (wt=33) [para(24,16426),demod([17547])]   (x + x + x + x + (x + x')' + (x + x')')' = (x + x + x + (x + x')')'.

The last step is an instance of Winker2.

------------ end of proof -------------

2006: Prover9 Proof with Two Unary Definitions

assign(max_weight,30).
set(restrict_denials).

list(weights).

  weight(g(_)) = 1.       % with variable argument
  weight(g(x)) = 1000.    % with any other argument

  weight(h(_)) = 1.
  weight(h(x)) = 1000.

end_of_list.

assign(eq_defs, fold).    % introduce defined operations

formulas(assumptions).

  x + y = y + x                # label(Commutativity).
  (x + y) + z = x + (y + z)    # label(Associativity).
  ((x + y)' + (x + y')')' = x  # label(Robbins).

  g(x) = (x + x')'             # label(definition_g).
  h(x) = x + (x + (x + g(x)))  # label(definition_h).

end_of_list.

formulas(goals).

  (x + y')' + (x' + y')' = y           # answer(Huntington).
  (exists a exists b (a + b = a))      # answer(Winker1a).
  (exists a exists b (a + b = b))      # answer(Winker1b).
  (exists a exists b ((a + b)' = a'))  # answer(Winker2a).
  (exists a exists b ((a + b)' = b'))  # answer(Winker2b).

end_of_list.

% Proof 1 at 27.39 (+ 0.11) seconds: Winker2b.
% Proof 2 at 28.11 (+ 0.11) seconds: Winker1b.
% Proof 3 at 43.29 (+ 0.15) seconds: Winker1a.
% Proof 4 at 43.29 (+ 0.15) seconds: Winker2a.
% Proof 5 at 47.38 (+ 0.16) seconds: Huntington.

Same formulas, but automatic (except for assign(eq_defs, fold))
Input File, Output File, XML-formatted proofs

% Proof 1 at 965.62 (+ 1.40) seconds: Winker2b.
% Proof 2 at 989.94 (+ 1.46) seconds: Winker1a.
% Proof 3 at 989.95 (+ 1.46) seconds: Winker1b.
% Proof 4 at 989.97 (+ 1.46) seconds: Winker2a.
% Proof 5 at 1025.36 (+ 1.48) seconds: Huntington.

Prover9 Proof with One Unary Definition

assign(sos_limit, 40000).
assign(max_weight, 35).
assign(max_vars, 3).

set(restrict_denials).
assign(eq_defs, fold).

assign(pick_given_ratio, 8).
assign(max_hours, 1).

list(weights).

    weight(h(_)) = 1.      % variable argument
    weight(h(x)) = 1000.   % else 1000 (nonvariable arg)

end_of_list.

formulas(assumptions).

  x + y = y + x                   # label(Commutativity).
  (x + y) + z = x + (y + z)       # label(Associativity).
  ((x + y)' + (x + y')')' = x     # label(Robbins).

  h(x) = x + (x + x')'            # label(definition_h).

end_of_list.


formulas(goals).

  (x + y')' + (x' + y')' = y             # answer(Huntington).
  (exists a exists b (a + b = a))        # answer(Winker1a).
  (exists a exists b (a + b = b))        # answer(Winker1b).
  (exists a exists b ((a + b)' = a'))    # answer(Winker2a).
  (exists a exists b ((a + b)' = b'))    # answer(Winker2b).

end_of_list.

% Proof 1 at 393.60 (+ 0.88) seconds: Winker2b.
% Proof 2 at 524.26 (+ 1.06) seconds: Winker1b.

Try Lots of Different Definitions

• enumerate terms
• canonicalize with associativity and commutativity
• up to a reasonable number (several thousand)

• one unary definition (874)
• one binary definition (909)
• two unary definitions, one depends on the other (726)

Looper

• Script to run a sequence of Prover9 (or Mace4) jobs.
• Takes a base file and a file of candidates (one per line).
• For each candidate, append it to the base file and run Prover9 (or Mace4).
• Don't keep all the outputs, but generate a summary.

Looper Results

• one unary definition (874): No Proofs
• one binary definition (909): No Proofs
• two unary definitions, one depends on the other (726): 15 proofs

Two Unary Definitions

The Winner

g(x) = (x + x')'.
h(x) = (x + (x + (x + g(x))))'.

% Proof 1 at 87.93 (+ 0.26) seconds: Winker2a.
% Proof 2 at 99.69 (+ 0.28) seconds: Winker1b.
% Proof 3 at 100.42 (+ 0.28) seconds: Winker1a.
% Proof 4 at 117.16 (+ 0.29) seconds: Winker2b.
% Proof 5 at 118.62 (+ 0.30) seconds: Huntington.

prover9 -f winner.in > winner.out

Sidebar: Folding with Standard Definitions

Folding with meet, join, complementation: proof in 16 seconds:

prover9 -f olsax-fold.in > olsax-fold.out

All in terms of the Sheffer stroke: no proof in 1 hour.

References

1. E. V. Huntington, ``New sets of independent postulates for the algebra of logic'', Trans. AMS 35, 274--304 (1933).
2. E. V. Huntington, ``Boolean algebra: A correction'', Trans. AMS 35, 557--558 (1933).
3. L. Henkin, J. D. Monk, and A. Tarski, Cylindric Algebras, Part I, North-Holland, 1971.
4. W. McCune, ``Solution of the Robbins problem'', J. Automated Reasoning, 19(3):263--276, 1997. Also see http://www.cs.unm.edu/~mccune/papers/robbins/.
5. W. McCune, Prover9, http://www.cs.unm.edu/~mccune/prover9/, 2005-2007.
6. S. Winker, ``Absorption and idempotency criteria for a problem in near-Boolean algebras'', J. Algebra 153(2), 414--423 (1992).