[Hol-info] New article type PROOF PEARLS in Journal of Automated Reasoning (fwd)

[Josef Urban]

---------- Forwarded message ----------
Date: Thu, 17 Jul 2008 18:26:00 +0200
From: Tobias Nipkow <nipkow@...>
To: hol-info@...
Subject: [Hol-info] New article type PROOF PEARLS in Journal of Automated
     Reasoning

Journal of Automated Reasoning is very happy to announce the new article
type of

  *Proof Pearls*.

The goal of *Proof Pearls* is to disseminate insights gleaned from the
growing body of machine-checked formalizations and proofs, obtained
using both interactive and automated methods. Application areas include
the full range from pure mathematics and logic to software and hardware
verification. Proof pearls should be short communications that focus on
a few central ideas rather than extended research reports. Contributions
may include:

o a short, elegant proof of a self-standing result

o a novel way of defining a fundamental concept

o a notable approach to proving a key lemma in a larger development

o a snippet of verified code, carefully engineered to balance efficiency
with ease of verification

o a clever or impressive application of automated tools in a particular
domain

*Proof Pearls* adapt Jon Bentley's notion of a "programming pearl" to
the verification paradigm. Proof pearls should thus encapsulate
fundamental insights that are adaptable and reusable, while being
elegant and satisfying in their own right. Typical examples could be a
verification of Huffman's algorithm, a perspicuous proof of the
fundamental theorem of algebra, or a novel axiomatization of a
particular algebraic system that was discovered using automated methods.

Submissions will undergo the usual refereeing process, and will be
evaluated according to expository and theoretical merit. Systems and
formalizations should be made available online.

We look forward to your submissions
Tobias Nipkow
Editor-in-Chief
JAR

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
hol-info@...
https://lists.sourceforge.net/lists/listinfo/hol-info

[Josef Urban]

Hi,

at http://octopi.mizar.org/~urban/dupl.html is a list of more than 1000
MML duplications.

Josef

[Jesse Alama]

Josef Urban <urban@...> writes:

> at http://octopi.mizar.org/~urban/dupl.html is a list of more than
> 1000 MML duplications.

How many of these are caused by the fact that, in some articles, some
authors prove results without "exporting" them using the theorem
keyword?  It is frustrating to find out, after looking for a theorem in
the MML, that it is off-limits to you because the author thought that a
result should be just a lemma rather than a theorem.  (Down with lemmas,
I say!  Make every proved result available to everyone, not just
yourself.)

Lemmas can even lead to odd situations such as Lm1 in ZFMISC_1 and
ZFMISC_1:37.

Jesse

--
Jesse Alama (alama@...)

[Josef Urban]

On Mon, 28 Jul 2008, Jesse Alama wrote:

> Josef Urban <urban@...> writes:
>
>> at http://octopi.mizar.org/~urban/dupl.html is a list of more than
>> 1000 MML duplications.
>
> How many of these are caused by the fact that, in some articles, some
> authors prove results without "exporting" them using the theorem
> keyword?

I guess more than half. There are funny situation when the lemma is proved
more than once (even in one file :-), and when it is equivalent to more
than one theorem :-). A more "legal" source of duplications is when a
cluster is justified by a lemma or a theorem.

> It is frustrating to find out, after looking for a theorem in
> the MML, that it is off-limits to you because the author thought that a
> result should be just a lemma rather than a theorem.  (Down with lemmas,
> I say!  Make every proved result available to everyone, not just
> yourself.)

I agree, "Mizar theorems" are no match for what mathematicians grade as
"theorems" anyway. Unless a lemma is only needed to prove a clearly (from
a Mizar point of view) stronger result, it should be exported as a "Mizar
theorem".

> Lemmas can even lead to odd situations such as Lm1 in ZFMISC_1 and
> ZFMISC_1:37.

There are quite a few situations like that, my conjecture is that this is
done to keep the theorem numeration stable.

Josef

[Piotr Rudnicki]

On Tue, Jul 29, 2008 at 02:52:30AM +0200, Josef Urban wrote:
>
> On Mon, 28 Jul 2008, Jesse Alama wrote:

> >Lemmas can even lead to odd situations such as Lm1 in ZFMISC_1 and
> >ZFMISC_1:37.

> There are quite a few situations like that, my conjecture is that this is
> done to keep the theorem numeration stable.

Maintaining the numbering of theorems stable (if this is the case)
leeds to fossilization of MML.  What is the problem in renumbering theorems
after moving them around?  Renumbering all theorems and references in MML
after a revision seems like a mundane editorial job.

One argument that I see in support for avoiding renumbering theorems is that
authors get used to numbers of frequently referenced theorems.  This does not
apply to me; I have to look at the referenced theorems all the time ;-)

Cheers,

--
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr

[Freek Wiedijk]

Dear Piotr,

>Maintaining the numbering of theorems stable (if this
>is the case) leeds to fossilization of MML.  What is the
>problem in renumbering theorems after moving them around?

I would have to edit
<http://www.cs.ru.nl/~freek/100/mizar.html> all the time?

Seriously, I think it would be nice to have _some_ stable
way of referencing theorems in the MML.  That you can write
(in a paper, for instance) "this has been formalized as
lemma so-and-so in MML", instead of just being able to
give the statement and then say "well, try to find it,
I'm sure it's there _somewhere!"_

Of course, if you think the results in MML are not
interesting enough for referencing, then this objection
doesn't apply :-)

>Renumbering all theorems and references in MML after a
>revision seems like a mundane editorial job.

_If_ you start to change the numbers on a bigger scale,
then _please_ also move the theorems between articles on
a much bigger scale, so articles will no longer contain
theorems that really should have been somewhere else.

>One argument that I see in support for avoiding renumbering
>theorems is that authors get used to numbers of frequently
>referenced theorems.  This does not apply to me;

Not to me either.  The only one I that I used to know was
AXIOMS:22 (however I don't remember anymore what that was),
and I don't think _that_ one exists anymore.

On the other hand, I _still_ use the old webpage version
of the JFM (now long obsolete) to look up stuff sometimes.
If you start changing numbers, that would not be useful
anymore.

And if one had been working on an article, got distracted,
but then tried to pick it up half a year or so later,
one would have a bit of a problem, wouldn't you?  To get
it working again would take much more work then it takes now.

So I don't know.

Freek

[Josef Urban]

Hi Freek,

>> Maintaining the numbering of theorems stable (if this
>> is the case) leeds to fossilization of MML.  What is the
>> problem in renumbering theorems after moving them around?
>
> I would have to edit
> <http://www.cs.ru.nl/~freek/100/mizar.html> all the time?

You should mention the MML version number anyway. This is very standard,
e.g. references to Wikipedia articles should also refer to a particular
version, not to "current", as it can change arbitrarily. As for html, at
http://mmlquery.mizar.org/mml/ the versions are kept and can be referenced
absolutely.

It is a bit of shame that unpacked "raw text" articles are only available
for the last version at ftp://mizar.uwb.edu.pl/pub/version. We should keep
at least the aricles and abstracts from all versions also available for
absolute referencing.

>> Renumbering all theorems and references in MML after a
>> revision seems like a mundane editorial job.
>
> _If_ you start to change the numbers on a bigger scale,
> then _please_ also move the theorems between articles on
> a much bigger scale, so articles will no longer contain
> theorems that really should have been somewhere else.

That is one of the ideas behind a wiki for Mizar. I hope it will happen,
and not just in the very distant perfect future :-).

>> One argument that I see in support for avoiding renumbering
>> theorems is that authors get used to numbers of frequently
>> referenced theorems.  This does not apply to me;
>
> And if one had been working on an article, got distracted,
> but then tried to pick it up half a year or so later,
> one would have a bit of a problem, wouldn't you?  To get
> it working again would take much more work then it takes now.

It would work with the old system, and if the article is worth anything,
you might get help from Adam & Co. to port it to new version of the
system. Surely, if renaming is done on a larger scale, appropriate tools
will be more useful/needed than now. Such tools will obviosly be needed
also for wiki functionality.

