We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proving techniques, which are implemented as strategies 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 employing 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. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Meier, A., Pollet, M., & Sorge, V. (2001). Classifying isomorphic residue classes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2178 LNCS, pp. 494–508). Springer Verlag. https://doi.org/10.1007/3-540-45654-6_39
Mendeley helps you to discover research relevant for your work.