On 04/05/2013 10:51 AM, Martin Baker wrote: > It seems a sight irony that Axiom(the program) does not do much about > axioms.
Of course, AXIOM can deal with axioms, but the SPAD language does not include any way to specify axiom (not even Aldor can do this). >> Looks like you aim at a general term rewriting system. > Yes, but again I recognise that there are no resources, so I was > wondering if it would be possible to start with a very simple domain For a term rewriting system you basically have to start with the implementation of a term algebra. The signature would basically tell, what symbols are allowed. Since LISP is so fitting for a representation of such a term algebra, it is no surprise that quite a lot of computer algebra systems were written in LISP. Then you can add equations (axioms) and a mechanism to reduce a given term modulo such equations. But there is no general algorithm to transform a given term modulo such equation into a canonical form. A "canonical form" does not even exist for every given term rewriting system. The non-existence of the "eierlegende Wollmilchsau" (http://de.wikipedia.org/wiki/Eierlegende_Wollmilchsau http://en.wiktionary.org/wiki/eierlegende_Wollmilchsau) is the reason why people work on specialized solvers and use special representations of the respective term algebra to make things fast. Ralf _______________________________________________ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail