[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] [piotr@sedalia.cs.ualberta.ca: A request from W W Armstrong]
Hi:
I sent this message on Saturday but it bounced back.
----- Forwarded message from Piotr Rudnicki <piotr@sedalia.cs.ualberta.ca> -----
Date: Sun, 25 Aug 2002 09:23:49 -0600
From: Piotr Rudnicki <piotr@sedalia.cs.ualberta.ca>
To: mizar-forum@mizar.uwb.edu.pl
Cc: arms@dendronic.com
Subject: A request from W W Armstrong
User-Agent: Mutt/1.2.5.1i
Hi:
Bill Armstrong, Y. Nakamura and I are finishing formalization of the
celebrated 1974 Bill's paper on the functional dependencies in
relational data bases. Bill joined the effort quite late but is very
helpful in improving the final editing. He took seriously my claim
that Mizar texts are readable with routine effort and studies on his
own the parts of the paper done before he joined. He wanted me to
pass the following comment. When trying to understand the following
completely on his own
definition
let X be set;
cluster (B1) (B2) Subset-Family of X;
end;
he got stuck and was totally confused. The attributes and the type are
earlier defined in the paper. The source of his confusion was the word
"definition" because what on Earth is being defined here. Bill says that
if instead of "definition" there was some other keyword, his confusion would
probably be not as frustrating.
And also, Bill wishes that Mizar has numerous synonyms for the keyword
"theorem" because as of now, facts that differ by orders of magnitude
in importance and difficulty are announce as "theorem" which makes him laugh
at times.
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr
----- End forwarded message -----
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr