Some Group Theoretic Examples with Completion Theorem Provers

. In this paper we investigate the performance of completion theorem provers on a number of group theoretic problems. These are of a rather different character to the usual test problems and exercise different features of the programs. Very large rewriting systems and very deeply nested terms arise, but, where the programs allow, additional mathematical information can often be used to dramatically speed the computations. We compare two general-purpose theorem provers with some more specialised tools and conclude by drawing some lessons for the design of future general-purpose provers. 1 Introduction This paper is an expanded version of the paper of the same name given at the workshop "Automated Reasoning in Algebra" at the CADE-12 conference in Nancy, France, June 1994. In very general terms, proofs of mathematical results can be obtained in three ways: \Gamma human invented proof ("by hand"); \Gamma special-purpose computations and \Gamma automated theorem proving. Apart from the r..