[isabelle-dev] Two new experimental features in Sledgehammer

[Jasmin Blanchette]

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