Skip to content

Research at St Andrews

Some Group Theoretic Examples with Completion Theorem Provers

Research output: Contribution to journalArticle

Author(s)

School/Research organisations

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.

Close

Details

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

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. GAP – Groups, Algorithms, and Programming, Version 4.10.2

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 19 Jun 2019

    Research output: Non-textual formSoftware

  2. GAP – Groups, Algorithms, and Programming, Version 4.10.1

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 23 Feb 2019

    Research output: Non-textual formSoftware

  3. GAP – Groups, Algorithms, and Programming, Version 4.10.0

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 1 Nov 2018

    Research output: Non-textual formSoftware

  4. GAP – Groups, Algorithms, and Programming, Version 4.9.3

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 5 Sep 2018

    Research output: Non-textual formSoftware

  5. PatternClass Version 2.4.2: A permutation pattern class package (GAP package)

    Hoffmann, R., Linton, S. & Albert, M., 24 Jul 2018

    Research output: Non-textual formSoftware

Related by journal

  1. Type-based cost analysis for lazy functional languages

    Jost, S., Vasconcelos, P., Florido, M. & Hammond, K., Jun 2017, In : Journal of Automated Reasoning. 59, 1, p. 87-120 34 p.

    Research output: Contribution to journalArticle

  2. Satisfiability in the year 2000

    Gent, I. P. & Walsh, T., Feb 2002, In : Journal of Automated Reasoning. 28, 2, p. 99-99 1 p.

    Research output: Contribution to journalEditorial

  3. Satisfiability in the Year 2000

    Gent, I. P. & Walsh, T., Feb 2000, In : Journal of Automated Reasoning. 24, 1-2, p. 1-3 3 p.

    Research output: Contribution to journalEditorial

  4. Unification in Boolean Rings

    Martin, U. H. M. & Nipkow, T., 1988, In : Journal of Automated Reasoning. 4, p. 381-396

    Research output: Contribution to journalArticle

ID: 104074

Top