Hi Jesse, On Fri, 14 Dec 2007, Jesse Alama wrote:
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
Did you set the mml_dir path at the top of utils.pl to the location of the 'pl' directory in the unpacked distro?
What is the `xml2' doing there?
The .xml2 is a default extension for the prolog form of whole mizar articles. The food chain is .xml (creatde by verifier) -> .xml1 (created by addabsrefs.xsl) -> .xml2 (created by mizpl.xsl).
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.
I would advise against doing anything excessively non-automatic when processing MML. New MML versions arrive in fast rate, and repeating large amount of manual work for them gets quickly very boring.
Josef