Thanks a lot Freek! I'll go fix my `o's. I'm completely satisfied
with your explanation of miz3 error messages. I sure thought this
didn't work in miz3, but maybe I goofed, and I'll go check:
>But in Mizar we can also write more simply
>
> consider x such that
> Between (b,x,b) /\ Between (a,x,a) by -, H1, A7 [X1];
2-column proofs are what kids do in a US high school Geometry class,
so the statements are numbered in the left margin 1, 2, 3, ... and in
the right hand column you give reasons that are often earlier numbers.
It would be nice to be able to use that convention in miz3. BUT:
I think you can't change the position of labels, and I withdraw my
request. Your 1201.3601v2.pdf precisely explains the miz3 grammar
(Fig 1 on p 16), and in particular
<proof step> ::= <formula> <labels> <proof> | ...
That looks great, and I can't ask you to change that. I have other
three other problems with 1201.3601v2.pdf.
1) Minor cases problem: The cases fork in <proof step> says
cases <by refs> ; ....
and <by refs> is defined to always begin with `by'. As we agree, this
isn't always true.
2) You write <proof step>* twice in your grammar, which I think means
any non-negative number of proof steps. But I think you need at least
on proof step, so that you should have written <proof step>+, as you
do in the `now' fork of <proof step>. Maybe I'm wrong about * & +
(that's the Emacs regexp convention), and maybe I'm wrong about miz3.
3) More substantively, on p 14 you write
We now present the meaning of the miz3 language.
I'd like to see that explained much better. The problem is that there
isn't, I think, any good explanation of the meaning of Mizar. You continue:
It is almost exactly the same as that of the Mizar language [20].
That's a 93 page article I've gleaned lots of important bits from, but
I did not see the meaning of Mizar. Maybe I missed it.
At every step in a proof there is a designated statement called the
thesis. This is the statement that is being proved (the goal of a
procedural prover). Subproofs have their own local thesis. Now
steps can add extra variables and statements to the proof context,
but can also change the thesis. If that happens the step is called
a skeleton step.
I didn't know any of this. Thanks for explaining.
Here is a table that summarizes the main miz3 proof steps:
I didn't get much out of the table, but I've certainly seen similar
Mizar tables.
This then is the basic miz3 proof language.
Well, I'd like to see more. Now that I pretty much understand the
grammar and your thesis discussion, I can take a hack at it myself.
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
