Re: [mizar] question about dependence operator in mmlquery

[Jesse Alama <alama@stanford.edu>]

Hi Josef,

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

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

I'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?  (Also, I find Mizar.html a bit too
cryptic; from an outsider's perspective, it seems to be a inexplicable.)

Perhaps those who work on MMLQuery can explain just what the dependence
operator means.

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)