A very interesting question and a wonderful answer! Maybe I will ask a silly question here:
I would like to know how we can collect these information, I mean the run time, gctime, and primitive inference steps and so on, especially in HOL4. Best Wishes, Liya Quoting Michael Norrish <[email protected]>: > 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``; > runtime: 0.000s, gctime: 0.000s, systime: 0.000s. > Axioms asserted: 0. > Definitions made: 0. > Oracle invocations: 0. > Theorems loaded from disk: 0. > HOL primitive inference steps: 2. > Total: 2. > val it = > |- p ? T ? q ? p ? q > : thm > > 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. > > Michael > > > ------------------------------------------------------------------------------ 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
