Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
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.
- Automated proofs of equality problems in Overbeek's competition
- Solving open problems in right alternative rings with Z-module reasoning
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Automated deduction in ring theory
- Z-module reasoning
- scientific article; zbMATH DE number 3870641 (Why is no real title available?)
- Unnecessary inferences in associative-commutative completion procedures
- scientific article; zbMATH DE number 4068331 (Why is no real title available?)
- A case study of completion modulo distributivity and Abelian groups
- Automated proofs of the Moufang identities in alternative rings
This page was built for publication: Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1102357)
