*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)*From*: Jean Martina <Jean.Martina at cl.cam.ac.uk>*Date*: Tue, 12 Oct 2010 12:31:17 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <B6942165-3A0E-439A-8D76-7468A5468ADE@gmail.com>*References*: <AANLkTimCR2asEkXW7+-tj9WAWjbwUzKkBmYCgzb4-kS6@mail.gmail.com> <E5F2B2B2-3D38-4BD5-BA8C-E81AF9A7D3F9@gmail.com> <47ADF916-B724-4051-861E-9B95AE342058@cl.cam.ac.uk> <B6942165-3A0E-439A-8D76-7468A5468ADE@gmail.com>*Sender*: "J.E. Martina" <jem74 at hermes.cam.ac.uk>

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

**References**:**[isabelle] HOL/Auth subgoal (Nonce secrecy)***From:*Denis Butin

**Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)***From:*Jasmin Blanchette

**Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)
- Next by Date: Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)
- Previous by Thread: Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)
- Next by Thread: Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list