Hi Jesse,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)