Theorem proving with group presentations: Examples and questions

Ursula Martin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Let G be a group on generators A. We investigate C(G,A), the class of all t-complete rewrite systems for G over A, that is convergent inter-reduced rewrite systems for G which can be proved terminating with a total division ordering on A*. Given G, A and an element > of Tot(A), the total division orderings over A, there is a unique convergent inter-reduced rewrite system for G which can be proved terminating using >. C(G,A) induces a partition of Tot(A), where the complete system T corresponds to the set of all orderings which prove T terminating. We give a collection of examples which illustrate different phenomena which can occur, and indicate some of the natural questions which arise. In particular we investigate how these results extend to subgroups and quotients. [ Rewrite rules, algebra ]
Original languageEnglish
Title of host publicationAutomated Deduction - Cade-13
Subtitle of host publication13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30 – August 3, 1996 Proceedings
EditorsM. A. McRobbie, J. K. Slaney
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Print)978-3-540-68687-3
Publication statusPublished - 1996

Publication series

NameLecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)


Dive into the research topics of 'Theorem proving with group presentations: Examples and questions'. Together they form a unique fingerprint.

Cite this