[Axiom-developer] RE: Copyright?

[Bill Page]

Ralf,

Earlier in an email you asked:

> ...
> Depending on what publishing really means, I think that 
> copyright actually forbid it to put the file onto an axiom
> server.
>
> Have you contacted Doye?
> ...

On July 16, 2006 3:10 PM I replied:
> ... 
> I did not try to contact Doye before uploading his thesis to
> axiom-developer. Given the content of the thesis and the intent
> of our website I did not think there was any serious risk of a
> copyright issue. Of course if he (or anyone else) asked me to,
> I would certainly be prepared to remove it from the site.
>

Actually, my brain is a seive and if it weren't for this archive
I would probably not remember my own name! In fact I did ask Nic
if it was ok to put a copy of his thesis online. See:

http://lists.nongnu.org/archive/html/axiom-developer/2005-09/msg00134.html
 
This reminds me that someday real-soon-now I still hope to spend
some time looking at OBJ:

http://cseclassic.ucsd.edu/~goguen/sys/obj.html
http://www.cse.ucsd.edu/users/goguen

and how it might related to Axiom. More specifically, I was thinking
of installing some version of OBJ on the axiom server and making it
accessible via the wiki. This might be one (more) way of starting to
mix automated theorem proving with computer algebra. Do you think
anyone else would be interested in this?

Apparently there is/was? a version of OBJ3 that uses/used? GCL:

"There is a new release (from June 2000) of OBJ3, version 2.06; it is
a cleaned-up version OBJ3 version 2.04 (from 1992), engineered by Joseph
Kiniry and Sula Ma, and built and supported by Joseph Kiniry; it runs
under GCL 2.2.2, and has modern open source documentation."

but I have not been able to locate the source code yet since the links
seem to be out of date.

Perhaps I should consider using cafeOBJ?

http://www.ldl.jaist.ac.jp/cafeobj

which appears to be newer and apparently also can be compiled using
GCL.

Or for the adventuresome, there is BOBJ - a Java-based version of
OBJ. I think BOBJ is very interesting because

"BOBJ is used in the Tatami project, which is developing the Kumo
proof assistant and proof website generator."

http://www.cs.ucsd.edu/groups/tatami
http://www.cse.ucsd.edu/groups/tatami/kumo
http://www.cse.ucsd.edu/groups/tatami/bobj

Regards,
Bill Page.