Abduction: Abduction Prover against MiniF2F

[yutakang]

• Domain-specific optimisations?
  • Avoid template-based conjecturing when no user-defined types appear in the proof goal.
  • More tactics for math problems.
  • math_olympic mode or IMO mode
  • How to handle large terms?
  • Local assumptions and fixed variables?