Neste trabalho, apresentamos um método computacional rigoroso para a demonstração de existência de órbitas periódicas de alguns sistemas de equações diferenciais ordinárias com campo autônomo do tipo polinomial. Mostraremos que o problema de encontrar órbitas periódicas para esses sistemas de equações é equivalente a buscar por raízes de certas funções definidas no espaço de Banach das sequências com decaimento algébrico. O método pode ser dividido em duas etapas. Na primeira, buscamos numericamente por soluções periódicas aproximadas. Na segunda, mostraremos a existência de uma órbita periódica numa vizinhança da curva encontrada numericamente. O rigor das verificações computacionais é garantido pelo uso de aritimética intervalar.

In this work, we present a rigorous computational method for proving the existence of periodic orbits of some systems of ordinary differential equations with autonomous vector field of polynomial type. We show that the problem of finding periodic orbits for these systems is equivalent to check for roots of certain functions defined in the Banach space of sequences with algebraic decay. The method can be divided into two steps. First, we seek, numerically, to approximated periodic solutions. Then, we show the existence of a periodic orbit in a neighborhood of the curve numerically found in the previous stage. The accuracy of the computational verifications is guaranteed by the use of interval arithmetic.