axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Ocaml, Coq, and ACL2


From: C Y
Subject: Re: [Axiom-developer] Ocaml, Coq, and ACL2
Date: Thu, 20 Oct 2005 09:26:40 -0700 (PDT)

--- Martin Rubey <address@hidden> 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/




reply via email to

[Prev in Thread] Current Thread [Next in Thread]