This is certainly true. Of course, it all depends on what you're trying to measure. If you're interested in the size of the natural deduction proof that actually establishes a particular theorem, you really need to try something like: extracting the proof using some sort of recording machinery (opentheory, say), and then analysing the result to prune away unneeded bits of work. This would measure the true size of the theorem's actual proof. It would not measure the amount of mechanical or human work required to *find* the proof though, and that's presumably quite an interesting statistic too...
Michael On 21/05/12 12:29, Lu Zhao wrote: > 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 >> [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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
