Email Gateway (Aug 19 2022 at 17:22): Email Gateway (Aug 19 2022 at 17:22):From: Bohua Zhan <bzhan@mit.edu>
Hi, everyone
Recently I have been working on writing a new theorem prover based on
Isabelle. This is the first time I think it is in good enough shape to
be made public. It is now available at
https://github.com/bzhan/auto2
An informal documentation (doc.pdf) is also available.
It is still more of a "proof-of-concept" than anything that can be
used in production. The focus has been on reproducing the proof of
selected theorems in HOL/Number_Theory/Primes.thy. A lot of work will
be needed to extend it to be able to prove a wide range of theorems.
I am posting it here to see if there are any suggestions, things that
are known that could help with this project, or (even better)
contributions. I can also answer questions about the program here. In
particular please point out anything that is confusing or need to be
elaborated on in the documentation.
Thanks,
Bohua
Email Gateway (Aug 19 2022 at 17:23):From: Makarius <makarius@sketis.net>
On Mon, 16 Mar 2015, Bohua Zhan wrote:
Recently I have been working on writing a new theorem prover based on
Isabelle.
I was first confused by this wording, but "auto2" seems to be a plain
proof tool inside Isabelle, i.e. just a normal application of the existing
framework.
I recommend to add a formal session ROOT to make clear what is the project
structure. See also "isabelle mkroot" in the "system" manual.
BTW, using some unspecified "development version of Isabelle" means this
is mainly a private experiment of yours. I you have good reasons for not
using the latest Isabelle release (Which ones?) the minimum is to say
which changeset id of the Isabelle repository is required. It is also
possible to make a formal Mercurial subrepository reference (in a
Mercurial repository, probably not a git one).
I am posting it here to see if there are any suggestions, things that
are known that could help with this project, or (even better)
contributions.
Just some notes from looking briefly:
Theory names are always capitalized in Isabelle.
The @{term_pat} antiqutation is a bit strange. If you really mean to
refer to schematic terms, you should say so via
Proof_Context.mode_schematic, and not Proof_Context.mode_pattern.
Makarius
Email Gateway (Aug 19 2022 at 17:23):From: Bohua Zhan <bzhan@mit.edu>
Hi, Makarius
Thanks. Updated with capitalization of theory names, and moved to
support Isabelle2014.
It seems when a schematic variable without specified type is read in
mode_schematic, the type is set to be a free variable rather than
schematic variable. I would actually prefer it to be schematic, since
there is potential for type matchings.
I will need more time to figure out mkroot. The general structure is:
Auto2 depends on Arith_Thms, Logic_Thms
Auto2_Test depends on Auto2 (unit testing)
Primes_Ex depends on Auto2.
Best,
Bohua
Email Gateway (Aug 22 2022 at 10:38):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Bohua,
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
Email Gateway (Aug 22 2022 at 10:46):From: Bohua Zhan <bzhan@mit.edu>
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
Email Gateway (Aug 22 2022 at 10:49):From: Bohua Zhan <bzhan@mit.edu>
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:
Please see README and the updated documentation for details. Again I
would welcome any comments and suggestions.
Best,
Bohua
Last updated: Apr 25 2024 at 12:23 UTC