Some experiments in nonassociative ring theory with an automated theorem prover
type: Item
instance of: scholarly article
title: Some experiments in nonassociative ring theory with an automated theorem prover
zbMATH Open document ID: 0648.17001
DOI: 10.1007/BF00243209
author: Rick L. Stevens
published in: Journal of Automated Reasoning
publication date: 1987-01-01T00:00:00Z
review text: The author presents some experiments he made using an automated theorem prover, and discusses the difficulties he encountered. In particular, the program was able to prove (1) a ring that satisfies the right and left alternative laws is flexible, and (2) the Teichmüller identity holds in any ring. However, the program was unable to give a completely automated proof that the Moufang identities hold in any alternative ring. By a completely automated proof is meant one in which the program produces a proof in one run without interactive help from the user.
Mathematics Subject Classification ID: 17-04
Mathematics Subject Classification ID: 17A99
zbMATH DE Number: 4057735
zbMATH Keywords: automated theorem prover
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 4057735