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

[Michael N. <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