Hi, 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?
Before I speak of HOL, an example I think can help illustrate my question is that SMT solvers often say "the number of clauses" that can be solved. When someone who does not know an SMT solver hear that a solver could solve 200 clauses 15 years ago but now can solve 2,000,000 clauses, she knows that there is big difference, because there is a huge gap between these two numbers: 200 vs 2,000,000. The numbers make her feel there is a difference. Now, come to HOL. What number should I use to convey the amount of work in a proof? Or something else if not a number. Some examples popping out in my mind are: the number of tactics used (may be silly), the number of rewriting steps, or ... Thanks. Lu ------------------------------------------------------------------------------ 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
