[isabelle-dev] Vampire

[Blanchette, J.C.]

Makarius wrote:

> I don't remember the reason for its "tristate logic", with "unknown" as default.

The thinking is as follows. In an "unknown" state, "vampire" gets added to the list of provers by Sledgehammer, and users get a warning. In a "no" state, it doesn't. Thus, "unknown" serves a documentational purpose. If the default were "no" instead, many noncommercial users would likely fail to enable Vampire.

I'm not married to the above scheme, but the years of experience with it and Z3 (until Z3 was open-sourced) suggest that it works well.

Jasmin