News for hackers. Stuff that matters.
Re:Learn Shen by mjn on Thursday November 01, 2012 @11:02PM (#4731054)
For better or worse, it's not that uncommon for licenses to complicate it. To take one prominent example, Microsoft Research's Z3 is completely proprietary: source-code is available but you cannot make any derivative works of it (except in-house without distribution). The famous Q array-processing language is also completely proprietary. Less restrictively, it's common for things to be released under an "academic use only" or "noncommercial use only" license.
Re:Learn Shen by kd0amg on Friday November 02, 2012 @10:56AM (#4732894)
And the papers I've read about array languages don't base their languages on Q. I haven't done much reading on theorem provers, but I suspect I'll see a lot more papers about things derived from ACL2 or Coq than from Z3.