Abstraction, generalization, common results

[siddhartha-gadgil]

• This includes Abstraction, including consolidate enumerative/computational proofs and results of experiments #221 - using results from experiments.
• To rewrite one or more statements
  • identify complex terms that are parts of statements and proofs.
  • generate functions with types domains of these complex terms.
  • use the equations thus generated to backward propagate, ideally to generate the terms via functions.
• For multiple equations, look for common generation, using a concave function to favour terms involved in many results.

[siddhartha-gadgil]

• We can introduce one or more variables to generate functions.
• By tracing equations, we look for both ingredients and nearby stuff.
• Give these weights and generate equations.
• We look for equations giving the given terms, but actually can just dump all equations.
• We can use both depth bounds and tangential generation to search without blowup.

[siddhartha-gadgil]

• We can rewrite terms, both by generating functions with codomains and by simply making stuff into lambda.
• Finding common patterns involves generating many statements and/or proofs efficiently.