On 28/08/12 13:29, Bill Richter wrote: >> Yes, Mizar is certainly shackled in the way Michael described.
> I can't figure out your position. I agree there might be some value in > shackling for retrieval from huge libraries. Why don't we concentrate on > education. I contend that shackling the students' proof assistant is bad > design. Michael did not say this, but I say it after listening to Michael, > and I'm glad that miz3 is not shackling the students (me, right now). We can imagine two sorts of student here. One is the person who is mathematically sophisticated but a novice as far as theorem-proving is concerned. This person (i.e., Bill) manifestly doesn't want a "shackled" backend prover. However, if the student has little sophistication when it comes to writing proofs, I think there are two advantages in having a shackled prover: 1. the student doesn't waste time waiting for the prover to give up on unrealistic or unprovable goals. Fast feedback is universally recognised as a good thing when using a system: having it come back fast and say "No. Make your proof better" has to be a good thing for learning how to make better proofs. 2. if the student does occasionally get the backend prover to fluke a hard result, they miss out on the pedagogically valuable exercise of actually proving that result. Do you really want a student to be able to come back to you with that theorem due to Los, and say "Oh, I proved it by waiting for meson to finish." Bill thought that proving it by hand was interesting and valuable, and discussed Rob Arthan's proof at length. Surely the value that Bill derived from that exercise would be just as great for students. 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
