[isabelle-dev] Two new experimental features in Sledgehammer

[Tobias Nipkow]

Jasmin,

I am totally excited by the emergence of abduction in Isabelle. I had always 
hoped for something like it but had no idea how to rank the probably huge set of 
formulas that the ATPs find that would imply the goal. I assume you have some 
such ranking? Does the (equally huge) literature on abduction help?

Tobias

PS I already saw one "missing assumption" notification but in that case it did 
not help.

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4638 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230308/c8879a75/attachment.bin>