The theory of Enceladus and Dione - An application of computerized algebra in dynamical astronomy

The orbits of the satellites of the outer planets are poorly known, due to lack of attention over the past half century. We have been developing a new theory of Saturn's satellites Enceladus and Dione which is literal (all constants of integration appear explicitly), canonically invariant (the Hori-Lie method is used), and which correctly handles the eccentricity-type resonance between the two satellites. The algebraic manipulations are being performed using the TRIGMAN formula manipulation language, and the programs have been developed so that with minor modifications they can be used on the Mimas-Tethys and Titan-Hyperion systems.