--- Martin Rubey <[EMAIL PROTECTED]> wrote: > I'd just like to add that Renaud Rioboo is working on Focal, which > seems to be exactly what Cliff Yapp is looking for. However, it is > (and will stay) disconnected from Axiom.
Neat! > As far as I know it is based on Coq and Ocaml. See > > http://focal.inria.fr/site/manual.html I'll add that to my reading list. > I have no idea in what sense a theorem prover would be useful in a > CAS-context. Maybe Bruno Buchberger has some answers: > > http://www.risc.uni-linz.ac.at/research/theorema/description/ I've seen a couple efforts along those lines scattered around, but I haven't taken the time to study them in depth. Guess I should do that before anything else. Cheers, and thanks! CY __________________________________ Yahoo! Music Unlimited Access over 1 million songs. Try it free. http://music.yahoo.com/unlimited/ _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
