[Top][All Lists]

[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.


> As far as I know it is based on Coq and Ocaml. See

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:

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!


Yahoo! Music Unlimited 
Access over 1 million songs. Try it free.

reply via email to

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