ABSTRACT
Integration of computer algebra and automated deduction aims at a more uniform way to structure mathematical knowledge. This is traditionally either represented explicitly, as stored facts in a theorem prover, or implicitly, in the algorithms of a computer algebra system.
The tight coupling of algorithms and their specifications leads to algorithmic theories. One way of obtaining such a coupling is through schemata. The concept of schemata enables a meaningful definition of the context of a computation. Contexts in turn make the coupling memory-efficient.
