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



Hi Jean,

(I'm taking the liberty of answering to the mailing list.)

> From my own trial and error experiences in this specific domain inside Isabelle, E and vampire tend to give a lot of ill-typed translations.
> 
> 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.

> If you enable fuil_types, you need around 5 times more CPU time to arrive to the same results (again just considering this domain, I did the test 2 years ago), so in the end it is worth to get some ill-typed results that you can sieve out quickly.

And have you tried playing with the "no_atp" (previously "noatp") attribute? Unsound proofs tend to always involve the same facts, and using this tag you can instruct Sledgehammer to leave them out. Alternatively, with 2009-2, you can try the syntax

    sledgehammer (del: evil_facts_go_here)

We haven't given up all hopes of coming up with a sound (or at least sounder) yet efficient encoding for Sledgehammer, but in the meantime these are the workarounds.

Regards,

Jasmin






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