On 06/07/12 16:44, Bill Richter 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.
miz3 is not constructing a Mizar proof, nor even a "miz3" proof. Rather it is constructing a proof in higher-order logic, ultimately using the primitive rules of inference of higher-order logic. (See the HOL4 Logic manual for a presentation of one set of primitives.) That is the "ground truth" of the system and attempting to recast things at a higher level of abstraction is always going to be a bit fraught. Certainly, miz3 presents an appealing interface that lets the user think they are working at a rather higher level. It's an illusion, but a reasonably convincing one. The illusion hangs together because the engineering heuristics that Freek and John have put together mean that the steps that a human thinks should be obvious are ones that the system often accepts too. But this stuff really is a matter of heuristics: - What should the timeout be? - Should simplification precede attempts at first order reasoning? - If so, how much should be allowed? - What default simplification rules should be included (if any)? - What proof search strategy should be used when doing the f.o. reasoning? - etc If you hit the sweet spot, then the system lurking behind "by" doesn't prove so much that the user doesn't learn anything, but isn't so stupid that the human has to provide unnecessary detail. Ultimately, I'm afraid there is no precise way of explaining what Mizar/miz3 are capable of for your paper. You can only point to experience, and say that the system behind "by" seems to allow reasonable leaps of inference. Note that a Mizar/miz3 proof is probably fairly solid in the face of changes to the underlying systems, but if its reasoning power (remember how this depends on those heuristics) doesn't always increase then it's possible (though unlikely I suspect) that a proof that worked yesterday won't work today. If you haven't already been pointed at John's 1996 paper about the original Mizar mode for HOL Light, then I certainly recommend it: http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html Michael ------------------------------------------------------------------------------ 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
