Computer assisted proof of the existence of homoclinic tangency for the Henon map and for the forced-damped pendulum

We present a topological method for the efficient computer assisted verification of the existence of the homoclinic tangency which unfolds generically in a one-parameter family of planar maps. The method has been applied to the Henon map and the forced damped pendulum ODE.