Algebra and automated deduction

Steve Linton, Ursula Martin, Péter Pröhle, Duncan Shand

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


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.
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 'Algebra and automated deduction'. Together they form a unique fingerprint.

Cite this