[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Hindrances
Hi:
Does anyone have a better idea how to name issue that Andrzej describes below
and similar to what Adam Naumowicz described as a puzzle a few e-mails ago?
Some time ago, Andrzej suggested "hindrances" with understanding
"hindrances to MML maintenance". We finally used "integrity" in a
paper for MKM. Frankly, I do not like either of these names.
"Smoothing rough edges" describes what is the essence of the issue but
is still no good as a name for the problem.
Best,
PR
On Thu, Nov 07, 2002 at 05:08:05PM +0100, Andrzej Trybulec wrote:
> What really hinders the work with MML, it is using different
> formulations of the same fact in different theorems. The typical
> example:
> sometimes it is 'i < j' sometimes 'i+1 <= j'
> and one has to use NAT_1:38 to move from one to the other.
> The same goes for 'A meets B' and " A /\ B <> {}'. This had been revised
> when we were working on XBOOLE_1.
>
> Recently I looked to 'A in bool X', i.e. 'A c= X'. I have found 20
> occurrences of it in MML. Mostly ZFMISC_1. An attempt to revise 'in
> bool' was quite successful. With the exception of SUBSET_1 (that cannot
> use the requirements SUBSET), the proofs became shorter, the authors
> actually needed the 'c=' version of the theorem, not 'in bool'.
> The resulting theorems (in ZFMISC_1) either are already in XBOOLE_1 or
> should be moved to it.
>
> The same was done in MBOOLEAN (following ZFMISC_1; for many sorted
> sets).
>
> Adam Grabowski promised to revise it soon.
>
> Andrzej Trybulec
>
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr