OK I guess your problem is that you don't know how powerful (in the
automation dimension) each of the miz3 keywords is, so you wouldn't know
which ones to include in your restricted set anyway.
For that you will have to search for documentation, read the miz3 code, or
wait for someone who knows to answer because unfortunately I don't :)
On Fri, Jul 6, 2012 at 8:17 AM, Ramana Kumar <[email protected]> wrote:
> If there are powerful theorem provers that can prove every result in the
> course, you should think hard about the value you are imparting to your
> students by making them write proofs in a restricted language, and design
> that language accordingly.
>
> I feel like maybe you didn't understand what I said, so let me try one
> thing again: miz3 is an OCaml library that defines a bunch of functions and
> stuff that make up what looks like a proof language, but ultimately the
> proofs that are checked by the proof assistant are the low level higher
> order logic proofs that those functions create. The proof assistant does
> not care whether they were generated by miz3 functions or by MESON or by
> anything else: in fact, it does not know! Perhaps it would be instructive
> for me to show you the OpenTheory proof for one of your theorems, that is,
> a proof you might have thought you never wrote but actually is what is
> generated - if so, let me know and I'll try to get Joe's proof-logging fork
> to run your code some time.
>
> It sounds like what you want is control over which functions your students
> are allowed to call when they're trying to write proof scripts (that is,
> code to create low level HOL proofs).
> Well, that's easy: write down the list of functions (or miz3 keywords or
> whatever) that you want them to be allowed to use, make an OCaml module out
> of it, tell them to import that module and forbid them (verbally, or
> manually, or you could write a script to check their source files if you
> don't trust them) from importing anything else or from defining their own
> functions.
>
>
> On Fri, Jul 6, 2012 at 7:44 AM, Bill Richter <
> [email protected]> wrote:
>
>> Thanks, Ramana! You explain very well I think how I could check what
>> proofs I'm getting, and why HOL Light is reliable. That's really
>> valuable information, but it's not what I want. Let me try again.
>>
>> The fact that HOL Light (using miz3) checks my proofs conclusively
>> tells me that my theorems are correct. I just proved a new one:
>>
>> OrderedCongruentAngles_THM : thm =
>> |- ∀ A O B A' O' B' G.
>> ¬Collinear A O B ∧ ¬Collinear A' O' B'
>> ⇒ angle A O B ≡ angle A' O' B'
>> ⇒ G ∈ int_angle A O B
>> ⇒ (∃G'. G' ∈ int_angle A' O' B' ∧ angle A O G ≡ angle A' O' G')
>>
>>
>> http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
>> I'm not worried that the theorem might actually be false.
>>
>> My question is: What kind of proof is miz3 saying I have? Recall that
>> my long-term purpose is to teach a rigorous axiomatic high school
>> Geometry course. There must be powerful theorem provers that could
>> prove every result in the course! Josef got Vampire to prove most of
>> my Tarski miz3 results. So I'd like to know that miz3 isn't powerful
>> enough to make it useless for teaching Geometry! I think miz3 is just
>> about right, from my experience of 2350 lines of Hilbert axiomatic
>> code and 985 lines of Tarski code, but I'll never be sure until I know
>> what miz3 calls a proof. Part of the problem is that there's no
>> documentation for exactly what a Mizar proof is. Again, from my
>> original Tarski code experience, I think Mizar is about the right
>> level of power. But I don't know, and can't explain it in my paper.
>>
>> So I can read "fusion.ml", and kananaskis-7-logic-1.pdf, as you
>> suggested, and learn what a HOL proof. That's great. But miz3 proofs
>> are much simpler. John's book (which I haven't understood yet)
>> clearly explains (I think) what John means by a Mizar-like FOL proof.
>> I was hoping someone would explain this to me, and then explain how
>> John's purple book Mizar-like FOL compares to miz3. Maybe I'll have
>> to explain it myself, after learning it. I have time, as I have 6
>> more tough pages in my paper to formalize before I'll submit my paper
>> http://www.math.northwestern.edu/~richter/hilbert.pdf
>>
>> Here's my hazy idea. I more or less know what an FOL proof is, and I
>> think writing them down is tedious, and we'd like a proof assistant to
>> automate the tedious details (substituting variables etc) , so we're
>> left with the interesting part of the FOL proof. I think this is what
>> Mizar, John's Mizar-like FOL, and miz3 all do. But I'd like to know
>> for sure, and more precisely, exactly what automation they do.
>>
>> It's never happened that when I ``intentionally'' wrote up a miz3
>> proof, that miz3 proved the theorems before I thought I had completed
>> the proof. That's what I want. But once I goofed in my miz3 proof,
>> miz3 approved a proof that I didn't think was a proof. Freek
>> explained that MESON is quite powerful, and explained how MESON proved
>> my result. So as long as I don't goof like that, I'm OK. But could
>> my students exploit the power of MESON to hand in miz3 proofs that I
>> wouldn't call proofs? I know issues like this get discussed here,
>> maybe it's called `malicious' proofs. I'm not really worried about
>> malice, and I'd be thrilled to have any students, but the teacher
>> ought to know what the proof assistant will accept as a proof.
>>
>> --
>> 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
