Symbolic dynamics based method for rigorous study of the existence of short cycles for chaotic systems

It is shown that the problem of existence of periodic orbits can be studied rigorously by means of a symbolic dynamics approach combined with interval methods. Symbolic dynamics is used to find approximate initial positions of periodic points and interval operators are used to prove the existence of periodic orbits in a neighborhood of the computer generated solution. As an example the Lorenz system is studied. All 2536 periodic orbits of the Poincare map with the period n les 14 are found.