Bill, On 30 Jul 2012, at 09:31, Bill Richter wrote:
> https://dl.dropbox.com/u/34693999/nonobv.pdf > > Rob, thanks for the acknowledgment and modifying your proof 2 of Los's Logic > result. Sorry for posting my code yesterday with my Isabelle-type fonts > still in. I'm including the version which runs in HOL Light. I recommend > you learn miz3, One day maybe. Ars longa, vita brevis. > and I coded up your proof 2 in miz3 to get you started. I didn't understand > your declarative ProofPower proof 2 formalization, but I know mine is a lot > shorter. No, it's not. The ProofPower proof involves 29 non-comment lines of ML and 9 of those are boiler-plate. Your miz3 version is 52 lines of code. The document I posted includes commentary and pasted-in output from the tool to show what is going on. > Regards, Rob. ------------------------------------------------------------------------------ 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
