Re: [Axiom-developer] Calculemus

[root]

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

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