Automated Proofs of the Moufang Identities in Alternative Rings
Resource
Journal of Automated Reasoning, v.6, p.79-109
Journal
Journal of Automated Reasoning
Journal Volume
6
Journal Issue
1
Pages
79-109
Date Issued
1992
Date
1992
Author(s)
Abstract
In this paper we present automatic proofs of the Moufang identities in alternative rings. Our approach is based on the term rewriting (Knuth-Bendix completion) method, enforced with various features. Our proofs seem to be the first computer proofs of these problems done by a general purpose theorem prover. We also present a direct proof of a certain property of alternative rings without employing any auxiliary functions. To our knowledge our computer proof seems to be the first direct proof of this property, by human or by a computer. © 1990 Kluwer Academic Publishers.
SDGs
Type
journal article
File(s)![Thumbnail Image]()
Loading...
Name
17.pdf
Size
23.19 KB
Format
Adobe PDF
Checksum
(MD5):85b327e68cd4213aacf283dc6e7f3094