Computer-generated proofs of phase portraits for planar systems

This paper introduces new algorithms for automatically constructing proofs for the correctness of phase portraits obtained from numerical integration of structurally stable planar polynomial vector fields. These algorithms are based upon the concept of rotated vector fields and the use of interval arithmetic to obtain rigorous bounds on the accuracy of floating point arithmetic calculations. Phase portrait features such as the existence or non-existence of limit cycles in particular regions are proved while avoiding the awkwardness associated with error estimates for the accuracy of approximate trajectories obtained from numerical integration. In some cases this method extends local analysis to obtain a complete, rigorous description of the flow structure of a system.