Case studies of Z-module reasoning: Proving benchmark theorems from ring theory (Q1102357)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Case studies of Z-module reasoning: Proving benchmark theorems from ring theory |
scientific article |
Statements
Case studies of Z-module reasoning: Proving benchmark theorems from ring theory (English)
0 references
1987
0 references
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.
0 references
automated theorem proving
0 references
Z-module reasoning
0 references