[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Reference distances?
Hi Freek,
Yes, I know all this. But I am not able to measure the
"distance" of the references to theorems from other articles,
One way to do this is to imagine all of MML merged into one big article (
in the processing order givan by $MIZFILES/mml.lar). Other way is to do
this separately for each article according to its environment, etc.
and _most_ of the "top level" references seem to me of a
similar kind. So I thought I should treat them similarly,
i.e., ignore them.
OK, it's your choice, for basic statistics it should be sufficient. In
MPTP 0.2. the top-level non-theorem lemmas are actually also handled a bit
differently from other propositions, so their naming starts with "l"
(e.g. l1_card_1) instead of "e". So it should be easy for you to filter
them out.
One more question: can you clarify the outcome of the "sed"
command you mentioned to me? For instance, suppose that I
have a proof:
proof
assume
A1: ... and
A2: ...;
consider ... such that
A3: ... and
A4: ... by ...;
thus
A5: ... by ...;
end;
Then I have five labels, but only two justifications. So
what would the structure of the output of the sed command
that you gave be like in this case. Would it have two
lines? Or five? Or seven?
The "sed" was preceded by "grep mizar_by", which selects just the
propositions with the "by" justification. So you would get two lines from
above. I think the "consider" item needs a bit of explanation (cf. the
XML description at http://lipa.ms.mff.cuni.cz/~urban/Mizar.html#Consider).
The "by-justified" proposition for it is something like:
(e3) ex ... st A3 & A4 by ...;
This proposition is hidden from the Mizar author - he cannot quote it, but
it is present as a regular proposition in Mizar and in MPTP, so MPTP gives
it a name (e3) too. The quotable propositions A3 and A4 are "justified" by
this proposition, and they come right after it, so their MPTP names are
"e4" and "e5". Similar thing happens e.g. for "reconsider", "per cases",
etc. So in the MPTP numbering, there are usually more labels than it is
theoretically possible to have in the Mizar article - simply every
Proposition (http://lipa.ms.mff.cuni.cz/~urban/Mizar.html#Proposition)
gets a number, regardless if "quotable" or not.
So for your example there are six Mizar (and MPTP) propositions, and two
of them have the mizar_by inference slot in MPTP.
(I could try to find proofs like this in the library and look
at what actually happens there, but maybe it becomes clearer
if you explain it.)
Experimenting should be quite simple:
mizf foo.miz # creates foo.xml
xsltproc addabsrefs.xsl foo.xml > foo.xml1 # makes rich xml
xsltproc mizpl.xsl foo.xml1 > foo.xml2 # makes the MPTP file
addabsrefs.xsl and mizpl.xsl are in the MPTP distro, or at
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/xsl4mizar/ .
Best,
Josef