Re: [Hol-info] useful HOL statistics to show the amount of proof work?

[<li...@en...>]

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 <Mic...@ni...>:

> 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
>
>
>