Case studies of Z-module reasoning: Proving benchmark theorems from ring theory (Q1102357)

A new method, called Z-module reasoning, was formulatd for proving and discovering theorems from ring theory. In a case study, the ZMR system designed to implement this method was used to prove the benchmark \(x^ 3\) ring theorem from associative ring theory. The system proved the theorem quite efficiently. The system was then used to prove the \(x^ 4\) ring theorem from associative ring theory. Again, a proof was produced easily. These proofs, together with the successes in proving other difficult theorems from ring theory suggest that the Z-module reasoning method is useful for solving a class of problems relying on equality reasoning. This paper illustrates the Z-module reasoning method, and analyzes the computer proof of the \(x^ 3\) ring theorem.