This is a question which may have been asked before. I'm wondering if
anyone has looked into giving Maxima an inductive capability. To illustrate
with an example, if we issue to Maxima the four lines
q(n,z,t):=sum(A[j](t)*z^j,j,-n,n);
lhs(n):=diff(q(n,z,t),t);
rhs(n):=z*(1+K(t)*z)/(1-K(t)*z)*diff(q(n,z,t),z)+4*K(t)*z/(1-K(t)*z)^2*q(n,z
,t);
zero(n):=lhs(n)-rhs(n);
we can have Maxima compute
taylor(zero(n),z,0,n);
for various values of n, e.g. n=2,3,4 (but Maxima doesn't know what to do if
n is symbolic). In doing so we see an obvious inductive formula for z^(-n)
in zero(n), 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:zSzzSzwww.cs.utexas.e
duzSzuserszSzmoorezSzpublicationszSzbm75.pdf/boyer75proving.pdf) 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