@inproceedings{e7ab9820e2c54e2f886e54729e042142,

title = "Theorem proving with group presentations: Examples and questions",

abstract = "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 ]",

author = "Ursula Martin",

year = "1996",

doi = "10.1007/3-540-61511-3_100",

language = "English",

isbn = "978-3-540-68687-3",

series = "Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)",

publisher = "Springer Berlin Heidelberg",

pages = "358--372",

editor = "McRobbie, {M. A.} and Slaney, {J. K.}",

booktitle = "Automated Deduction - Cade-13",

}