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
That's easy, Ramana, I want my students to learn how to write mathematical proofs! I think that's a valuable skill. Thanks for explaining in more detail how miz3 & Ocaml work. 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. That would be instructive if apply OpenTheory to my code! -- 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
