Re: [Hol-info] useful HOL statistics to show the amount of proof work?
On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote: This is particularly dangerous when I have proof automation scripts that try different rewriting rules. The number reported is not representative on the complexity of the problem, but the number of inference steps conducted by HOL, which is not necessarily related to a correct proof construction that actually verifies a theorem. Since HOL is not designed for automatic reasoning, I can't let this one by. HOL is designed to allow one to automate as much reasoning as possible with tactics. Whether or not good enough automation tactics have been written is another story, but I think there are quite good ones (including integrations with other, stronger purely automatic tools). so reporting the number of inference steps can be misleading in measuring the implementation complexity of solving problems, especially when using proof automation scripts with lots of rewriting rules. Now, to answer your question, as Michael suggested you may find using the Opentheory proof-logging kernel useful. It builds a proof object for every theorem, so once your final theorem is proved you can simply count the number of inference steps in its proof. This will not count any of the inference steps built along the dead-end attempts. (Indeed if you export the theorem into an Opentheory article, the opentheory tool (not include with HOL) will perform easy simplifications on the proof and count the primitive inferences by type for you.) Lu On 04/07/2011 11:29 AM, Lu Zhao wrote: I found out in Count.sml that there are other utilities available, too. For example, you can use the following to start counting: val meter = Count.mk_meter(); and use Count.report(Count.read meter); to see the statistics, after whatever operations you do. Best, 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] useful HOL statistics to show the amount of proof work?
Ramana Kumar wrote: On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote: This is particularly dangerous when I have proof automation scripts that try different rewriting rules. The number reported is not representative on the complexity of the problem, but the number of inference steps conducted by HOL, which is not necessarily related to a correct proof construction that actually verifies a theorem. Since HOL is not designed for automatic reasoning, I can't let this one by. HOL is designed to allow one to automate as much reasoning as possible with tactics. Whether or not good enough automation tactics have been written is another story, but I think An important part of this story is the fact that the tools are there for you to write your own according to the features of the problem at hand, so long as you are comfortable with not-quite-trivial Standard ML programming. Jeremy there are quite good ones (including integrations with other, stronger purely automatic tools). so reporting the number of inference steps can be misleading in measuring the implementation complexity of solving problems, especially when using proof automation scripts with lots of rewriting rules. Now, to answer your question, as Michael suggested you may find using the Opentheory proof-logging kernel useful. It builds a proof object for every theorem, so once your final theorem is proved you can simply count the number of inference steps in its proof. This will not count any of the inference steps built along the dead-end attempts. (Indeed if you export the theorem into an Opentheory article, the opentheory tool (not include with HOL) will perform easy simplifications on the proof and count the primitive inferences by type for you.) -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] useful HOL statistics to show the amount of proof work?
Using the following method has some problems, when there are failures in proof attempts. For example, the following sequence reports 44 primitive inference steps, after a proof failure. val meter = Count.mk_meter(); g `p /\ p /\ q /\ F`; e (METIS_TAC []); Count.report(Count.read meter); This is particularly dangerous when I have proof automation scripts that try different rewriting rules. The number reported is not representative on the complexity of the problem, but the number of inference steps conducted by HOL, which is not necessarily related to a correct proof construction that actually verifies a theorem. Since HOL is not designed for automatic reasoning, so reporting the number of inference steps can be misleading in measuring the implementation complexity of solving problems, especially when using proof automation scripts with lots of rewriting rules. Lu On 04/07/2011 11:29 AM, Lu Zhao wrote: I found out in Count.sml that there are other utilities available, too. For example, you can use the following to start counting: val meter = Count.mk_meter(); and use Count.report(Count.read meter); to see the statistics, after whatever operations you do. Best, 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] useful HOL statistics to show the amount of proof work?
This is certainly true. Of course, it all depends on what you're trying to measure. If you're interested in the size of the natural deduction proof that actually establishes a particular theorem, you really need to try something like: extracting the proof using some sort of recording machinery (opentheory, say), and then analysing the result to prune away unneeded bits of work. This would measure the true size of the theorem's actual proof. It would not measure the amount of mechanical or human work required to *find* the proof though, and that's presumably quite an interesting statistic too... Michael On 21/05/12 12:29, Lu Zhao wrote: Using the following method has some problems, when there are failures in proof attempts. For example, the following sequence reports 44 primitive inference steps, after a proof failure. val meter = Count.mk_meter(); g `p /\ p /\ q /\ F`; e (METIS_TAC []); Count.report(Count.read meter); This is particularly dangerous when I have proof automation scripts that try different rewriting rules. The number reported is not representative on the complexity of the problem, but the number of inference steps conducted by HOL, which is not necessarily related to a correct proof construction that actually verifies a theorem. Since HOL is not designed for automatic reasoning, so reporting the number of inference steps can be misleading in measuring the implementation complexity of solving problems, especially when using proof automation scripts with lots of rewriting rules. Lu On 04/07/2011 11:29 AM, Lu Zhao wrote: I found out in Count.sml that there are other utilities available, too. For example, you can use the following to start counting: val meter = Count.mk_meter(); and use Count.report(Count.read meter); to see the statistics, after whatever operations you do. Best, 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info signature.asc Description: OpenPGP digital signature -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] useful HOL statistics to show the amount of proof work?
Thanks Lu! And thanks for Dr. Michael Norrish! Sorry I'm not familiar with Structure Count. Now, I got it! Best Wishes, Liya Quoting Michael Norrish michael.norr...@nicta.com.au: 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] useful HOL statistics to show the amount of proof work?
On Thursday 07 April 2011 02:07:11 am Michael Norrish wrote: 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``; ... 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. I don't know that the strength of modern theorem provers is the number of primitive inferences (the number of steps in the proof) they make. Rather it is pruning the search tree of all possible proofs. In theory one could build a prover that simply tries all possible proof steps in a breadth-first search. Unfortunately the universe would reach heat death before useful results were returned, so great is the branching in the search. A better measure of the cleverness and power of a theorem prover might be the size of potential search space. For instance, it may have taken n steps, but there were 10^10^n steps that it (and those who programmed it) might have taken, but did not even search. -paul- -- Paul E. Black 100 Bureau Drive, Stop 8970 paul.bl...@nist.gov Gaithersburg, Maryland 20899-8970 voice: +1 301 975-4794fax: +1 301 975-6097 http://xlinux.nist.gov/~black/KC7PKT -- 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
