Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
type: Item
instance of: scholarly article
title: Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
zbMATH Open document ID: 0644.16023
author: Tie-Cheng Wang
published in: Journal of Automated Reasoning
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 16U70
Mathematics Subject Classification ID: 16-04
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4049822
zbMATH Keywords: automated theorem proving
zbMATH Keywords: Z-module reasoning
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 4049822