Computer proofs in Group Theory |
| |
| Authors: | Yuan Yu |
| |
| Affiliation: | (1) The University of Texas at Austin, 78712 Austin, TX, USA |
| |
| Abstract: | This paper reports the results of an experiment in using the Boyer-Moore Theorem Prover in seeking computer-checked proofs in Group Theory. Starting from the axioms for groups and elementary list and number theory, the theorem prover was led to the proofs of two basic theorems in Elementary Group Theory by a sequence of lemmas suggested by the author. The computer proofs illustrate the effective use of the Boyer-Moore Theorem Prover in Group Theory. |
| |
| Keywords: | Automated theorem proving Boyer-Moore theorem prover group theory homomorphism kernel the Lagrange theorem |
| 本文献已被 SpringerLink 等数据库收录！ |
