Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)



On 12 Oct 2010, at 12:05, Jasmin Blanchette wrote:

>> SPASS on the other hand don't do that often. A critical issue in his initial problem is the willing to inspect the analz set. I would say (empirically again) that 80% of sledgehammer's output in this situation is ill-typed.
> 
> That's a lot (Nipkow & Boehme found it was < 10% on their test data), but it's known to vary from theory to theory. SPASS is usually run with the SOS (set of support) strategy, which might make it less likely that it finds (untyped) contradictions between the included facts.

This number i cited above is a specific case where sledgehammer need to deal with the analz function. Probably it does not have anything to do with Sledgehammer, but with the way things are thrown to it.  I noticed that the rate of success of sledgehammer is dependent on the way you generate and prepare the subgoals to be sledgehammered. 

Jean




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.