# DAAD: Differenzengleichungen und Computeralgebra

### Project Description

P.Paule.

Doktoratstipentium von Manuel Kauers

Budget: 14.425,66 Eur.

### Project Lead

### Project Duration

01/01/2004 - 31/12/2004## Publications

### 2006

### A Computer Proof of Turan's Inequality

#### Stefan Gerhold, Manuel Kauers

Journal of Inequalities in Pure and Applied Mathematics 7(2), pp. 1-4. May 2006. Article 42. [ps]@

author = {Stefan Gerhold and Manuel Kauers},

title = {{A Computer Proof of Turan's Inequality}},

language = {english},

abstract = {We show how Turan's inequality $P_n(x)^2-P_{n-1}(x)P_{n+1}(x)\geq0$ for Legendre Polynomials and related inequalities can be proven by means of a computer procedure. The use of this procedure simplifies the daily work with inequalities. For instance, we have found the stronger inequality $|x|P_n(x)^2-P_{n-1}(x)P_{n+1}(x)\geq0$ ($-1\leq x\leq 1$) effortlessly with the aid of our method},

journal = {Journal of Inequalities in Pure and Applied Mathematics},

volume = {7},

number = {2},

pages = {1--4},

isbn_issn = {?},

year = {2006},

month = {May},

note = {Article 42},

refereed = {yes},

length = {4}

}

**article**{RISC2876,author = {Stefan Gerhold and Manuel Kauers},

title = {{A Computer Proof of Turan's Inequality}},

language = {english},

abstract = {We show how Turan's inequality $P_n(x)^2-P_{n-1}(x)P_{n+1}(x)\geq0$ for Legendre Polynomials and related inequalities can be proven by means of a computer procedure. The use of this procedure simplifies the daily work with inequalities. For instance, we have found the stronger inequality $|x|P_n(x)^2-P_{n-1}(x)P_{n+1}(x)\geq0$ ($-1\leq x\leq 1$) effortlessly with the aid of our method},

journal = {Journal of Inequalities in Pure and Applied Mathematics},

volume = {7},

number = {2},

pages = {1--4},

isbn_issn = {?},

year = {2006},

month = {May},

note = {Article 42},

refereed = {yes},

length = {4}

}

### Indefinite summation with unspecified summands

#### M. Kauers, C. Schneider

Discrete Math. 306(17), pp. 2073-2083. 2006. ISSN 0012-365X. Preliminary version online. [pdf]@

author = {M. Kauers and C. Schneider},

title = {{Indefinite summation with unspecified summands}},

language = {english},

journal = {Discrete Math.},

volume = {306},

number = {17},

pages = {2073--2083},

isbn_issn = {ISSN 0012-365X},

year = {2006},

note = {Preliminary version online},

refereed = {yes},

length = {11}

}

**article**{RISC2873,author = {M. Kauers and C. Schneider},

title = {{Indefinite summation with unspecified summands}},

language = {english},

journal = {Discrete Math.},

volume = {306},

number = {17},

pages = {2073--2083},

isbn_issn = {ISSN 0012-365X},

year = {2006},

note = {Preliminary version online},

refereed = {yes},

length = {11}

}

### Application of unspecified sequences in symbolic summation

#### M. Kauers, C. Schneider

In: Proceedings of ISSAC'06, Jean-Guillaume Dumas (ed.), Proceedings of ISSAC'06, pp. 177-183. 2006. ACM Press, [pdf] [ps]@

author = {M. Kauers and C. Schneider},

title = {{Application of unspecified sequences in symbolic summation}},

booktitle = {{Proceedings of ISSAC'06}},

language = {english},

abstract = { We consider symbolic sums which contain subexpressions that represent unspecified sequences. Existing symbolic summation technology is extended to sums of this kind. We show how this can be applied in the systematic search for general summation identities. Both, results about the non-existence of identities of a certain form, and examples of general families of identities which we have discovered automatically are included in the paper.},

pages = {177--183},

publisher = {ACM Press},

isbn_issn = {?},

year = {2006},

editor = {Jean-Guillaume Dumas},

refereed = {yes},

length = {7},

conferencename = {ISSAC'06}

}

**inproceedings**{RISC2895,author = {M. Kauers and C. Schneider},

title = {{Application of unspecified sequences in symbolic summation}},

booktitle = {{Proceedings of ISSAC'06}},

language = {english},

abstract = { We consider symbolic sums which contain subexpressions that represent unspecified sequences. Existing symbolic summation technology is extended to sums of this kind. We show how this can be applied in the systematic search for general summation identities. Both, results about the non-existence of identities of a certain form, and examples of general families of identities which we have discovered automatically are included in the paper.},

pages = {177--183},

publisher = {ACM Press},

isbn_issn = {?},

year = {2006},

editor = {Jean-Guillaume Dumas},

refereed = {yes},

length = {7},

conferencename = {ISSAC'06}

}

### 2005

### A Procedure for Proving Special Function Inequalities Involving a Discrete Parameter

#### Stefan Gerhold, Manuel Kauers

In: Proceedings of ISSAC '05, Manuel Kauers (ed.), pp. 156-162. 2005. ACM Press, ISBN 1-59593-095-705/0007. [ps]@

author = {Stefan Gerhold and Manuel Kauers},

title = {{A Procedure for Proving Special Function Inequalities Involving a Discrete Parameter}},

booktitle = {{Proceedings of ISSAC '05}},

language = {english},

abstract = {We define a class of special function inequalities that contains many classical examples, such as the Cauchy-Schwarz inequality, and introduce a proving procedure based on induction and Cylindrical Algebraic Decomposition. We present an array of non/trivial examples that can be done by our method and have not been proven automatically before. Some difficult well-known inequalities such as the Askey-Gasper inequality and Vietoris's inequality lie in our class as well, but we do not know if our proving procedure terminates on them.},

pages = {156--162},

publisher = {ACM Press},

isbn_issn = {ISBN 1-59593-095-705/0007},

year = {2005},

editor = {Manuel Kauers},

refereed = {yes},

length = {7}

}

**inproceedings**{RISC2466,author = {Stefan Gerhold and Manuel Kauers},

title = {{A Procedure for Proving Special Function Inequalities Involving a Discrete Parameter}},

booktitle = {{Proceedings of ISSAC '05}},

language = {english},

abstract = {We define a class of special function inequalities that contains many classical examples, such as the Cauchy-Schwarz inequality, and introduce a proving procedure based on induction and Cylindrical Algebraic Decomposition. We present an array of non/trivial examples that can be done by our method and have not been proven automatically before. Some difficult well-known inequalities such as the Askey-Gasper inequality and Vietoris's inequality lie in our class as well, but we do not know if our proving procedure terminates on them.},

pages = {156--162},

publisher = {ACM Press},

isbn_issn = {ISBN 1-59593-095-705/0007},

year = {2005},

editor = {Manuel Kauers},

refereed = {yes},

length = {7}

}

### Algorithms for Nonlinear Higher Order Difference Equations

#### Manuel Kauers

RISC-Linz. PhD Thesis. October 2005. [ps] [ps]@

author = {Manuel Kauers},

title = {{Algorithms for Nonlinear Higher Order Difference Equations}},

language = {english},

abstract = {In this thesis, new algorithmic methods for the treatment of special sequences are presented. The sequences that we consider are described by systems of difference equations (recurrences). These systems may be coupled, non-linear, and/or higher order. The class of sequences defined in this way (admissible sequences) contains a lot of sequences which are of interest in various mathematical applications. While some of these sequences can be handled also with known Algorithms, for many others no adequate methods were available up to now.In the center of our interest, there are algorithms for automatically proving known identities of admissible sequences, and for automatically discovering new ones. By "finding new identities", we mean in particular solving of difference equations in closed form, finding closed forms for symbolic sums, and finding algebraic dependencies of given sequences. In addition, we present a procedure by which some inequalities of admissible sequences can be proven automatically. For their algorithmic treatment, admissible sequences are represented as elements of certain special difference rings.In these difference rings, computations are then carried out, whose results can be interpreted as statements about the original admissible sequences. Known techniques for commutative multivariate polynomial rings, especially the theory of Gr\"obner bases, are applied to this end.Part of the present thesis is an implementation of the presented algorithms in form of a software package for the computer algebra system Mathematica. With the aid of our software, we succeeded in proving a lot of identities and inequalities from the literature automatically for the first time. Additionally, with the same software, we have found some identities which were probably unknown up to now.},

year = {2005},

month = {October},

translation = {0},

school = {RISC-Linz},

length = {155}

}

**phdthesis**{RISC2568,author = {Manuel Kauers},

title = {{Algorithms for Nonlinear Higher Order Difference Equations}},

language = {english},

abstract = {In this thesis, new algorithmic methods for the treatment of special sequences are presented. The sequences that we consider are described by systems of difference equations (recurrences). These systems may be coupled, non-linear, and/or higher order. The class of sequences defined in this way (admissible sequences) contains a lot of sequences which are of interest in various mathematical applications. While some of these sequences can be handled also with known Algorithms, for many others no adequate methods were available up to now.In the center of our interest, there are algorithms for automatically proving known identities of admissible sequences, and for automatically discovering new ones. By "finding new identities", we mean in particular solving of difference equations in closed form, finding closed forms for symbolic sums, and finding algebraic dependencies of given sequences. In addition, we present a procedure by which some inequalities of admissible sequences can be proven automatically. For their algorithmic treatment, admissible sequences are represented as elements of certain special difference rings.In these difference rings, computations are then carried out, whose results can be interpreted as statements about the original admissible sequences. Known techniques for commutative multivariate polynomial rings, especially the theory of Gr\"obner bases, are applied to this end.Part of the present thesis is an implementation of the presented algorithms in form of a software package for the computer algebra system Mathematica. With the aid of our software, we succeeded in proving a lot of identities and inequalities from the literature automatically for the first time. Additionally, with the same software, we have found some identities which were probably unknown up to now.},

year = {2005},

month = {October},

translation = {0},

school = {RISC-Linz},

length = {155}

}

### 2004

### Computer Proofs for Polynomial Identities in Arbitrary Many Variables

#### Manuel Kauers

In: Proceedings of ISSAC 2004, Jaime Gutierrez (ed.), pp. 199-204. 2004. ACM Press, ISBN 1-58113-827-X. [ps]@

author = {Manuel Kauers},

title = {{Computer Proofs for Polynomial Identities in Arbitrary Many Variables}},

booktitle = {{Proceedings of ISSAC 2004}},

language = {english},

pages = {199--204},

publisher = {ACM Press},

isbn_issn = {ISBN 1-58113-827-X},

year = {2004},

editor = {Jaime Gutierrez},

refereed = {yes},

length = {6}

}

**inproceedings**{RISC212,author = {Manuel Kauers},

title = {{Computer Proofs for Polynomial Identities in Arbitrary Many Variables}},

booktitle = {{Proceedings of ISSAC 2004}},

language = {english},

pages = {199--204},

publisher = {ACM Press},

isbn_issn = {ISBN 1-58113-827-X},

year = {2004},

editor = {Jaime Gutierrez},

refereed = {yes},

length = {6}

}