Hacker News new | past | comments | ask | show | jobs | submit login
Vampire: First-Order Theorem Proving [pdf] (chalmers.se)
68 points by tosh 5 days ago | hide | past | web | favorite | 19 comments





"This license does not allow this Software to be used in a commercial context. Users wishing to use the Software in a commercial context should contact the copyright holder for an alternative licence.

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++.


That's true. However, it might still be worthwhile given it appears to dominate competitions in many categories:

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 Licencee may not distribute the Software.

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


Just to give you a flavor of the way the main Vampire author does things: Until one or two years ago, not even a binary was freely available on the vampire website, and one had to contact them by email to ask for one; source code was definitely not distributed in any form.

You are mixing things up a bit, the alternatives you want are z3, cvc4, spass and e. Coq and TLA+ are proof assistents / formal specification languages, not smt solvers/theorem provers.

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.


Oh. Noted, thanks.

Can you explain the last sentence? Are you saying it’s bad software, so it’s not worth paying for? Or is the commercial license generally frowned upon for an open source project?

According to OSI [1], it is not open source if it cannot be used freely in commercial context.

[1]: https://opensource.org/faq#commercial


Thanks for saving me time!

This looks very interesting, some of the application areas sound really useful.

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


There's a tremendous amount of work that's been done on trustworthy theorem provers (see LCF, HOL, HOL Light, Milawa, ...), verified SAT solving and SMT solving, proof-producing first-order solvers, etc. All of this is cool and interesting.

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.


Some on the parts of some verified compilers are not "really" verified, in that there is no proof they always work. Rather, what is proved is that IF the compiler successfully compiles the program, THEN the result is correct. This can be easier, because it only requires that the compiler be able to provide a checkable certificate that its output is correct.

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.)


What Vampire and similar “automated theorem provers” are doing is searching for a proof of some logical statement (that you specify). That proof search is a really tough problem, so there’s a ton of research that goes into finding ways of speeding up the search e.g. through novel data structures. Proof verification —- the process of verifying the correctness of some claimed proof —- is much faster.

If the prover provides a written proof, then verifying that the proof (of the particular theorem) is correct is a much easier problem.

Do you mean "is it tested?" if so, I can see some results in table 1. Or do you mean "too big, therefore prone to UB, therefore not usable"?

Before <safe_language_of_the_day> came out people managed to shoot rockets to the moon...

UB exploitation is not about <safe_language_of_the_day>, C compilers used to be a lot saner than they are now. We shot people to the moon long, long before that change happened.

See https://news.ycombinator.com/item?id=19659555


I'm not sure why it was name Vampire; however, I wonder if it's inspired by Charle Stross's "The Laundry" books. In that universe, you become a Vampire by proving a certain Theorem. This causes your brain to attract the attention of interdimensional parasites.

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 :)


> VAMPIRE has a special mode for working with very large knowledge bases and can answer queries to them.

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?




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: