Johannes Kepler Symposium on Mathematics
As part of the Johannes Kepler symposium on mathematics Dr. Christoph Koutschan, Johann Radon Institute for Computational and Applied Mathematics (RICAM), Austrian Academy of Sciences (ÖAW), will give a public talk (followed by a discussion) on Wed, June 29, 2016 at 15:15 o'clock at HS 13 on the topic of "Quod Erat Demonstrandum - Proofs by Computer" . The organziers of the symposium,
O.Univ.-Prof. Dr. Ulrich Langer,Univ.-Prof. Dr. Gerhard Larcher
A.Univ.-Prof. Dr. Jürgen Maaß, and
die ÖMG (Österreichische Mathematische Gesellschaft),
hereby cordially invite you.
Series B - Mathematical Colloquium:
The intention is to present new mathematical results for an audience interested in general mathematics.
Quod Erat Demonstrandum - Proofs by Computer
In today's mathematics, the computer has become an indispensable tool, not only as a number cruncher, but also as a proof assistant. There are different approaches to constructing mathematical proofs with the computer: general theorem provers versus special-purpose algorithms that are designed for a particular type of problem or a particular class of objects. We follow the second approach. The objects we deal with are holonomic functions and sequences, a rather large class of mathematical functions, that are given as solutions of certain systems of linear differential equations or recurrences. The type of problem that we address is to prove identities among these objects, possibly involving integrals and sums. The foundations of the proof theory for holonomic functions have been laid by Wilf and Zeilberger in the early 1990s. We first discuss some of our contributions to the theory. Then we present a fine selection of various applications that demonstrate the power and usefulness of this approach.
