Hagenberg Research N.N.∗ October 22, 2010 1 Computer-Assisted Discovery and Proving First we comment on computer-assisted guessing in the context of mathe- matical discovery. Then we turn to the activity of proving, more precisely, to proving methods where computer algebra algorithms are used. Here we restrict to this special type of computed-assisted proving; for general mathe- matical proving machines like the THEOREMA system developed at RISC. 1.1 I.Q. Tests, Rabbits, and the Golden Section Let us consider the following problem taken from an I.Q. test [10, Aufgabe 13, Denksport I fuer Superintelligente] from the sixties of the last century: Continue the sequence 1, 1, 2, 3, 5, 8, 13, 21. In the 21st century we let the computer do the problem. To this end we load the RISC package GeneratingFunctions written by C. Mallinger [19] in the computer algebra system Mathematica: In[1]:= GeneratingFunctions.m In the next step we input a little program that can be used to solve such I.Q. tests automatically: In[2]:= GuessNext2Values[Li ] := Module[{rec}, rec = GuessRE[Li,c[k],{1,2},{0,3}]; RE2L[rec[[1]],c[k],Length[Li]+1]] ∗ This is an exercise for the RISC course “Computer based working environments”. 1 Finally the problem is solved automatically with In[3]:= GuessNext2Values[{1, 1, 2, 3, 5, 8, 13, 21}] Out[3]= {1,1,2,3,5,8,13,21,34,55} To produce additional values is no problem: In[4]:= GuessNext2Values[{1, 1, 2, 3, 5, 8, 13, 21, 34, 55}] Out[4]= {1,1,2,3,5,8,13,21,34,55,89,144} Note. The same automatic guessing can be done in the Maple system; there B. Salvy and P. Zimmermann [24] developed the poineering pack- age gfun which has served as a model for the development of Mallinger’s GeneratingFunctions. What is the mathematical basis for such automatic guessing? The answer originates in a simple observation: Many of the sequences (xn )n≥0 arising in practical applications (and in I.Q. tests!) are produced from a very simple pattern; namely, linear recurrences of the form pd (n)xn+d + pd−1 (n)xn+d−1 + · · · + p0 (n)xn = 0, n ≥ 0, with coefficients pi (n) being polynomials in n. So packages like Mallinger’s GeneratingFunctions try to compute-via an ansatz using undetermined coefficients-a recurrence of exactly this type. For the I.Q. example above a recurrence is obtained by In[5]:= GuessRE[{1, 1, 2, 3, 5, 8, 13, 21},f[n]] Out[5]= {{-f[n]-f[1+n]+f[2+n]==0,f[0]==1,f[1]==1}, ogf} Since only finitely many values are given as input, the output recurrence fn+2 = fn+1 + fn (n ≥ 0) can be only a guess about a possible building principle of an infinite sequence. However, such kind of automated guessing is becoming more and more relevant to concrete applications. For instance, an application from mathematical chemistry can be found in [8] where a prediction for the total number of benzenoid hydrocarbons was made. Three years later this predication was confirmed [27]. Recently, quite sophisticated applications arose in connection with the enumeration of lattice paths and also with quantum field theory. In 1202 Leonard Fibonacci introduced the numbers fn . The fact that f0 = f1 = 1, and fn+2 = fn+1 + fn , n ≥ 0, 2 in Fibonacci’s book was given the following interpretation: If baby rabbits become adults after one month, and if each pair of adult rabbits produces one pair of baby rabbits every month, how many pairs of rabbits, starting with one pair, are present after n months? A non-recursive representation is the celebrated Euler-Binet formula √ n+1 √ n+1   1 1+ 5 1− 5 fn = √  − , n ≥ 0. 5 2 2 √ The number (1 + 5)/2 ≈ 1.611803, the golden ratio, is important in many parts of mathematics as well as in the art world. For instance, Phidias is said to have used it consciously in his sculpture. Mathematicians gradually began to discover more and more interesting things about Fibonacci numbers fn ; see e.g. [13]. For example, a typical sunflower has a large head that contains spirals of tightly packed florets, usually with f8 = 34 winding in one direction and f9 = 55 in another. Another observation is this: Define gn as a sum over binomial coefficients of the form n n−k gn := . k=0 k From the values g0 = 1, g1 = 1, g2 = 2, g3 = 3, g4 = 5, and g5 = 8 it is straight-forward to conjecture that the sequence (gn )n≥0 is nothing but the Fibonacci sequence (fn )n≥0 . In the next subsection we shall see that nowadays such statements can be proved automatically with the computer. 1.2 Pi, Inequalities, and Finite Elements We have seen that linear recurrences can be used as a basis for automated guessing. Concerning symbolic computation, this is only the beginning. Namely, following D. Zeilberger’s holonomic paradigm [29], the description of mathematical sequences in terms of linear recurrences, and of mathematical functions in terms of linear differential equations, is also of great importance to the design of computer algebra algorithms for automated proving. For example, consider the sequence (gn )n≥0 defined above. To prove the statement fn = gn , n ≥ 0, 3 in completely automatic fashion, we use the RISC package Zb [21], an imple- mentation of D. Zeilberger’s algorithm [28]: In[6]:= Zb.m In[7]:= Zb[Binomial[n-k,k],{k,0,Infinity},n,2] Out[7]= {SUM[n] + SUM[1 + n] − SUM[2 + n] == 0} The output tells us that gn = SUM[n] indeed satisfies the same recurrence as the Fibonacci numbers. A proof for the correctness of the output recurrence can be obtained automatically, too; just type the command: In[8]:= Prove[] For further details concerning the mathematical background of this kind of proofs, see e.g. Zeilberger’s articles [29] and [28] which were the booster charge for the development of a new subfield of symbolic computation; namely, the design of computer algebra algorithms for special functions and sequences. For respective RISC developments the interested reader is referred to the web page http://www.risc.uni-linz.ac.at/research/combinat For various applications researchers are using such algorithms in their daily research work-sometimes still in combination with tables. However, there are particular problem classes where symbolic (and numeric) algorithms are going to replace tables almost completely. Concerning special sequences the most relevant table is N. Sloane’s hand- book [25], [26]. Sloane’s home page provides an extended electronic version of it; also symbolic computation algorithms are used to retrieve information about sequences . Concerning special functions one of the most prominent tables is the ‘Handbook’ [1] from 1964. Soon it will be replaced by its strongly revised successor, the NIST Digital Library of Mathematical Functions (DLMF); see http://dlfm.nist.gov. The author of this section is serving as an associate editor of this new handbook (and author, together with F. Chyzak, of a new chapter on computer algebra) that will be freely available via the web. We expect the development of special provers will intensify quite a bit. By special provers we mean methods based on computer algebra algorithms specially tailored for certain families of mathematical objects. Special func- tion inequalities provide a classical domain that so far has been considered as 4 being hardly accessible by such methods. To conclude this section we briefly describe that currently this situation is about to change. Consider the famous Wallis product formula for π: 2 2 4 4 6 6 8 8 π =2· · · · · · · · · ··· . 1 3 3 5 5 7 7 9 This product is an immediate consequence (n → ∞) of the following inequal- ity (John Wallis, Arithmetica Infinitorum, 1656): 2n cn ≤ ≤ 1, n ≥ 0, 2n + 1 π where −2 24n+1 2n cn := . 2n + 1 n In analysis one meets such inequalities quite frequently. Another example, similar to that of Wallis, is 1 1 ≤ an ≤ , n ≥ 0, 4n 3n + 1 where 2 1 2n an := . 24n n We shall prove the right hand side, i.e. an ≤ 1/(3n + 1), (the left hand side goes analogously) to exemplify the new Gerhold-Kauers method [12] for proving special function/sequence inequalities. As proof strategy they use mathematical induction combined with G. Collins’ cylindrical algebraic decomposition (CAD). First observe that (2n + 1)2 1 (2n + 1)2 an+1 = an ≤ , (2n + 2)2 3n + 1 (2n + 2)2 where for the inequality the induction hypothesis is used. In order to show that this implies an+1 ≤ 1/(3n + 4), it is sufficient to establish that 1 (2n + 1)2 1 ≤ . 3n + 1 (2n + 2)2 3n + 4 But this step can be carried out automatically with any implementation of Collins’ CAD; for instance, in Mathematica: 5 2 In[9]:= Reduce[ 3n+1 (2n+1)2 ≤ 3n+4 , n] 1 (2n+2) 1 Out[9]= − 4 < n < −1 || −1 < n < − 3 || n ≥ 0 3 1 The Gerhold-Kauers method already found quite a number of non-trivial applications. They range from new refinements of Wallis’ inequality [20] like 32n2 + 32n + 7 cn 16(n + 1)(2n + 1) ≤ ≤ , n ≥ 0, 4(2n + 1)(4n + 3) π 32n2 + 56n + 25 to a proof of the long-standing log-concavity conjecture of V. Moll [17]. Fur- ther applications and details about the method are given in [16]. We want to conclude by referring to results that emerged from numerical- symbolic SFB collaboration in the context of finite element methods (FEM). In order to set up a new FEM setting, J. Sch¨berl (RWTH Aachen, formerly o JKU) needed to prove the following special function inequality: n (4j + 1)(2n − 2j + 1)P2j (0)P2j (x) ≥ 0 j=0 for −1 ≤ x ≤ 1, n ≥ 0, and with P2j (x) being the Legendre polynomials. Using the Gerhold-Kauers method together with RISC symbolic summation software, V. Pillwein [22] was able to settle this conjecture. Remarkably, there is still no human proof available! Last but not least, we mention a recent collaboration of J. Sch¨berl with o C. Koutschan (RISC), which led to a new tool for engineering applications in the context of electromagnetic wave simulation. Formulas derived by Koutschan’s symbolic package HolonomicFunctions resulted in a significant speed-up of numerical FEM algorithms e.g. for the construction of antennas or mobile phones. The method is planned to be registered as a patent. 2 Gr¨bner Bases Theory for Nonlinear Poly- o nomial Systems 2.1 The Relevance of Gr¨bner Bases Theory o To a great extent, Gr¨bner bases theory was the starting point of the Re- o search Institute for Symbolic Computation and, hence, the Softwarepark 6 Hagenberg. Gr¨bner bases theory was initiated in the PhD thesis [3, 4] and o turned out to be one of the first coherent results in the emerging area of what was later called “computer algebra”. Gr¨bner bases theory allows to handle o a big variety of fundamental problems connected to systems of multivariate polynomials, for example the problem of solving such systems (finding all common roots of such systems) or the problem of deciding whether two given multivariate polynomials are “equivalent” with respect to a given system of multivariate polynomials. Since nonlinear polynomial systems are a mathematical model for a large class of problems in science and engineering, it is no surprise that a general algorithmic method like the Gr¨bner bases method for handling such systems o has an unlimited range of applications. In fact, in many fields of science and engineering, prior to the advent of Gr¨bner bases theory only linear o approximations of the actual problems could be studied. In some cases, if we are satisfied with approximate solutions, linear approximations to the original models may be good enough. However, there are many areas in which only the exact treatment of the exact non-linear problems gives meaningful answers. For example, graph coloring problems can be translated into the problem of solving certain non-linear polynomial systems, see below, where each solution corresponds to a possible coloring. Linear approximations to the systems or approximations to the solutions of the original systems would not make it possible to distinguish between or identify the various colorings. Over the years, a many applications of Gr¨bner bases theory, some of o them quite surprising, have been found. An overview on these applications, up to 1998, can be found in the proceedings [6]. An online-bibliography has been compiled at the occasion of the Special Semester on Gr¨bner Bases o at the Radon Institute for Computational and Applied Mathematics (RI- CAM) in Linz 2006, which contains over 1000 papers on Gr¨bner bases, o see www.ricam.oeaw.ac.at/spec_sem/srs/groeb/ (follow link “Bibliogra- phy”). A quick way of getting access to the growing literature on Gr¨bner o bases is to use the online citation index “citeseer” (at researchindex.org/). If one enters “Gr¨bner” or “Buchberger”, one will obtain several thousand ci- o tations of papers containing contributions to the development, extension and improvement of the Gr¨bner bases method and its many applications. Also, o there are a couple of textbooks available on Gr¨bner bases, see for example o [2] and [18]. The latter contains a list of most other textbooks on Gr¨bner o bases in its introduction. Applications of Gr¨bner bases reach from algebraic geometry or poly- o 7 nomial ideal theory (the original field for which Gr¨bner bases theory was o invented in [3, 4]) to invariant theory, coding theory, cryptography and cryp- toanalysis, systems theory, control theory, automated geometrical theorem proving, graph theory, invention and proof of combinatorial identities, soft- ware engineering, integration of differential equations and many others. Here are some surprising recent applications of Gr¨bner bases in quite distinct ar- o eas: Origami Construction The Japanese art of Origami aims at construct- ing two-dimensional and three-dimensional objects by certain folding operations starting from a square paper sheet. Six classes of folding operations are permitted. The mathematical problem consists in de- ciding whether a given sequence of operations provenly leads to an object having prescribed properties. For example, ways were proposed to fold a regular heptagon from the initial square using only Origami folding operations. In this case, the question is to prove rigorously that a proposed sequence of operations results, indeed, in a heptagon. Gr¨bner bases can be used for proving or disproving the correctness o of arbitrary such sequences of operations for arbitrary properties (that can be described by multivariate polynomials) completely automati- cally. The method consists, roughly, in translating the sequence of operations into a set of polynomial relations (which is easily possible) and to check whether or not the polynomial that describes the desired property is in the “ideal” generated by the polynomial relations, which is always possible by the Gr¨bner bases methodology. For details, see o for example [15]. Solution of Linear Boundary Value Problems Initial value problems for a wide class of differential equations can be solved by symbolic meth- ods. For boundary value problems, there were hardly any symbolic methods available. A generalization of Gr¨bner bases theory for non- o commutative polynomials allows now to obtain symbolic solutions also for boundary value problems. In this new application, the strength of the Gr¨bner bases method is demonstrated by the fact that the o invention of the Green’s functions, which was deemed to be an ad hoc creative process for each boundary value problem, is replaced by a completely algorithmic procedure, which is nothing else than just the reduction (“remaindering”) operation w.r.t. a (non-commutative) 8 Gr¨bner basis, which represents the relations between the fundamental o operations of functional analysis for boundary problems, see [23]. Optimization of Oil Platforms (the “Algebraic Oil Project”) In this surprising application, the fundamental problem of improved control of the valves on an oil platform, with unknown geometry of the oil cav- erns under the sea, is attacked. In a “learning phase” the quantity of oil produced in dependence on the position of the valves on the platform is measured. The assumption is made that this dependence can be described by a system of multivariate polynomials (whose coef- ficients are unknown in the learning phase). With the data collected from sufficiently many measurements, the Gr¨bner bases method allows o then to determine these coefficients (in fact, the system of polynomials generated for modelling the flow will be a Gr¨bner basis). Now, this o multivariate polynomial model of the flow can be used, in the “appli- cation phase”, to optimize the flow w.r.t. various criteria. This new application of (a numerical variant of) Gr¨bner bases was proposed in o a cooperation between Shell company and the CoCoA Group, see [14]. The results are practically promising. Automated Synthesis of Loop Invariants for Programs The proof that programs meet their specification is one of the fundamental problems in computer science. The method of “loop invariants” for solving this problem requests that, for certain points in the given program, an as- sertion (formula), called a “loop invariant” is invented for which one can prove that, for every moment the program gets to that point the respective assertion is true for the values of the program variables. The invention of these loop invariants often needs quite some creativity and this is a major obstacle for the practical use of the method of loop invariants. In the Theorema Group at RISC, a method was developed by which, for a wide class of programs, these loop invariants can be generated by a combination of symbolic execution of the program, so- lution of the resulting recursive equations, see Section 1 above, and the use of the Gr¨bner bases method. o Breaking Cryptographic Codes Gr¨bner bases are being used both for o constructing cryptosystems as well as for trying to break such sys- tems (cryptoanalysis). Breaking an (algebraic) crypto-code basically amounts to solving a system of nonlinear algebraic equations with 9 Boolean coefficients for the values that constitute the bits of the un- known code, i.e. the number of unknowns in the system is the number of unknown bits in the code. Typically, this number is 80 or more. Recently, proposals for algebraic codes that have been deemed to be sufficiently safe have been broken using the Gr¨bner bases method, see o [11]. This was one of the most exciting recent applications of Gr¨bner o bases. The Determination of Species Relationship in Evolution In this re- search area, the probabilities of one species being closer in the evolution with some species than with some other species are determined from an anal- ysis of the genetic codes of species. The result of such an analysis is called the phylogenetic tree of the species. In [7] it has recently been shown how this problem of finding the mutual neighborhood probabil- ities can be cast into the language of multivariate polynomial ideals in Gr¨bner bases form. o Wavelets Wavelets are spectra of functions. Each function in a spectrum is determined by a couple of parameters. By combining the functions in a spectrum, i.e. by specifying the values of the individual parameters in a spectrum, (graphical) information can be presented in highly condensed form (“data compression”). The search for suitable spectra of wavelets is an important research topic in wavelet theory. This search leads to systems of algebraic equations that recently have been solved by the Gr¨bner bases method, see [9]. o Gr¨bner bases theory is still a very active research area with focus on gen- o eralizations of the method (e.g. the non-commutative case), specializations for certain classes of polynomial sets (e.g. toric sets) with higher efficiency, new approaches to compute Gr¨bner bases for improving the efficiency, nu- o meric variants of the method, and new applications in a big spectrum of different areas. 2.2 Gr¨bner Bases: Basic Notions and Results o Gr¨bner bases are sets of multivariate polynomials that enjoy certain unique- o ness properties, which make it possible to solve many fundamental problems on such sets algorithmically. The main result of algorithmic Gr¨bner bases o 10 theory is that any finite set of multivariate polynomials can be transformed, by an algorithm, into an equivalent Gr¨bner basis and that, hence, many o fundamental problems on arbitrary sets of multivariate polynomials can be solved algorithmically by, first, transforming the sets into Gr¨bner bases form o and then using the respective algorithms for Gr¨bner bases. Three examples o of such fundamental problems that can be solved algorithmically by trans- formation into Gr¨bner bases form are: o • the exact solution of systems of multivariate polynomial equations, • the problem of deciding whether or not two given multivariate polyno- mials are equivalent w.r.t. to a given set of multivariate polynomials that define the equivalence, • the problem of solving “diophantine” equations, i.e. the problem of finding (all) multivariate polynomials that satisfy linear relations whose coefficients are also multivariate polynomials. We explain here one of the many different, equivalent, ways of defining the notion of Gr¨bner bases. For this, consider for example the two quadratic o bivariate polynomials f1 and f2 in the indeterminates x and y: f1 := −2y + xy f2 := x2 + y 2 . If we fix an ordering on the power products (for example, the lexicographic ordering that ranks y higher than x), each polynomial has a “leading power product”, in our case xy and y 2 , respectively. Consider now the following linear combination g of f1 and f2 : g := (y)f1 + (−x + 2)f2 = 2x2 − x3 . Observation: The leading power product x3 of g is neither a multiple of the leading power product xy of f1 nor a multiple of the leading power prod- uct y 2 of f2 . Now, a set F of multivariate polynomials is called a Gr¨bner o basis (w.r.t. the chosen ordering of power products) iff the above phenomenon cannot happen, i.e. for all f1 , . . . , fm ∈ F and all (infinitely many possible) polynomials h1 , . . . , hm , the leading power product of h1 f1 + . . . + hm fm is a multiple of the leading power product of at least one of the polynomials in F . 11 Example 2.1 The Set F := {f1 , f2 } is not a Gr¨bner basis. The equivalent o 2 3 Gr¨bner basis is {f1 , f2 , f3 }, where f3 := 2x − x , which can only be checked o by the theorem below. The following theorem is the crucial result on which the algorithmic use- fulness of Gr¨bner bases hinges. o Theorem 2.2 (Buchberger) F is a Gr¨bner basis iff, for all f1 , f2 , the o remainder of the S-polynomial of f1 and f2 w.r.t. F is 0. The remainder of a multivariate polynomial w.r.t. a set of such polyno- mials is the rest in a generalized polynomial division, which is an algorithmic process. The S-polynomial of two multivariate polynomials is obtained by multiplying the two polynomials with the lowest possible power products that make the leading power products equal and by subtracting the resulting two polynomials. In the above example, the S-polynomial of f1 and f2 is y(−2y + xy) − x(x2 + y 2 ) = −x3 − 2y 2 . The proof of this theorem is difficult, see [5] for a concise version. The algorithmic power of the Gr¨bner bases method is based on this theorem o and its proof because the theorem shows, essentially, that the infinite test appearing in the definition of Gr¨bner bases for checking whether or not a o given set F is a Gr¨bner basis can be replaced by the finite, algorithmic, test o on the right-hand side of the theorem! This theorem can now be transformed into an algorithm for constructing Gr¨bner bases, i.e. for the problem to o find, for any given multivariate polynomial set F , a set G such that G is a Gr¨bner basis and F and G generate the same set of linear combinations, o see Algorithm 1. The notion of Gr¨bner bases, the theorem on the characterization of o Gr¨bner bases by S-polynomials, and the algorithm for the construction of o Gr¨bner bases, together with termination proof, first applications and com- o plexity considerations, were introduced in the PhD thesis [3] and the corre- sponding journal publication [4]. Buchberger gave the name “Gr¨bner” to his o theory for honoring his PhD thesis advisor Wolfgang Gr¨bner (1899–1980). o Example 2.3 Solving the problem of graph coloring by Gr¨bner bases. This o problem consists in finding all admissible colorings in k colors of a graph with n vertices and edges E. A coloring of the vertices of a graph is admissible if 12 Algorithm 1 Buchberger’s Algorithm Start with G ← F for all pairs of polynomials f1 , f2 ∈ G do h ← remainder of the S-polynomial of f1 and f2 w.r.t G if h = 0 then consider the next pair else add h to G and iterate end if end for no two adjacent vertices obtain the same color. For example, the left picture in Figure 1 is an admissible coloring in 3 colors of a graph with 4 vertices and edges {1, 2}, {1, 3}, {2, 3}, {3, 4}, whereas the right picture in Figure 1 is not an admissible coloring in 3 colors of the same graph. 1 2 1 2                         3 4 3 4 Figure 1: An admissible and a non-admissible coloring of a graph. It is easy to see that the possible colorings of a graph can be obtained by considering all solutions of a certain system of polynomial equations (where the n indeterminates appearing in the polynomials correspond to the colors a the n vertices). We illustrate the construction of the polynomial system in 13 the example: {−1 + x3 ,1 . . . the color at vertex 1 is a ternary root of 1, i.e. the three ternary roots of 1 encode the three colors −1 + x3 , 2 . . . the color at vertex 2 is a ternary root of 1, −1 + x3 , 3 −1 + x3 , 4 x2 + x1 x2 + x2 , . . . the colors at 1 and 2 must be different 1 2 x2 + x1 x 3 + x2 , 1 3 x2 + x2 x 3 + x2 , 2 3 x2 + x3 x4 + x2 } 3 4 Now, compute a Gr¨bner basis of this polynomial set (this can be done by o using for example Mathematica because, nowadays, Buchberger’s algorithm is routinely available in all mathematical software systems) and compute all solutions. The corresponding Gr¨bner basis is: o −1 + x3 , x2 + x1 x2 + x2 , −x1 − x2 − x3 , −x1 x2 + x1 x4 + x2 x4 − x2 . 1 1 2 4 One sees that the corresponding Gr¨bner basis is “decoupled” (this is one o of the fundamental properties of Gr¨bner bases w.r.t. to lexicographic or- o derings), i.e. it can be completely solved by determining the values of one indeterminate after the other, starting with the first polynomial, which is always a polynomial in the first indeterminate only. For example, the solution {x1 → 1, x2 → −(−1)1/3 , x3 → −1 + (−1)1/3 , x4 → −(−1)1/3 } (1) corresponds to the coloring illustrated in Figure 2. Oversimplified, the strategy for solving problems with Gr¨bner bases consists o of the following steps: 1. Describe the problem (e.g. “coloring”), if possible, by sets of multi- variate polynomials (e.g. polynomials on “roots of unity” instead of “colors”). 2. Transform the occurring sets of polynomials into Gr¨bner basis form. o 14 1 2             3 4 Figure 2: The graph coloring corresponding to the solution (1) of a system of polynomial equations. 3. Solve the problem for the corresponding Gr¨bner bases (which, typ- o ically, is simpler than for the original sets). (For instance, find all solutions of the Gr¨bner basis.) o 4. Translate the solutions back to the original sets. (In the case of find- ing solutions, the solutions of the Gr¨bner basis are the same as the o solutions of the original system.) 5. Interpret the results in the language of the original problem (e.g. trans- late “roots of unity” into “colors”). References [1] M. Abramowitz and I. Stegun, editors. Handbook of Mathematical Func- tions. United States Government Printing Office, 1964. Reprinted by Dover, 1965. [2] T. Becker and V. Weispfenning. Gr¨bner Bases: A Computational Ap- o proach to Commutative Algebra. Springer, New York, 1993. [3] B. Buchberger. An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal. PhD thesis, University Innsbruck, Mathematical Institute, 1965. German, English translation in: J. of Symbolic Computation, Special Issue on Logic, Mathematics, and Computer Science: Interactions. Volume 41, Number 3–4, Pages 475–511, 2006. 15 [4] B. Buchberger. An Algorithmical Criterion for the Solvability of Alge- braic Systems of Equations. Aequationes mathematicae, 4(3):374–383, 1970. German. English translation in: B. Buchberger, F. Winkler (eds.), Groebner Bases and Applications, London Mathematical Society Lec- ture Note Series, Vol. 251, Cambridge University Press, 1998, pp. 535– 545. [5] B. Buchberger. Introduction to Groebner Bases. In B. Buchberger and F. Winkler, editors, Groebner Bases and Applications, number 251 in London Mathematical Society Lecture Notes Series, pages 3–31. Cam- bridge University Press, 1998. [6] Bruno Buchberger and Franz Winkler, editors. Gr¨bner Bases and Ap- o plications. Proc. of the International Conference “33 Years of Groebner Bases”, volume 251 of London Mathematical Society Lecture Note Se- ries. Cambridge University Press, 1998. 560 pages. [7] J. Chifman and S. Petrovic. Toric Ideals of Phylogenetic Invariants for the General Group-based Model on Claw Trees K1,n. In H. Anai, K. Horimoto, and T. Kutsia, editors, Algebraic Biology, Proc. of the Second International Conference on Algebraic Biology, volume 4545 of Lecture Notes in Computer Science, pages 307–321, RISC, Hagenberg, Austria, July 2007. Springer. [8] F. Chyzak, I. Gutman, and P. Paule. Predicting the Number of Hexag- onal Systems with 24 and 25 Hexagons. MATCH, 40:139–151, 1999. [9] F. Chyzak, P. Paule, O. Scherzer, A. Schoisswohl, and B. Zimmermann. The Construction of Orthonormal Wavelets using Symbolic Methods and a Matrix Analytical Approach for Wavelets on the Interval. Exper- iment. Math., 10:67–86, 2001. [10] Hans J. Eysenck. Check Your Own I.Q. Rowohlt, 1966. [11] J.C. Faugere and A. Joux. Algebraic Cryptoanalysis of Hidden Field Equation (HFE) Cryptosystems Using Groebner Bases. In D. Boneh, editor, CRYPTO 2003, volume 2729 of Lecture Notes in Computer Sci- ence, pages 44–60, 2003. 16 [12] S. Gerhold and M. Kauers. A Procedure for Proving Special Function Inequalities Involving a Discrete Parameter. In Proceedings of ISSAC’05, pages 156–162. ACM Press, 2005. [13] R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics. Addison-Wesley, 2nd edition edition, 1994. [14] D. Heldt, M. Kreuzer, S. Pokutta, and H. Poulisse. Algebraische Mod- ellierung mit Methoden der approximativen Computeralgebra und An- ¨ wendungen in der Olindustrie. OR-News, 28, 2006. issn 1437-2045. [15] T. Ida, D. Tepeneu, B. Buchberger, and J. Robu. Proving and Con- straint Solving in Computational Origami. In B. Buchberger and John Campbell, editors, Proceedings of AISC 2004 (7 th International Con- ference on Artificial Intelligence and Symbolic Computation), volume 3249 of Springer Lecture Notes in Artificial Intelligence, pages 132–142. Copyright: Springer-Berlin, 22-24 September 2004. [16] Manuel Kauers. Computer Algebra for Special Function Inequalities. In Tewodros Amdeberhan and Victor Moll, editors, Tapas in Experimental Mathematics, volume 457 of Contemporary Mathematics, pages 215–235. AMS, 2008. [17] Manuel Kauers and Peter Paule. A Computer Proof of Moll’s Log- Concavity Conjecture. Proceedings of the AMS, 135(12):3847–3856, De- cember 2007. [18] M. Kreuzer and L. Robbiano. Computational Commutative Algebra I. Springer New York–Heidelberg, 2000. [19] Christian Mallinger. Algorithmic Manipulations and Transformations of Univariate Holonomic Functions and Sequences. Master’s thesis, RISC- Linz, August 1996. [20] P. Paule and V. Pillwein. Automatic Improvements of Wallis’ Inequal- ity. Technical Report 08–18, RISC Report Series, University of Linz, Austria, 2008. [21] P. Paule and M. Schorn. A Mathematica version of Zeilberger’s Algo- rithm for Proving Binomial Coefficient Identities. J. Symbolic Comput., 20(5-6):673–698, 1995. 17 [22] V. Pillwein. Positivity of Certain Sums over Jacobi Kernel Polynomials. Advances Appl. Math., 41:365–377, 2007. [23] M. Rosenkranz, B. Buchberger, and H. W. Engl. Solving Linear Bound- ary Value Problems Via Non-commutative Groebner Bases. Applicable Analysis, 82(7):655–675, July 2003. [24] B. Salvy and P. Zimmermann. Gfun: A Package for the Manipulation of Generating and Holonomic Functions in One Variable. ACM Trans. Math. Software, 20:163–177, 1994. [25] N.J.A. Sloane. A Handbook of Integer Sequences. Academic Press, 1973. [26] N.J.A. Sloane. The New Book of Integer Sequences. Springer, 1994. [27] Markus Voege, Anthony J. Guttmann, and Iwan Jensen. On the Num- ber of Benzenoid Hydrocarbons. Journal of Chemical Information and Computer Sciences, 42(3):456–466, 2002. [28] D. Zeilberger. A Fast Algorithm for Proving Terminating Hypergeomet- ric Identities. Discrete Math., 80:207–211, 1990. [29] D. Zeilberger. A Holonomic Systems Approach to Special Function Iden- titites. J. Comput. Appl. Math., 32:321–368, 1990. 18