Re: [mizar] question about dependence operator in mmlquery

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

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

Josef