ISSN:
1573-0670
Keywords:
abstract algebra
;
completion
;
Knuth-Bendix procedure
;
groups
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract 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 by 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00244494
Permalink
