Hacker News Reader

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

View on HN

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.

Reply on news.ycombinator.com