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

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 amou

[Hol-info] CALL FOR PAPERS: SPIN 2011 ** EXTENDED DEADLINE APRIL 15 **

[Apologies if you receive multiple copies] *** Call for Papers: SPIN 2011 18th Int. SPIN Workshop on Model Checking of Software July 14-15, Snowbird, Utah, USA Co-located with CAV 2011 *

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

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

[Hol-info] [fm-announcements] RV 2011 - 2nd Call for Papers and Tutorials

2nd Call for Papers and Tutorials International Conference on Runtime Verification (RV 2011) September 27 - 30, 2011 San Francisco, California, USA http://rv2011.eecs.berkeley.edu/ Runtime verification (RV) is concerned with monitoring and analysis of software or hardware system executions. The

[Hol-info] [fm-announcements] NFM 2011 - call for participation

CALL FOR PARTICIPATION NFM 2011 Third NASA Formal Methods Symposium Pasadena, California, USA April 18 - 20, 2011 http://lars-lab.jpl.nasa.gov/nfm2011 THEME

[Hol-info] Major upgrade to HOL-Omega

I'd like to announce a major upgrade to the HOL-Omega logic and system. The major change is deep but important: whereas ranks were previously an attribute of types, they are now made an attribute of kinds, specifically of both the base kind and kind variables. This enables the kind of a type oper