Automated proofs of the moufang identities in alternative rings |
| |
Authors: | Siva Anantharaman Jieh Hsiang |
| |
Affiliation: | (1) LIFO, Dépt. Math-Info., Université d'Orléans, 45067 Orléans Cedex 02, France;(2) Department of Computer Science, National Taiwan University, Taipei, Taiwan, Republic of China |
| |
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.On leave from the Department of Computer Science, UNYY at Stony Brook, New York. Research supported in part by NSF grants CCR-8805734, INT-8715231, and CCR-8901322. |
| |
Keywords: | Automated theorem proving equational logic Knuth-Bendix completion term rewriting Moufang identities alternative rings |
本文献已被 SpringerLink 等数据库收录! |
|