Exploring properties of residue classes
Andreas Meier, Volker Sorge · 2001
Abstract. We report on an experiment in exploring properties of residue classes over the integers with the combined eort of a multi-strategy proof planner and two computer algebra systems. An exploration module classi-es a given set and a given operation in terms of the algebraic structure they form. It then calls the proof planner to prove or refute simple proper-ties of the operation. Moreover, we use dierent proof planning strategies to implement various proving techniques: from naive testing of all possi-ble cases to elaborate techniques of equational reasoning and reduction to known cases. 1