Institute of Mathematics and Informatics Bulgarian Academy of Sciences
Serdica Journal of Computing, Vol. 4, No 1, (2010), 73p-84p
We discuss some main points of computer-assisted proofs based
on reliable numerical computations. Such so-called self-validating numerical
methods in combination with exact symbolic manipulations result in very
powerful mathematical software tools. These tools allow proving mathematical
statements (existence of a fixed point, of a solution of an ODE, of
a zero of a continuous function, of a global minimum within a given range,
etc.) using a digital computer. To validate the assertions of the underlying
theorems fast finite precision arithmetic is used. The results are absolutely
To demonstrate the power of reliable symbolic-numeric computations we
investigate in some details the verification of very long periodic orbits of
chaotic dynamical systems. The verification is done directly in Maple, e.g.
using the Maple Power Tool intpakX or, more efficiently, using the C++
class library C-XSC.