[Axiom-developer] Questions of Simplification

[C Y]

I know in general simplification and comparisons of equality are hard
problems, but I'm afraid I'm not familiar with the formal mathematical
results that demonstrate this.  Practically the problem is obviously
difficult, and I have heard on many occasions that equality of two
expressions is undecidable in general, but I'm curious if these
questions have some "formal" mathematical analysis behind them.

Can someone recommend some resources on automatic simplification,
discussions of what "simplification" means, and issues related to
undecidable equality cases?  My motivation is this - for some cases
equality is undecidable, for some it is undecidable in reasonable time,
for others is is solvable (4^a=2^(2a) being the example in issue 191). 
If equality cannot be decided in general, perhaps there is a way to
categorize expressions so that it is "decidable if the question is
decidable", so to speak.  I suppose the question is not terribly
interesting from a theoretical mathematical standpoint, but if it
should happen to be possible it would be very useful in CAS work.

Maybe there isn't any way in general to make this systematic, but if
not I would like to understand why that's the case.  Any pointers
appreciated.

Cheers and thanks,
CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com