********** 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 ...