Holonomic Systems and Automatic Proofs of Identities, Frédéric Chyzak (1994). Research Report no. 2371, INRIA. 61 pages.

This report presents three computer algebra packages in the Maple language for the symbolic manipulation of linear systems of differential and recurrence equations. They are especially designed to deal with so-called holonomic systems. We also give a theoretical justification to our implementation. The set of holonomic functions and sequences is a large class of objects. It forms an algebra and is closed under algebraic substitution and diagonal. An implementation of these properties makes it possible to perform computer assisted proofs of holonomic identities in a simple way, since any holonomic system has a normal form obtained by an extension of the Gröbner basis algorithm. For instance, combinatorial problems often lead to holonomic systems and to identities involving binomial coefficients. Many identities involving special functions are also captured by the theory of holonomy. Examples are given to show how some interesting identities are proved by our system.