Rob, thanks for explaining your ProofPower proof was shorter than mine. I went to your ProofPower web site, and it sounds similar to HOL Light. Is it easy to port code from one to the other? You must be a HOL Light expert, because John H thanked you (along with Freek W and Michael N) in his purple book.
Ars longa, vita brevis. Chaucer's version is "Life is so short, and the craft takes so long to learn." But I think it would be easy for you to paste my miz3 code into a ocaml/HOL-Light process window, and then maybe fiddle with the code, make the proof shorter or longer. Anyway, thanks for explaining your excellent solutions of Los's Logic problem, which previously it seemed that only MESON could solve. -- 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
