Using the following method has some problems, when there are failures in proof attempts. For example, the following sequence reports 44 primitive inference steps, after a proof failure.
val meter = Count.mk_meter(); g `p /\ p /\ q /\ F`; e (METIS_TAC []); Count.report(Count.read meter); 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, 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. 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 > hol-info@lists.sourceforge.net > 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
