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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
