Exploring Properties of Residue Classes

Volker Sorge

We describe a framework for exploring simple algebraic properties of operations on residue class sets over the integers as well as possible isomorphism between these sets. The framework is implemented within the OMEGA theorem proving environment. It employs computations of the computer algebra system GAP to classify a given residue class set together with one or two operations in terms of its algebraic structure. During this classification process proof obligations for proving or refuting single properties are generated. These proof obligations are passed to OMEGA multi-strategy proof planner MULTI that constructs a proof with the help of GAP and MAPLE. After classifying the residue class sets isomorphism between two sets can be automatically detected and either proved or refuted.

Since the presented exploration framework has originated from work done in the context of tutor systems, the motivation is not to obtain new results in finite algebra. It shall rather enable a user to learn fundamental algebraic notions by fiddling about with arbitrary residue class sets and combinations of operations. Moreover the module enables the automatic exploration of large testbeds.

Christoph Benzmüller, chris@ags.uni-sb.de

Last modified: Wed Sep 20 16:14:33 MEST 2000