Hi Jesse, On Sun, 4 May 2008, Jesse Alama wrote:
Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:On Sat, 3 May 2008, Jesse Alama wrote:I'm interested in fine-grained dependency analysis of proofs in mizar....when I query `dependence ENUMSET1:func 1'. Rather, I'd like to focus on the existence and uniqueness proofs for ENUMSET1:func 1. As it stands, that seems to be the meaning of `dependence ENUMSET1:def 1', but with an additional twist: ENUMSET1:def 1 depends on ENUMSET1:func 1. Does anyone have any idea how I might carry out that kind of analysis using mmlquery (or any other tools, for that matter)?You can use XPath/XQuery directly on the XML form of articles (perhaps after running through addabsrefs.xsl). E.g. Existence//Ref will collect references inside an Existence block, see Mizar.html for the xml description, and e.g http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl for a Perl exampleI'm afraid I'm a bit of a neophyte when it comes to XPath/XQuery. Can you say a bit more about how I can use to collect, for example, all references within a theorem?
say for ABCMIZ:1 the following XPath expression can be used //JustifiedTheorem[@aid="ABCMIZ_0" and @nr="1"]//Ref
(Also, I find Mizar.html a bit too cryptic; from an outsider's perspective, it seems to be a inexplicable.)
I don't say the documentation of the XML format is perfect. It probably requires some knowledge about how Mizar works, though some parts could be quite easy to understand. Also it is quite new, and I am probably the only regular user so far. But certainly, I can extend the documentation if there is enough interest and feedback. Also, it may really be quite low-level for immediate query usage by outsiders, it is more intended as an API for easy building of nice interfaces like MML Query, collecting and transforming a lot of data from MML, etc.
Josef