Re: [Axiom-developer] Re: [Gcl-devel] Axiom and Maxima

Hi Camm,

Camm Maguire <camm@enhanced.com> writes:

> Tim:
>> I already have plans "in place" (see the
>> savannah website) to merge ACL2 in a similar way. 
>> 
>
> I was looking for this on the site, but could not see anything
> pertinent.  What am I missing?

I think Tim is refering to the following:

In http://www.nongnu.org/axiom/

 BOYER-MOORE THEOREM PROVER INTEGRATION
  Motivation: Computational logic is a branch of computer mathematics
              that is not currently available in Axiom. The Boyer-Moore
              theorem prover, written in common lisp, provides a good
              general purpose platform to study the interaction of the
              theorem proving systems with Axiom
-  Contact Boyer & Moore
-  Contact Chandy & Misra
-  Download ACL2
   Build ACL2
   Invoke ACL2 from Axiom
   Integrate ACL2 into Axiom
     Use Dijkstra's methods against SetCategory
   Draft research paper


Yours,
d.
-- 
 david.mentre@wanadoo.fr