Studying Mizar
Boris Schminke <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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.