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.
CITATION STYLE
Linton, S., Martin, U., Pröhle, P., & Shand, D. (1996). Algebra and automated deduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1104, pp. 448–462). Springer Verlag. https://doi.org/10.1007/3-540-61511-3_106
Mendeley helps you to discover research relevant for your work.