On Thursday 07 April 2011 02:07:11 am Michael Norrish wrote: > On 07/04/11 14:19, Lu Zhao wrote: > > First, please forgive me if this question is too silly. I had this > > question when I talked to a colleague, who has no idea about theorem > > proving at all, about the amount of proof work that can be involved > > in solving a problem. How to evaluate the amount of proof work that HOL > > does? What are the statistics that I can use, and how to get them > > in HOL? > > I don't think this is a silly question! > > I'd use Count.apply: > > Count.apply (REWRITE_CONV []) ``p /\ T /\ q``; > ... > The number of primitive inferences something takes is a good measure of > the logical complexity of the problem, at least as far as that problem's > implementation.
I don't know that the strength of modern theorem provers is the number of primitive inferences (the number of steps in the proof) they make. Rather it is pruning the search tree of all possible proofs. In theory one could build a prover that simply tries all possible proof steps in a breadth-first search. Unfortunately the universe would reach heat death before useful results were returned, so great is the branching in the search. A better measure of the cleverness and power of a theorem prover might be the size of potential search space. For instance, it may have taken n steps, but there were 10^10^n steps that it (and those who programmed it) might have taken, but did not even search. -paul- -- Paul E. Black 100 Bureau Drive, Stop 8970 paul.bl...@nist.gov Gaithersburg, Maryland 20899-8970 voice: +1 301 975-4794 fax: +1 301 975-6097 http://xlinux.nist.gov/~black/ KC7PKT ------------------------------------------------------------------------------ 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
