Description
Abstract. In this talk we consider the problem of automatically proving inequalities involving sequences that are only given in terms of their defining recurrence relations. We will consider sequences satisfying linear recurrences with constant coefficients (C-recursive), linear recurrences with polynomial coefficients (P-recursive or holonomic), or certain systems of polynomial non-linear recurrences (admissible). Even when restricting to the simplest class, C-recursive, and the positivity problem, decidability is only known for orders up to five. And yet, there are computer algebra methods that try to tackle this problem. Obviously, they do not succeed on all types of input and so even though correctness can be proven, termination is typically an issue. In this talk, we will give an overview on this topic, share some available methods and showcases where algorithmic proofs actually succeeded.
