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