Classifying Isomorphic Residue Classes

Abstract. We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic prop-erties of residue classes as well as for isomorphisms between residue classes using dierent proving techniques, which are implemented as stra-tegies in a multi-strategy proof planner. We show how these techniques help to successfully derive proofs in our domain and explain how the search space of the proof planner can be drastically reduced by employ-ing computations of two computer algebra systems during the planning process. Moreover, we discuss the results of experiments we conducted which give evidence that with the help of the computer algebra systems the planner is able to solve problems for which it would fail to create a proof otherwise.