[mizar] Re: calculating the transitive closure of required mizar items for a theorem

[Jesse Alama <alama@stanford.edu>]

Hi Josef,

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> On Wed, 7 Nov 2007, Jesse Alama wrote:
>
>> Thanks for helping out with this.  It looks like the task of computing a
>> "custom MML" is going to require about as much effort as writing an
>> article. :->
>
> I think that this may be quite practically important: If MML ever
> becomes collaboratively editable on the web (some formal wiki), then
> fast computing of articles potentially influenced by some editing will
> be needed. The smaller the depending set of articles, the faster its
> real-time re-verification.
>
>> Can you say more about how to use the MPTP system for doing one of the
>> recursive steps?  I'm interested in how (2) and (3) would work.
>
> Get mptp0.2 (http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp0.2.tar.gz),
> SWI prolog, edit the path at the top of utils.pl approprietly and
> create the "problems" directory inside the mptp directory, then load
> utils.pl into SWI, and run e.g.
>
> :- mk_first100.
>
> It will create the ATP problems for theorems from the first 100 MML
> articles. if you want all, run following instead:
>
> :-declare_mptp_predicates,load_mml,all_articles(L),!,member(A,L),mk_article_problems(A,[[mizar_by,mizar_from,mizar_proof],[theorem]],[opt_REM_SCH_CONSTS]),fail.

I downloaded mptp 0.2, loaded utils.pl into SWI prolog, but got an error
when I tried mk_first100.:

  ?- mk_first100.
  ERROR: source_sink `/sw/share/mizar/mml/xboole_0.xml2' does not exist 

What is the `xml2' doing there?

> It will take quite a while. This is (2), grep for fof([rcf]c[0-9]\+_ArticleName
> in the created problems to get the existential, conditional and
> functor registrations chosen by MPTP. If you want to try (3), paste
> the problem into the formula box at
> http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP, select EP 0.999 or
> SPASS 3.0 from the list of ATPs, and hope that they will solve the
> problem. If so, grep the resulting proof again (in case of E 0.999),
> or just the list of needed formulas (in case of SPASS 3.0).
>
> If you get that far, I promise to produce a new version of MPTP, based
> on the current MML soon :-).

Sounds great! :->  (But I didn't get that far because of the unexpected
`xml2' error.)

>> Option (1) may also work.  I would create one enormous MIZAR file
>> containing everything from the union of the articles metioned in the
>> environment of the article in which I prove x, and then write some code
>> to whittle away at the huge file until the removal of anything causes an
>> error which implies that the proof x is incorrect.
>
> Yes, there might even be similar utilities for "cleaning the
> environment" in the Mizar CVS. One danger of your approach (having all
> inside the article) is that some (possibly redundant) registrations
> will be needed for parsing other (possibly redundant) registrations,
> causing irrelevant errors.

True, that may happen, but it seems that one could deal with these "by
hand".  An entirely automatic solution would be nice, but I'm willing to
put in some local, non-automatic work into this project.

Thanks much,

Jesse

-- 
Jesse Alama (alama@stanford.edu)