Re: [isabelle] Work on a new theorem prover



Dear Bohua,

> On 01.07.2015, at 18:37, Bohua Zhan <bzhan at mit.edu> wrote:
> 
> Hi, everyone
> 
> I have uploaded the second version of auto2 at
> https://github.com/bzhan/auto2
> 
> It now supports Isabelle2015. The biggest internal addition is proof
> scripts, which allows the user to specify intermediate steps of a
> proof, similar to (but currently independent from) Isar. There is also
> much better support for induction.
> 
> There are now more examples from different areas:
> - Number theory: infinitude of primes and unique factorization theorem.
> - Lists, trees, and red-black trees.
> - Hoare logic.
> 
> Please see README and the updated documentation for details. Again I
> would welcome any comments and suggestions.

This looks interesting. What I would be curious to see is how âauto2â performs with respect to other Isabelle automation (âautoâ, âblastâ, etc., and âsledgehammerâ). The paper âSledgehammer: Judgement Dayâ by BÃhme and Nipkow applied Sledgehammer to 1240 goals from Isabelle theories, using a tool called Mirabelle, included with Isabelle. It would be fairly straightforward to extend Mirabelle with âauto2â and perform some comparisons. Please let me know if this interests you and I can help you get started with Mirabelle.

Cheers,

Jasmin





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