Re: [Axiom-developer] Calculemus

[Camm Maguire]

Greetings!

root <address@hidden> writes:

> Dylan,
> 
> Yes, I did see that actually.
> 
> One of the proposed pieces of work with Axiom is to join it with
> ACL2. There have been email discussions with that group (Kaufmann,
> Boyer, and Moore) about it in the past.
> 
> ACL2 and Axiom are both written in common lisp and both run on GCL
> so it would be straightforward to load them into the same image.
> Cover functions could be created in axiom (since axiom code can
> directly call lisp code).
> 

This could be very interesting.  As you've said, luckily, the
technical aspects of the combination should be trivial, as both
projects have a thorough workout atop the same GCL image, at least in
the Debian autobuilding infrastructure.  The key of course lies in the
actual logic of the connections themselves.  I have a reasonably good
relationship with the ACL2 authors if/when we would like to solicit
their help/advice.

Take care,

> One research issue would be to take the merger as an assumption
> and see how axiom's categorical view supports or conflicts with
> ACL2's world view.
> 
> Another research issue would be to look at self-application of
> ACL2 to Axiom by focusing on something like Axiom's list or
> sorting implementations, showing proofs of code. Could proven
> axiom functions be used in further ACL2 proofs?
> 
> A third idea is to look at decorating the categories and domains
> with theorems (e.g. the ring properties and related theorems) and
> then propagating this information onto the domain functions and
> their arguments. Can we propagate properties to reach "logical
> conclusions" without actually computing a result?
> 
> A fourth idea is to apply ACL2 to computing "proviso" information
> (e.g. 1/x provided x!=0) where the provisos are carried at each
> step of a computation.
> 
> In general, I think that the merging of an algebra system, especially
> one based around theory as Axiom is, and a logic system will be a
> fruitful area of research work.
> 
> Tim
> 
> 
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/axiom-developer
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah