Vampire: First-Order Theorem Proving [pdf]
cse.chalmers.se
cse.chalmers.se
It is further prohibited to use this Software or a substantial portion of it in a competition or a similar competetive event"
No thanks, you can keep your 150k lines of C++.
https://web.archive.org/web/20190318010151/http://tptp.cs.mi...
As in, many people might be willing to get a license to get results some other prover weren't getting. It doesn't take a lot of complexity to choke one or explode its resource use.
> The Licensee may not modify, disassemble, translate, reverse engineer, or decompile the Software.
Clearly proprietary software. I didn't expect that from something advertised in an academic looking PDF. Back to Coq or TLA+, I guess.
And actually in my experience with using the sledgehammer tool in Isabelle, Vampire does not fare very well when it comes to real world problems.
One thing struck me:
"It is written in C++ and comprises about 152,000 SLOC."
OK, so how do I trust the results of this theorem prover? I can't find it right now, but I remember a talk by someone from Google who is/was also on the C++ standards committee saying that they have probably the best C++ programmers in the world, and nobody there can write code that is actually correct according to the standard, IIRC particularly but not limited to UB.
While I am generally fine with testing for most applications, something that says it provides proofs probably needs to be held to a higher standard. Or we call it a "theorem demonstrator"?
But from an industry perspective, there's plenty to like about plain old unverified C/C++ solvers and verification tools. They might crash sometimes, and they might occasionally have a soundness problem. But the odds that (1) your prover has a bug and (2) you will accidentally exploit that bug to "prove" something that isn't true are low.
To argue by analogy: plenty of people use unverified compilers, and of course these do have bugs. Even so, when your program isn't doing what you expect, it's still almost always a bug with your own code.
Consider a register allocator that uses graph coloring. In this case, the compiler just needs to check that the coloring that is produced is really a coloring: that it uses k colors, and that no two adjacent nodes in the associated graph are assigned the same color. This checking routine must be proved correct, but that's an easier task.
For a theorem prover to be verified in the same way, it just needs to produce an explicit proof, and then have a proof checker that is proved correct. The theorem prover itself, the part that produces the proof, doesn't have to be shown to always work (and indeed it won't, since it will very often time out.)
Addendum: It seems unlikely unless the name change is recent. The original version of VAMPIRE was in the early nineties. So unless Stross was inspired the other way :)
Does this mean it can somewhat replace Prolog? I forget why Prolog doesn't use full logic, but, does Vampire find a way to get around the need for Prolog's more limited, Horn clauses? Anyone know?