[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Strong Mizar wish: linking to consider (fwd)
On Sun, Mar 24, 2002 at 12:47:10PM +0100, Andrzej Trybulec wrote:
>
>
> Freek Wiedijk wrote:
>
> > For instance it might be nice to know what the thesis is,
> > when a skeleton step doesn't fit it (actually, because of
> > definitions, there probably is a whole list of "expanding"
> > theses.) I often get confused about what the thesis is,
> > especially when definitions are involved. Just knowing that
> > I got it wrong is less nice than knowing what it should be.
> >
> > And if a system prints the thesis in such an error message,
> > it would be nice to be able to "copy" the assumption from the
> > thesis to put it in an "assume". Something like that.
>
> I see, a good example. I guess the same goes for Correctness Conditions
> and Properties (in the second case I have often trouble, what should be
> proved).
On a much smaller scale, in Mizar-MSE, I have had at some point a
printout of the current thesis in case when the proof skeleton was
erroneous. It was not much of a help as the thesis was reconstructed
from the internal representation carrying only the semantic
resemblance to the source thesis and there were many source theses
that resulted in the same internal representation. As Mizar-MSE was
used for introductory teaching, this feature turned out to be more
trouble for the students than help.
As far Correctness conditions and Properties go I have a question:
where is a description of what they should be? Needles to say I never
remember what they should be and have to look up examples in MML. On
the same note, when one references definitional theorem sometimes one
heads for a surprise as such a theorem is not what one naively
expects. Again, I do not know where it is documented (besides
Grzegorz's MML Query services but then again there are in an internal
format).
--
Piotr Rudnicki CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr