3 ms·
> The Licencee may not distribute the Software. > The Licensee may not modify, disassemble, translate, reverse engineer, or decompile the Software. Clearly pr
by loup-vaillant 8y ago
> 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.
- grumdan 8y agoJust 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.
- poizan42 8y agoYou 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.
- loup-vaillant 8y agoOh. Noted, thanks.