**********
Background
**********

Collaboration with mathematicians (open questions).

Developing methods for systematically working towards solutions.

Use proofs with extra assumptions to help guide a search for a proof without
extra assumptions.

The later searches are biased to prefer proof steps (hints) from the earlier
searches.

Where do the extra assumptions come from?

   - theory hierarchies (e.g., Boolean Algebra -> Lattice Theory)

   - basic properties (e.g., commutativity, associativity, ...) 

   - conjectured properties specific to the target theory

Operationally, the challenges are

   - find good extra assumptions

   - eliminate extra assumptions from a proof to find a more general
     result (pushing a result up the hierarchy)


*******************************************
Using the Goal to Suggest Extra Assumptions
*******************************************

Question:  When attempting to prove A => g, can we make use of information
gained by temporarily assuming g?

If g is provable, then consequences of g are provable.

Idea:  Some of these consequences might be good extra assumptions in the
search for a proof of A => g.

How can we identify a good set?

----------------------------------------------

Say we have several proofs of g with different extra assumptions.

   PF1: A + EA1 => g
   PF2: A + EA2 => g
        :
   PFn: A + EAn => g

----------------------------------------------

Step 1

For each proof, use derivation information to identify those steps that
depend (in the proof) on the extra assumption and those that do not.

   D = union over i {c in PFi | c is dependent on EAi (in this proof)} 
   L = union over i {c in PFi | c is not dependent on EAi (in this proof)} 

The L clauses are lemmas of A.

Several of the d in D might be provable in A.

----------------------------------------------

Step 2

Identify as many d in D as possible: 

   Set X:  A => d  (not dependent on the relevant extra assumptions)

   Set Y:  A + g => d

----------------------------------------------

EA = Y - X are candidate extra assumptions.

   Several may be too strong to be helpful (e.g., g itself).

   Want to eliminate these first.

   Order the EA by "closeness" to g in the relevant PFi.

While EA is not empty,

   prove A + EA => g

   remove the first ea in EA that participates in the proof

That's the idea ... Let's see what happens!


*********************************
Application to the AIM Conjecture
*********************************

Weak AIM conjecture (32 goals):

    8 proved lemmas.
   15 nil3 1K goals.
    9 nil3 0K goals.

   Now known but still seek a first-order proof.

Strong aim conjecture (7 goals):

   4 single a goals (aK)
   3 double a goals (aa)

---------------------------------

First observations

   Hundreds of proposed extra assumptions.

   Finding/eliminating is a *long* process (several hours per step, long
   proofs).

   When elimination stalls, can still make use of accumulated proofs.

   Status:  A few new generalizations of previous results.

Example

   Target:  any one of the 15 nil3 1K goals (suffices for all 15) 

   Starting with several proofs of special cases,

      604 proposed new extra assumptions

      After 550/604 eliminated, weakened target theorem

         K(x,y) = K(y,x) => nil3 1K

         A few other (even less significant) generalizations.

Example

   Target:  {middle Bol, KK} => any aa goal (suffices for all 7 goals)

      x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
      K(K(x,y),z) = 1 # label("KK").

   Current status (weakened target theorem):

      {middle Bol, KK, imord2 R} => aa2

         R(R(x,y,z),y,z) = x # label("imord2 R").

      % Length of proof: 7481 (2575 new hints)
      % Level of proof: 135
      % Maximum clause weight: 41.000
      % Given clauses in run: 2449
      % Given clauses in proof: 1646 (0 new hints)

Example

   Target:  {imord2, aK} => any aa goal (strategic value)

      T(T(x,y),y) = x       # label("imord2 T").
      L(L(x,y,z),y,z) = x   # label("imord2 L").
      R(R(x,y,z),y,z) = x   # label("imord2 R").

   Current status (elimination loop):

      Down to 1 extra assumption.

      % Length of proof: 63347 (41181 new hints)
      % Level of proof: 268
      % Maximum clause weight: 53.000
      % Given clauses in run: 9365
      % Given clauses in proof: 6753 (0 new hints)

Example

   Target goal:  imord2 => any aK goal

   In progress ...