> -----Original Message-----
> From: maxima-bounces at math.utexas.edu
> [mailto:maxima-bounces at math.utexas.edu] On Behalf Of George Leeman
<snip>....
> In doing so we see an obvious inductive
> formula for z^(-n)
> in zero(n),
As you undoubtedly realize, the evidence of n=2, n=3, n=4 is not sufficient
for "mathematical induction" which requires a proof that case n can be
proved by assuming case n-1 and some base case(s).
You can easily construct examples for which the "obvious" formula exhibited
by any finite set of cases is violated by the first case which is not
examined.
It is not unusual, however, for someone to use a computer algebra system to
construct a number of examples, construct a hypothesis, and then test the
hypothesis.
The important component here, at least so far, is the human.
1. choosing a set of examples that are paradigmatic of the situation,
including but not exclusively consisting of border cases.
2. coming up with a generalization or hypothesis.
3. testing the hypothesis either by returning to mathematical first
principles and proving it, or pragmatically testing the hypothesis on
additional cases to such an extent that the hypothesis appears to be
confirmed.
I did this myself in
''A Case History in Interactive Problem Solving,'' SIGSAM Bulletin, no. 28,
December 1973, 30-32.
Also, in Proc. of a Conference on Information Linkage Between Applied
Mathematics and Industry,
Academic Press, 1979. 299-305.
The tools like ACL(2) (and Lisp and Macsyma) have been around for quite a
few years. You can look at the list of successes for ACL2 (or alternatives
such as Otter) by some Googling. You can also look at the activity under MKM
(mathematics knowledge management). I suspect that solving problems such as
yours is not going to be totally automated in the near future. Your
suggestion about interactivity may change the prospects, and I encourage you
to pursue this, perhaps by adding programs to Maxima.
RJF
> and there are elegant closed form expressions for
> the other
> coefficients. The question is whether there is machinery in
> Maxima to show
> such formulas are valid, possibly interactively with the
> user's help. In a
> seminal paper Boyer and Moore
> (http://citeseer.ist.psu.edu/cache/papers/cs/1068/http:zSzzSzw
> ww.cs.utexas.e
> duzSzuserszSzmoorezSzpublicationszSzbm75.pdf/boyer75proving.pd
> f) observed
> that in Lisp evaluation and induction are complementary
> operations. There
> is a follow-on system, "A Computational Logic for applicative
> common lisp"
> (ACL2, http://www.cs.utexas.edu/users/moore/acl2/). The
> beauty of using
> Lisp as an implementation language is that perhaps some of
> these systems or
> the ideas behind them could be added to Maxima, or maybe it
> has already been
> done. Any thoughts?
> Thanks, George Leeman
> _______________________________________________
> Maxima mailing list
> Maxima at math.utexas.edu
> http://www.math.utexas.edu/mailman/listinfo/maxima
>