[isabelle-dev] Two new experimental features in Sledgehammer

[Jasmin Blanchette]

Hi Tobias,

> 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?

For the moment, this is only implemented with E. As you correctly write, saturation provers generate a huge set of clauses that, if we had their negation, we could finish the refutation. However, the vast majority of these clauses are not descendants of the negated conjecture. These are effectively lemmas, like hd [x, y] = x, and there's hardly any point in suggesting to the user to prove hd [x, y] ~= x.

Remain the clauses that are descendants of the negated conjecture. Among these, I leave out all clauses of length more than 1 -- these are likely too complicated, too ad hoc, to be interesting. This leaves the unit clauses that are descendants of the negated conjecture. There are often very few of these -- of the order of 10, sometimes even 0. Currently, I sort them roughly by size, preferring those that talk about the goal's variables. In the future, I will completely filter out those that don't talk about the clauses variables, since arbitrary assumptions about arbitrary things are unlikely to be unprovable (e.g., "0 = 1").

In short, the approach I'm trying out is very simple -- so simple that if I wrote a paper about it, it would have to be a 5-page paper. It's very ad hoc and not based on the vast literature. But maybe it would be an idea to look more seriously at what the literature has to offer. One weakness of my simple approach is that the superposition prover uses a term order to break symmetries in the proof search. Due to that, not all consequences are derived, and sometimes a nice-to-have clause like "~ finite A" (corresponding to the missing assumption "finite A") is simply not generated, even though it is a consequence.

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

Good to know.

Jasmin