On Mon, May 21, 2012 at 3:29 AM, Lu Zhao <[email protected]> wrote: > This is particularly dangerous when I have proof automation scripts that > try different rewriting rules. The number reported is not representative > on the complexity of the problem, but the number of inference steps > conducted by HOL, which is not necessarily related to a correct proof > construction that actually verifies a theorem. > > Since HOL is not designed for automatic reasoning,
I can't let this one by. HOL is designed to allow one to automate as much reasoning as possible with tactics. Whether or not good enough automation tactics have been written is another story, but I think there are quite good ones (including integrations with other, stronger purely automatic tools). > so reporting the > number of inference steps can be misleading in measuring the > implementation complexity of solving problems, especially when using > proof automation scripts with lots of rewriting rules. Now, to answer your question, as Michael suggested you may find using the Opentheory proof-logging kernel useful. It builds a proof object for every theorem, so once your final theorem is proved you can simply count the number of inference steps in its proof. This will not count any of the inference steps built along the dead-end attempts. (Indeed if you export the theorem into an Opentheory article, the opentheory tool (not include with HOL) will perform easy simplifications on the proof and count the primitive inferences by type for you.) > > Lu > > On 04/07/2011 11:29 AM, Lu Zhao wrote: >> I found out in Count.sml that there are other utilities available, too. >> For example, you can use the following to start counting: >> >> val meter = Count.mk_meter(); >> >> and use >> >> Count.report(Count.read meter); >> >> to see the statistics, after whatever operations you do. >> >> Best, >> Lu >> >> ------------------------------------------------------------------------------ >> Xperia(TM) PLAY >> It's a major breakthrough. An authentic gaming >> smartphone on the nation's most reliable network. >> And it wants your games. >> http://p.sf.net/sfu/verizon-sfdev >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ > 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 ------------------------------------------------------------------------------ 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
