Re: [isabelle] Work on a new theorem prover



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
>




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