[Easycrypt-club] Hammers

Bas Spitters b.a.w.spitters at gmail.com
Wed Jan 24 15:33:56 CET 2018


There has been a lot of work on "hammers" for various systems.
E.g. HOL(y)hammer.
https://link.springer.com/content/pdf/10.1007/s11786-014-0182-0.pdf

They return the information they get from the SMT solver so that they
can be stored in the proof scripts. This saves a lot of recomputation
time.
Is this feasible for EC too?


More information about the Easycrypt-club mailing list