Re: [mizar] Re: Mizar Parser

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

Freek Wiedijk wrote:

> This seems close to what's on Grzegorz's webpages (although
> somehow I've never managed to see this: when I look for them
> the server never seems to work; so where are they at the
> moment?)

Megrez services are back in reality.
   http://megrez.mizar.org/mmlquery/
Sorry for delay.  Unfortunately, there is no yet any help
required for correct use.


> Also: I would like to have it offline, as I use Mizar most
> often on the train.  So would I need to install web server
> and a database and a lot of overhead like that for it to be
> usable in that environment?


MML Query can be downloaded. It is a bunch of perl scripts
plus 1Gb of data.  No other stuff is required. It works
in command mode.
For MML Query Browser you will need web server. But this
is not yet downloadable.  But elements of browser will be
systematically moved to command mode.

>  Because then I probably wouldn't
> use it.  I don't want so much stuff running on my system just
> to be able to search the MML.  I really would prefer it to be
> a simple standalone program.

Try mmlquery.

> BTW: I never used Grzeorz and Josephs systems.  I use grep.
> But it would be wonderful to be able to say "give me all the
> theorems of which the statement has these-and-these
> constructors".

OK. In search window in

   http://megrez.mizar.org/mmlquery/three.html

write

  at least * (ref IRRAT_1:th 10)

to find all library items which refer to all constructors from
IRRAT_1:10. "ref" gives list of constructors to which argument refers.
Use "exactly" or "at most" instead of "at least" if necessary.
If you write
  at least * fam (ref IRRAT_1:th 10)
you will get better result because search will concern all
constructors from IRRAT_1:th 10 and their redefinitions.

You can also search
  at least(ARYTM:attr 1, ARYTM:func 1, ARYTM:func 2, FUNCT_1:attr 1,
     FUNCT_2:attr 1,HIDDEN:mode 1, HIDDEN:pred 1, RELSET_1:mode 2,
     SEQ_1:func 1, SEQ_2:attr 4, SEQ_2:func 2, SUBSET_1:mode 2)

which is equivalent to the first query. (list inside is the result
of "ref IRRAT_1:th 10" query).

The names of items can be found in  Mizar eXtended Abstracts
  http://megrez.mizar.org/pub/mxa/
You may use also "Constructor explanation" in mizarmode for emacs
(mizar.el in Mizar distribution) or ask the query

   constructor(symbol aseq notation)

which result in the (mml query) names of constructors with notation
using symbol "aseq".

Now, there is no usable description of MML Query system.
But it is now under development (with Piotr Rudnicki)
and I hope it will be ready for MKM.

>  Although to be really useful you'd need to be
> able to phrase those constructors in Mizar input form (using
> the environment and context of a certain position in an
> article, I guess.)

See mizarmode for emacs. You can get there full info of a statement
in any place of mizar article. This info is ready for MML Query
or just for grep browsing the MML.  Josef can explain it better.

Best regards,
Grzegorz