Karsten Homann and Jacques Calmet Abstract
An intelligent mathematical environment must enable symbolic mathematical computation and sophisticated reasoning techniques on the underlying mathematical laws. This paper disscusses different possible levels of interaction between a symbolic calculator based on algebraic algorithms and a theorem prover. A high level of interaction requires a common knowledge representation of the mathematical knowledge of the two systems. We describe a model for such a knowledge base mainly consisting of type and algorithm schemata, algebraic algorithms and theorems.