Computer proofs for polynomial identities in arbitrary many variables

ABSTRACT

We present an algorithm for proving certain families of nomial identities in which the number of variables appears as a parameter.Typically,indefinite sums and products (possibly nested)are used for defining such polynomial ties, but in principle the definition of the problem may be given in terms of arbitrary polynomial recurrences (possibly nonlinear). An implementation of our algorithm in Mat e-matica was able to verify identities appearing in textbooks, which, to our knowledge,were previously not accessible by any symbolic method. A collection of examples is included in the paper.

REFERENCES

• 1: G.E.Andrews,R.Askey,and R.Roy. Special Functions, volume 71 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1999.
• 2: Frédéric Chyzak, An extension of Zeilberger's fast algorithm to general holonomic functions, Discrete Mathematics, v.217 n.1-3, p.115-134, April 2000 [doi>10.1016/S0012-365X(99)00259-9]
• 3: Frédéric Chyzak , Bruno Salvy, Non-commmutative elimination in ore algebras proves multivariate identities, Journal of Symbolic Computation, v.26 n.2, p.187-227, Aug. 1998 [doi>10.1006/jsco.1998.0207]
• 4: R. M. Cohn. Difference Algebra. Interscience Publishers, John Wiley & Sons,1965.
• 5: Ronald L. Graham , Donald E. Knuth , Oren Patashnik, Concrete Math, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 6: M. Kauers. An algorit m for deciding zero equivalence of nested polynomially recurrent sequences. Technical Report 2003-48,SFB F013,Johannes Kepler Universität, 2003.(submitted).
• 7: I. G. MacDonald. Symmetric Functions and Orthogonal Polynomials. American Mathematical Society, 1998.
• 8: O. Perron. Die Lehre von den Kettenbrüchen. Celsea Publishing Company, second edition, 1929.
• 9: M. Petkovsek, H. Wilf,and D. Zeilberger. A = B. AK Peters, Ltd.,1997.
• 10: C. Scheider. Symbolic Summation in Difference Fields . PhD thesis, RISC-Linz, Johannes Kepler Universit7auml;t Linz,2001.
• 11: R P Stanley, Enumerative combinatorics, Wadsworth Publ. Co., Belmont, CA, 1986
• 12: John R. Stembridge, A Maple package for symmetric functions, Journal of Symbolic Computation, v.20 n.5-6, p.755-768, Nov./Dec. 1995 [doi>10.1006/jsco.1995.1077]
• 13: D. Zeiberger, A fast algorithm for proving terminating hypergeometric identities, Discrete Mathematics, v.80 n.2, p.207-211, March 1990 [doi>10.1016/0012-365X(90)90120-7]
• 14: Doron Zeilberger, A holonomic systems approach to special functions identities, Journal of Computational and Applied Mathematics, v.32 n.3, p.321-368, Nov. 27, 1990 [doi>10.1016/0377-0427(90)90042-X]
• 15: D. Zeilberger. WZ Theory, Chapter II. In MSRI Workshop on Symbolic Computation in Geometry and Analysis, 1998. Transcript available at ttp://www.math.rutgers.edu/~zeilberg/.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms

General Terms:
Algorithms

Keywords:
computer proofs, polynomial identities