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 Shcweitzer'95.
展开▼
