Re: [Axiom-mail] A question about Axiom capabilities

[Gabriel Dos Reis]

On Fri, Apr 5, 2013 at 3:51 AM, Martin Baker <address@hidden> wrote:

> Given that there is no resources (or desire, as far as I can see) to change
> the structure of Axiom then I was wondering, just for specific domains where
> we want a specific equation solver, could we encode the axioms in a set of
> rules in a domain or package? I guess I'm looking for a compromise between
> building this into the Lisp code and writing a seperate equation solver in
> every domain.

Your probably know that OpenAxiom started putting the axioms in AXIOM.
See for example:

  
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet

In fact, a couple of years ago, a student of mine did experiments on
exploiting these axioms to help code generation and automatic
parallelization.  The results were very encouraging (see the
yli-sandbox for example.)

OpenAxiom is very much committed to get the axioms integrated to the
entire type checking and elaboration process.

-- Gaby