Some experiments in nonassociative ring theory with an automated theorem prover (Q1105012)

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.