Re: [mizar] Lexical resources

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

By the way,

Lexical resources (and not only) can be reported by MML Query:

   list of symbol    - all symbols
   list of symbol | vocabulary  - all vocabularies
   list of symbol | vocR  - all predicate symbols
ect.

I added operations "vocabulary", "vocR", etc. after reading
Andrzej's mail.

Other resources see
  http://megrez.mizar.org/mmlquery/description.html

Grzegorz

Andrzej Trybulec wrote:
> 
> I asked Adam Naumowicz if we have a utility that reports the size of
> lexical resources of MML. The answer, it is easy
> to grep them. All vocabularies are kept now one file :  MML.VCT
> 
> The results:
> 
>                                           Qualifier
> Number
> 
> Predicate symbols                  R                          586
> Functor symbols                     O                        2273
> Left Functor Brackets            K                            25
> Right Functor Brackets           L                            25
> Mode symbols                       M                          531
> Attribute symbols                   V                          913
> Selector symbols                    U                          103
> Structure symbols                   G                            82
> 
> To grep e.g. the number of mode symbols write
> 
>       grep -c ^M c:\mizamml.vct
> for other symbols one has change M to the proper qualifier.
> 
> A trap:
> 
>     every vocabulary starts with a line that begins with 'G' so after
> 
>      grep -c  ^G  c:\mizar\mml.vct
> 
> one gets the number of structure symbols + the number of vocabularies.
> 
> The number of vocabularies one gets after
> 
>     grep -c  ^#   c:\mizar\mml.vct
> 
> Remarks:
> 
> The number of left functor brackets is the same as the number of right
> functor brackets. It is not accidental, in older Mizar if one started
> i-th left functor bracket, it must be closed with i-th right functor
> bracket. One may mix now functor brackets, the only example that I know:
> the article MEASURE5: def 2, def 3, def 4, def 5
> 
>    Formats
>        [.a,b.]    ].a,b.]   [.a,b.[   ].a,b.[
> for respectively closed, open-closed, closed-open, open intervals of
> real numbers. It a result of a revision, of course.
> 
> The homonymic tokens:
>      Functor brackets     [ ]  and { }
>      Predicate symbol   =
> are not counted by grep.
> 
> Greetings,
> Andrzej Trybulec