[isabelle] Call for benchmarks



Hi everyone,

  I've worked on integrating the harvey theorem prover within Isabelle. The 
goal is to offer better automation for formulas falling in the domain of 
harvey (first-order formulas possibly containing set symbols), especially 
huge ones.
  If you have formulas of that kind, I will be pleased if you can send it to 
me, so that I can test my implementation against it. Attached is an example 
of what kind of lemmas it can handle. Don't hesitate to send much bigger 
problems.

Thanks,
Clément Hurlin

Attachment: problemExamples.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.