Some Group Theoretic Examples with Completion Theorem Provers

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

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.

Original languageEnglish
Pages (from-to)145-169
Number of pages25
JournalJournal of Automated Reasoning
Volume17
Issue number2
Publication statusPublished - Oct 1996

Keywords

  • abstract algebra
  • completion
  • Knuth-Bendix procedure
  • groups
  • WORD PROBLEM
  • THUE SYSTEM
  • HOMOLOGY
  • MONOIDS

Fingerprint

Dive into the research topics of 'Some Group Theoretic Examples with Completion Theorem Provers'. Together they form a unique fingerprint.

Cite this