Re: Studying Mizar

Dear Boris,

Have you tried browsing the HTML-linked articles?
(http://mizar.uwb.edu.pl/version/current/html/)

This linked version would help you to quickly find the exact meaning of 
every notion. E.g. starting from the definition of <i> in XCMPLX_0 you can 
go directly to the definition of -->, and so on.

Best,

Adam

On Thu, 15 Jul 2010, Boris Schminke wrote:

> Dear All,
> I'm writing to ask for advise in studying Mizar.
> I think that Mizar is great and I have been trying to study it for
> some time and now I understand syntax or at least proof's structures
> better than I used to do several months ago. The problem is that I
> still do not understand the whole logic of MML. For example, when I
> tried to prove some theorems from XBOOLE_1 article I faced no
> difficulty, but in great contrast to it, I do not understand a word
> from INTEGR1C and even XCMLPX_0 appears to be not very obvious for me.
> For instance, why imaginary unit <i> is the same as (0,1) --> (0,1) or
> even worse what does --> mean, since (0,1) somehow resembles the
> definition of imaginary unit I am used to.
> What should I do? Maybe it would be better to read or even write
> proofs for some amount of 'core' articles of MML? If so, then couldn't
> anybody said me, what exactly? Or maybe it's better to try to
> understand at last the INTEGR1C lurking the MML far and wide? I've
> tried to use MML Query but still the notions and names used in MML are
> not always the same with ones in my head. In MML there are 'bags',
> 'Go-boards' and other unusual objects. I will be very glad if somebody
> tells me how I can my best to comprehend the logic of MML.
> I'm looking forward to hearing from you.
> Yours,
> Schminke Boris.
>


Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================