This paper was published in a special issue of this journal that was dedicated to the application of automated reasoning to different algebraic domains and problems, and to the integration of computer algebra systems (CASs). The authors summarize their extended case studies to prove known properties of special finite algebraic structures: residue class sets.

Almost 20,000 automatically generated class sets were investigated from the residue classes modulo n, where n ranges from 2 to 10 (mostly 5, 6, and 10). The problems tackled were of two types. First, given residue class sets were classified according to their basic algebraic properties, then, pairs of structures of the same class were examined to determine whether they were isomorphic. To reduce the search space and avoid combinatorial explosion, deep knowledge of the problem domain is built into and used by each applied approach, method, and tool.

The two main approaches examined are application of a multi-strategy proof planner (Multi, an improved version of Omega), and a first-order equational automated theorem prover (ATP), in this case WaldMeister. The authors observed that the former approach was more understandable for humans than the latter, despite the fact that it includes a proof presentation tool.

Using Multi, alternative strategies are defined that are appropriate for the domain. Algebraic knowledge is also applied to the tools incorporated into the system. Two kinds of tools were used in the different case studies: computer algebra systems (CASs), in this case Maple and GAP, for symbolic computation; and the finite model generator Sem for pointwise generation of structures.

The authors suggest that CAS and a model generator both be incorporated into strategies, and their facilities be combined.