Hi Bill, I understand exactly what you are looking for (or at least I think I do!) - a theorem prover with very clearly defined functionality, that automates what is "trivial" and does not automate what is not "trivial", and that is easy to use, caters for all the classic styles of doing (symbolic) proof on paper and does not require months of training. And if this system is also a "serious" system involved in the formalisation of mathematics, and is highly trustworthy, then all the better. You see such a system as being an excellent way of teaching students how to do proof.
As you say, Mizar and miz3 (and don't forget Isar) perhaps come about the closest of any current systems to what you want. I've had in mind for many years a design of a system that does exactly what you want, but have been too busy with other stuff to develop this up till now. I suppose this doesn't really help you until it's been implemented, but I just wanted to tell you that! I suppose a problem with using existing systems is that they are trying to do something different - to enable proofs to be proved with minimal amount of user effort. Sometimes the approach they use to achieving this means that they come close to your goals, but they will never be perfect for what you want. By the way, "malicious" proofs are not proofs that use a theorem prover's automatic facilities when they are not intended to be used. Malicious proofs are proofs that deliberately take advantage of unsoundness (or other trustworthiness issues) in the theorem prover, to prove a fallacy, or to appear to prove a fallacy. Mark. on 6/7/12 7:45 AM, Bill Richter <[email protected]> wrote: > 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. > > .... > > 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. ------------------------------------------------------------------------------ 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
