Computer Algebra Systems in an Environment of Cooperating Theorem Provers
Date: July 17th (Wednesday)
Time: 09:20-09:45
Abstract
The specifics of some state-of-the-art theorem provers are discussed in order to
point to the topics where they can benefit mostly from cooperation with computer algebra
systems. Current fields of applications of theorem provers are sketched. This suggests
demands on computer algebra systems to facilitate their cooperation with theorem provers,
especially concerning problems of correctness and documentation. The talk is based on the
experience from the integration of automated theorem provers into the interactive system
ILF.