Patrick,
On Mon, Oct 26, 2009 at 1:30 AM, Patrick M. Rutkowski <rutski89 at gmail.com>wrote:
> ...I came across the following limit the other day in Spivak's chapter on
> logarithms and exponential functions:
>
> limit((b**h - 1)/h, h, 0) = log(b)
>
> ...I...eventually pieced together the proof:
>
...
> "Now, I can do it as a human, but how the heck would a computer
> analysis system figure that out!?"
>
Well, first thing to understand is the general notion of manipulating
algebraic expressions as tree structures.
Next thing is to work through some simple cases like symbolic
differentiation.
Much harder in general -- but easy in simple cases like 1*x => x, 0*x => 0,
etc. -- is simplification as a tree-to-tree transformation.
Finally, there are many mathematical techniques which are relatively easy to
program on algebraic expressions. In this case, L'Hopital's rule (or,
more-or-less equivalently, Taylor expansion) solves the problem.
Hope this helps you start on understanding all this.
-s