Ponente
Manuel Kauers
Descripción
The guess'n'prove problem solving paradigm consists of two steps: first, a solution is "guessed" empirically based on inspection of special cases and/or other dirty and non-rigorous tricks. Only in the second step, a completely rigorous formal proof of the potential solution found in the first step is derived. Computer algebra provides tools for supporting both steps: the guessing part and the proving part. There are cases where the computational cost for proving are much higher than for guessing a solution. One may then be content with an uncertified solution, because in practice, guessed results are correct anyway. In the talk we will illustrate the difference between rigorous and not-so-rigorous-but-nevertheless-trustworthy computations with a combinatorial counting problem on which we recently worked together with D. Zeilberger.
