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
