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)