*To*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Subject*: Re: [isabelle] Work on a new theorem prover*From*: Bohua Zhan <bzhan at mit.edu>*Date*: Thu, 2 Jul 2015 16:17:47 -0400*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51974AE9-1287-4B89-BA65-2F3DE6478A6A@inria.fr>*References*: <CAEMBaCBC6Q1_WJYQjQ9r55zX7Ae8+M+6-9PUCF+-9v7+o6wPpg@mail.gmail.com> <alpine.LNX.2.00.1503171146590.14159@lxbroy10.informatik.tu-muenchen.de> <CAEMBaCDbaHAjCF4sJ_Xw6-Uo+Pvcg6Dx95GeyzvxBAR2NNgBxQ@mail.gmail.com> <CAEMBaCCLCNM6XafsgUXm05pt8dP=O3e2DNH=JXxGuesLw__dPQ@mail.gmail.com> <51974AE9-1287-4B89-BA65-2F3DE6478A6A@inria.fr>

Hi, Jasmin The intention (not to say it is realized) is that auto2 should be stronger than auto and blast, perhaps comparable to an SMT solver. The way auto2 matches terms with patterns (up to rewriting the term using known equalities) is similar to what is done in SMT, although I would think the overall idea is different. One difficulty with directly comparing auto2 and sledgehammer tools is that auto2 needs each theorem it uses to be registered by hand, specifying which direction it is to be used and under what conditions (this is done for some theorems in logic, arithmetic, and sets in theories Logic_Thms, Arith_Thms, and Set_Thms). Naively adding all theorems in all directions will make auto2 very inefficient. Also, auto2 works directly with statements in HOL rather than in first-order logic (the point is to work as closely as possible to what a human sees). On the other hand, I think it would be very interesting to try to use auto2 to formalize different theories, such as the 7 examples in the reference you gave. The goal is to use auto2 to prove all major theorems, with hints provided in the form of intermediate steps of the proof. The hints should be no more detailed than what would appear in an informal proof in a textbook. If this cannot be done, it may point toward some improvements in auto2 that can be made. Best, Bohua On Thu, Jul 2, 2015 at 7:34 AM, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote: > 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 >

**References**:**Re: [isabelle] Work on a new theorem prover***From:*Bohua Zhan

**Re: [isabelle] Work on a new theorem prover***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Date: Re: [isabelle] using makeindex in document preparation
- Previous by Thread: Re: [isabelle] Work on a new theorem prover
- Next by Thread: [isabelle] Quickcheck counter example of "3 < 4"?
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list