[Date Prev][Date Next] [Chronological] [Thread] [Top]

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



On Wed, 7 Nov 2007, Josef Urban wrote:


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.
One simple idea for doing this practically is to experiment with the Article.ecl file. This file contains all registrations imported from the article's environment, and removal of registrations from it should be OK (it will not cause parse errors to other items in it, because they are already parsed (in the XML form)).
So assuming that your Article contains only theorems, the method for determining environmental registrations needed for ThX is to: 
- delete all but ThX from Article
- accommodate
- check that Article is without verification errors (it should at this point) - try deleting one XML entry (RCluster,FCluster,CCluster) from Article.ecl at a time, followed by verification; if error occurs, keep the entry, otherwise get rid of it
If your Article contains registrations and definitions, the above procedure could again cause irrelevant parsing errors in registrations or definitions which are irrelevant for ThX. So the cleanest way is probably to move them all into another article, export that article into local DB, append it to (the stripped-down) Article's registrations, constructors, notations, and definitions directives, and only then use the above procedure on Article's theorems.
I think this could be reasonably fast (if not enough, a speed-up possiblity is to heuristically try to remove larger chunks instead of just one entry) and precise. For definitional expansions do the same with Article.dfs . The resulting info could really be incorporated e.g. in MMLQuery, and later in some wiki for MML. 

Josef



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


Hi Jesse,

sorry, I focused my reply on getting all article's external
references, not on getting transitively all "things needed" for
proving one theorem.

Getting transitively all REFERENCES (theorems, schemes, definitions)
used for a proof of one theorem is relatively easy, and you just apply
one of the methods I described recursively (so I would definitely use
the prolog (mptp) tools for this).

Getting (transitively) ALL THINGS NEEDED (e.g. also registrations) for
a proof of a theorem is quite difficult if you want to do it
precisely. The options (speaking just about one step in the recursion)
are:

1. Include all registrations mentioned in the theorem's article
environment, plus all registrations preceding the theorem in its
article. This is easy, but very imprecise.

2. Use MPTP's algorithm for creation of ATP reproving problems for the
theorem (or for an older version of MML, just find the ATP problem at
http://www.cs.miami.edu/~tptp/MizarTPTP/). It cuts down the redundant
registrations using syntactic criteria, while still saying on the safe
side.

3. Solve the ATP reproving problem using and ATP system, and look
which registrations were actually used in the proof. This is much more
precise, but sometimes hard to do, and also the set of "registrations
necessary for an ATP proof" may slightly differ from those needed for
the Mizar proof.


There are other "things needed" which are analogous to the
registrations (no easy documentation of their usage by the verifier),
e.g. definitional expansions done in the Checker module. The possible
solutions suggested above also apply to them.

Josef


On Tue, 6 Nov 2007, Jesse Alama wrote:


Hi Josef,

This looks great -- thanks.  I'm a bit unclear on how to use the results
of these tools.  And in any case, if I understand correctly, this solves
only part of the problem I have in mind.

I'd like to start with a theorem, say x, and prepare a customized MML
that consists of exactly those MIZAR items that are used to get x.  The
idea is to compute the smallest set S of MIZAR items such that if any
item were taken away from S, there would no longer be a MIZAR proof of x
or x would no longer be a well-formed formula.

It seems to me that the tools you mention go some way toward achieving
this, but it seems that they go only one step of the way.  But perhaps
I'm misunderstanding something about the tools.  Can you clarify?

Thanks much,

Jesse

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


One option is just to grep article's XML form for "Ref" (postprocess
the XML with addabsrefs.xsl first, to get absolute names of
refrences). Throw away those which do not have the @articlenr
attribute (these are local references). A formally more correct way
would be to use an XPath expression (//Ref[@articlenr]) (see
e.g. http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl?rev=1.2&view=auto) 
on the XML, but in this case grep is enough, because the Refs occupy
always exactly one line in the XML. Of you also want schemes, grep
also for "From".

Another option is to additionally postprocess the XML with mizpl.xsl
(all these stylesheets are at
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/xsl4mizar/), and use
prolog on the resulting TPTP formulas. Again an easy way is just to
find there all symbols of the form [tds][0-9]+_articlename . With some
knowledge of the TPTP format, it should be easy to figure out where
the references reside in the data, and thus which
theorem/registration/definition uses them. (Again, this is also easy
using and XPath expression directly on the XML).

Josef

On Mon, 5 Nov 2007, Jesse Alama wrote:


I'd like to start with a proof of a theorem in MIZAR and calculate the
transitive closure of the "x uses y" relation for both local articles
and articles in the MML. What I have in mind is not only the transitive 
closure of the "refers to" relation (the proof of x uses y), but also
things like registrations and proofs of existence and uniqueness for
functors, etc.  What tools can I use for this purpose?  I'm prepared to
write some code to help me with this, but I thought I'd ask the list to
see whether anyone knows how this might be accomplished with existing
tools (e.g., mmlquery).  Any ideas?

Thanks,

Jesse

--
Jesse Alama (alama@stanford.edu)





--
Jesse Alama (alama@stanford.edu)






--
Jesse Alama (alama@stanford.edu)