Email Gateway (Aug 23 2022 at 08:16): Email Gateway (Aug 23 2022 at 08:16):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Dear Isabelle/HOL community,
In the same way that there are journals for long papers and journals for brief notes, I am interested to know how short submissions to Archive of Formal Proofs could be? For example, does the submission of only one non-trivial theorem is fine? By nontrivial theorem, I meant a result for which an elegant proof is at least 5000 lines in Isabelle/HOL. I think that short submissions may be useful for beginners and for people for which formalizations in Isabelle/HOL is not their main activity, but still an important part of their research.
Sincerely yours,
José M.
Email Gateway (Aug 23 2022 at 08:16):From: Manuel Eberl <eberlm@in.tum.de>
Anything that takes 5000 lines is almost certainly enough content to
justify an AFP entry. We have many quite a few that are below 1000
lines, and that's okay. We decide this on a case-by-case basis, but I
would say that the material should be interesting and it should be
non-trivial. So anything below, say, 200 lines is probably not enough.
Anything about 1000 lines is probably fine (in terms of size), unless,
the content is heavily inflated or extremely technical but uninteresting.
I, for example, have quite a few ‘single-theorem entries’, e.g. the
transcendence of e, the transcendence of pi, the irrationality of
zeta(3). The first one of these only has about 600 lines, but it is an
interesting result and it is non-trivial, so I doubt anyone would see an
issue with its size.
I'm sure my fellow AFP editors will chime in if they disagree with
anything I've said.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:25):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Manuel is right, completely agree with this.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:26):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I have developed a proof method for solving equality statements, whose
implementation (in Eisbach) is only about 60 lines long (including
comments but without documentation, which I still have to write). I
thought about submitting this proof method to the AFP, but now I’m
concerned that it would be rejected right away.
Note that I would consider this development much more complex than a
proof of the same size. Actually it caused me a lot of headache to
arrive at this result, and I was about to give up during development.
What I want to say is that I guess this proof method could be of value
to other people out there, as people without experience in low-level
Isabelle proof methods and Isabelle/ML would probably find it hard to
come up with something like this themselves.
I have also other, more common, developments to submit at some point.
However, I wouldn’t like to submit my proof method as part of one of
those other developments, as it is really a general tool, usable in a
variety of contexts.
How is such a situation handled?
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:26):From: Tobias Nipkow <nipkow@in.tum.de>
Please describe in a bit more detail what that proof method does so we can
assess its generality.
Thanks
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:26):From: Konrad Slind <konrad.slind@gmail.com>
I recall reading somewhere that Presburger's thesis was 9 pages.
Konrad.
Email Gateway (Aug 23 2022 at 08:26):From: Konrad Slind <konrad.slind@gmail.com>
Ah yes, here it is:
Email Gateway (Aug 23 2022 at 08:26):From: Manuel Eberl <eberlm@in.tum.de>
There are not many tool entries in the AFP yet. Of the ones that there
are, there are a few with only about 200 lines of ML code (and some thy
wrapper around it, maybe with a few examples).
I suppose we will have to decide what to do about tool submissions on a
case-by-case basis. 60 lines indeed doesn't sound like much, but if it
is a substantial and useful contribution, it might well still be
accepted as an AFP entry. If it's of enough general use, one could even
think about putting it somewhere in the distribution instead.
I do agree that you should not simply submit it as a part of a proof
development.
Manuel
Last updated: Apr 26 2024 at 04:17 UTC