Automated reasoning in algebra
by
David Stanovsky
Charles University, Prague

Thanks to the development of automated theorem provers and the increasing speed of computers, automated reasoning became a valuable tool for working algebraists. I will overview some of the results in algebra achieved with assistance of theorem provers.

In particular, automated reasoning tools have had great impact on loop theory over the past decade, both in finding proofs and in constructing examples. I'll shortly refer about our recent project with JD Phillips, the QPTP library, created to compare performance of various provers on loop theory problems.

Date received: May 7, 2008