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

[Jesse Alama <alama@stanford.edu>]

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)