@inproceedings{f43665ad11644fca893c96d348f42a77,

title = "Algebra and automated deduction",

abstract = "This paper develops links between algebra and automated deduction. We show how we have developed heuristics in automated deduction and computer algebra systems by looking at Tietze transformations from group theory and Knuth-Bendix completion. A complex induction proof of a theorem about a wreath product of two groups is developed with the aid of the Larch Prover in order to show how algebraic problems can be attacked with an automated theorem prover. We then present an automated solution of the 7th problem of Schweitzer'95.",

author = "Steve Linton and Ursula Martin and P{\'e}ter Pr{\"o}hle and Duncan Shand",

year = "1996",

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

language = "English",

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

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

publisher = "Springer Berlin Heidelberg",

pages = "448--462",

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

booktitle = "Automated Deduction - Cade-13",

}