[Matryoshka-devel] Evil axioms
j.c.blanchette at vu.nl
Thu Apr 20 15:53:57 CEST 2017
Thanks for your input! This is very useful. I'll just answer all emails in one go, focusing on those things where I have more to say than "Yes, thanks for the links" or "Good idea" or "OK". I've printed a few papers already.
> Larry had some manual blacklisting in SH long ago.
Indeed, we still have some of it, but it's mostly historical. His blacklisting used to be necessary because of the unsound encoding.
> Probably very empirical at first. A project for a bachelor student?
Indeed. The empirical flavor doesn't exactly excite me about doing it, but a well-done empirical study can be very illuminating once it's done. There's no hurry, but we can keep this in the back of our minds for veriT. Even though there's a priori no HO in it, it's very relevant to the "hammer"-style of proving and hence to Matryoshka's goals, and also surely to Josef's AI4REASON and Cezary's SMART projects.
> Notice that most of what superposition theorem provers do is about avoiding evilness.
That's one way to see it. I guess they're trying to promote goodness and avoid evilness. Honestly, I'm not sure I share this view (yet) -- e.g. some people might say that they try to replace inferences and proof search by rewriting and computation, and this would be also a possible characterization of efforts to e.g. support rich type systems, theories, deduction modulo, etc. Also, my definition of evilness is quite restricted: It talks about a single evil axiom (or clause), not a set of axioms that together are evil (e.g. Haniel's matching loops but distributed over several formulas).
> One more related thing is automatically figuring out the basic logical
> facts and removing them (from the training data). They can be derived
> by the ATP automatically, and they do slow down the proof (evilness).
> We do this in HH and I think there was once a similar thing in SH?
IIRC we assume in Sledgehammer (or perhaps just in MaSh) that any formula that only contains logical symbols (connectives and quantifiers) is a tautology. We probably have an exception for extensionality (which talks, once translated, about an "app" operation). If you happen to have proved "False" as a lemma: Too bad, the ATPs won't see it.
In this case, I would guess the evilness is close to minimal, but since these formulas probably never help, they are a bit evil indeed.
More information about the matryoshka-devel