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

A theory of Saturn's satellites Enceladus and Dione is discussed 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. Algebraic manipulations are designed to be performed using the TRIGMAN formula manipulation language, and computer programs were developed so that, with minor modifications, they can be used on the Mimas-Tethys and Titan-Hyperion systems.