[isabelle-dev] Two new experimental features in Sledgehammer

Jasmin Blanchette jasmin.blanchette at ifi.lmu.de
Fri Mar 10 11:07:58 CET 2023

Hi Tobias,

Thanks for sharing the example. I hadn't thought that wrong missing assumptions might be correlated with wrong conjectures!


> On 10 Mar 2023, at 11:05, Tobias Nipkow <nipkow at in.tum.de> wrote:
> Jasmin,
> Abduction: I just saw
> e: Candidate missing assumption:
> length xs + 1 = length xs
> and decided that there was probably somethig wrong with my goal, and it was. Had s/h just failed, I might not have drawn that conclusion.
> Tobias
> On 07/03/2023 17:59, Jasmin Blanchette wrote:
>> Hi all,
>> I have recently implemented two new features in Sledgehammer and would be grateful for your feedback before the release. One feature is some form of falsification or counterexample search, the other one is a form of abduction (inference of missing assumptions).
>> Perhaps the best explanation is an example. Suppose you state the goal
>> 	lemma "x - y + y = (x::nat)"
>> Notice that the condition "y <= x" was forgotten. In the "falsification" mode, which is run in parallel with the regular mode, Sledgehammer will add "!!x y. x - y + y = (x::nat)" to the theory and try to derive False. In this case, it will succeed and print
>> 	vampire found a falsification...
>> 	vampire: The goal is falsified by these facts: gt_ex, le_add2, order.strict_iff_not
>> The list of facts is probably of limited use in practice, but at least we're alerted to the goal's likely unprovability. (If the context is consistent but the goal isn't consistent with it, as is the case here, then the goal is not provable.)
>> On the same example, if the first feature didn't kick in, then the second feature, "abduction", would have:
>> 	e: Candidate missing assumption:
>> 	y < x
>> Here, E basically says: "I would be able to prove the goal if you added the assumption y < x." Note that this is not the best assumption possible -- that would be "y <= x" -- but it's enough to wake us up.
>> As a second example, consider
>> 	lemma "set_mset (mset_set A) = A"
>> This doesn't hold because A might be infinite, and converting it to a (finite) multiset will not preserve its elements. This is literally Sledgehammer's output:
>> 	e: Candidate missing assumption:
>> 	finite A
>> Having been bitten by this very example before, I am very excited that it is detected by Sledgehammer.
>> In conclusion, I would be grateful for your feedback concerning the new features and their user's interface. I hope they are more useful that confusing, but experience will tell. They were both easy additions, and I wouldn't mind disabling them by default if they turn out not to work well in practice.
>> Best,
>> Jasmin
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list