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. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
