A few improvements have been made over the versions that discovered modus ponens and $e_l = e_r$
Lambda-closures
If variables are specified, when an interesting lemma is discovered that depends on these, in addition to taking the tangent with respect to these, all partial lambda-closures are considered.
Scaling down cut-offs, relative scaling
- Previously, cutoffs were decided independently, which increased the chance of blowing up as a large number of processes with low cutoffs could be spawned.
- Now it is ensured that the total of the reciprocal of the cutoffs is at most the reciprocal of the original cutoff.
- Further, a scale factor decides the relative weights (hence cutoffs) - we make this high to increase sensitivity to the importance of lemmas.
Tracing, avoiding duplication of tangents
- A method was added to explore with traces.
- While seeking and exploring with traces, using the same term for a tangent twice is avoided.
Results
- Both $e_l = e_r$ and modus ponens are still discovered, and in both seek and explore.
- However, $e_l = e_r$ is discovered using two lemmas.
- Addendum: when exploring with traces, the dependence between the pi-closures of $A \to A$ and $(A \to B) \to (A \to B)$ was seen.