Computer Proofs for Polynomial Identities in Arbitrary Many Variables

摘要

We present an algorithm for proving certain families of polynomial identities in which the number of variables appears as a parameter. Typically, indefinite sums and products (possibly nested) are used for defining such polynomial identities, 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 Mathe-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.