Non-commutative elimination in Ore algebras proves multivariate identities (Q1264426)

Many special functions are solutions of holonomic systems. \textit{D. Zeilberger} [ J. Comput. Appl. Math. 32, No. 3, 312-368 (1990; Zbl 0738.33001)] showed that many special function identities can be proved in a finite number of steps by invoking J. Bernstein's theory of holonomic systems. In this paper the authors generalize the notions of \(P\)-finite functions and sequences used by Zeilberger and develop a theory of \(\partial\)-finite functions and sequences. This theory makes it possible to use on a general level skew polynomial algebras as the algebraic setting and non-commutative Gröbner bases as a tool to develop effective algorithms. The paper provides a very general framework for computing sums and integrals and for the proof and the discovery of multivariate identities. The authors illustrate the theory by well-chosen examples making use of an interesting Maple package (written by the first author).