Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Call for benchmarks

Email Gateway (Aug 17 2022 at 14:49):

From: Clément Hurlin <clement.hurlin@esial.uhp-nancy.fr>
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
problemExamples.png

Last updated: Nov 21 2024 at 12:39 UTC