Ramana Kumar wrote: > On Mon, May 21, 2012 at 3:29 AM, Lu Zhao <luz...@cs.utah.edu> 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 > An important part of this story is the fact that the tools are there for you to write your own according to the features of the problem at hand, so long as you are comfortable with not-quite-trivial Standard ML programming.
Jeremy > 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.) > > ------------------------------------------------------------------------------ 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
