Some experiments in nonassociative ring theory with an automated theorem prover (Q1105012)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Some experiments in nonassociative ring theory with an automated theorem prover |
scientific article |
Statements
Some experiments in nonassociative ring theory with an automated theorem prover (English)
0 references
1987
0 references
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.
0 references
automated theorem prover
0 references