Josef

[Freek Wiedijk]

Hi Josef,

>>And if one had been working on an article, got distracted,
>>but then tried to pick it up half a year or so later,
>>one would have a bit of a problem, wouldn't you?  To get
>>it working again would take much more work then it takes now.
>
>It would work with the old system, and if the article is worth anything,
>you might get help from Adam & Co. to port it to new version of the
>system.

I wouldn't want to work like that.  It feels wrong not to
use the latest MML.  Also I think the library committee
only wants to see articles that work with the latest MML.

Freek

[trybulec]

Very interesting and rich material. We should use it to revise MML, of
course. However the value of information  varies.
The most important are true repetition, i.e. the same kind of the item.

So we have three duplications of definitions (actually one in POLYEQ_3,
two remaining are redefinitions that do not changed the meaning). 24
functor registrations.

I work on a revision so I have removed repeated definitions, and 20
functor registrations. It caused some changed
in the Environment Declaration of depeding articles, nothimg serious.
At least one functor registration had been already removed (I mean the
duplication of it).

Josef,
it is very useful and very important utility. How to use it:

1. I would like it to be called after every revision (good chances that
new repetitions happen).

2. It would be useful tool for reviewers, or for the Athors if they
would rather avoid problems with reviews.

Could be it distributed with Mizar? How long it runs?

Regards,
Andrzej


Josef Urban wrote:

>
> Hi,
>
> at http://octopi.mizar.org/~urban/dupl.html is a list of more than
> 1000 MML duplications.
>
> Josef
>

[Josef Urban]

Andrzej,

> At least one functor registration had been already removed (I mean the
> duplication of it).

Yes, the data were taken from MML 1011 (that one at
http://octopi.mizar.org/~mptp/mml/html/), some things maybe outdated.

> it is very useful and very important utility.

this one is actually very simple, nothing remotely advanced like the
(type)generalization in MoMM; just string equality after normalization of
the formula

> 1. I would like it to be called after every revision (good chances that new
> repetitions happen).
>
> 2. It would be useful tool for reviewers, or for the Athors if they would
> rather avoid problems with reviews.
>
> Could be it distributed with Mizar? How long it runs?

the posted data are a byproduct of a MaLARea uniquifier
(http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/MPTP2/MaLARea/script/uniquify.pl?view=markup)
run on all the MPTP top-level items, piped to a htmlizer
(http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/MPTP2/MaLARea/script/htmlize.pl?view=markup)

assuming that the formulas are normalized (like in MPTP) into a file of
lines like:

fof(name,formula).

the Perl code could be just:

perl -e '%h=(); while(<>) { m/^fof.([^,]*),(.*)/; if(exists $h{$2}) {print "$1,$h{$2}\n"} else { $h{$2}=$1}}'

This will take very short time on 100000 entries (about the number of
MML top-level items) - less than one second on my computer.

So the only task is the normalization, i.e. exporting formulas in absolute
notation. I do it for various reasons using XSLT, which is slow in
comparison with Pascal. For all the MML top-level items it would take
probably (tenths of) minutes (I do it for all of MML, not just top-level
items). But if you want it fast, simple, and not dependent on a XSLT
processor, have a Pascal program that prints instead of symbols like "K10"
their absolute name like k3_abcmiz_0 or ABCMIZ_0:func 3 (whatever). Just a
different printing function in "exporter" (if only top-level items are
needed). That should also take only seconds for all of MML.

Regards,
Josef

> Josef Urban wrote:
>
>>
>> Hi,
>>
>> at http://octopi.mizar.org/~urban/dupl.html is a list of more than 1000 MML
>> duplications.
>>
>> Josef
>>
>
>

[Piotr Rudnicki]

On Thu, Jul 31, 2008 at 06:53:15PM +0200, trybulec wrote:

  ...
>
> 2. It would be useful tool for reviewers, or for the Athors if they
> would rather avoid problems with reviews.
>
> Could be it distributed with Mizar? How long it runs?

The utility for cleaning the environment is useful for authors.  
Could it be distributed with Mizar.

Cheers,

--
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr