Computer Algebra systems have a number of features that distinguish them from other software systems of similar size and complexity: on the one hand, there is the natural underlying semantics of pure mathematics, on the other hand, many of the algorithms used rely on sophisticated mathematical results for their correctness and may impose conditions on their inputs that go far beyond the scope of normal type checking. Finally, these systems tend to grow over time, and without a formal framework for the precise communication of the functions and restrictions of existing components, this process is inefficient and unsafe.
This talk will describe the possible relationships between computer algebra systems and Automated Theorem Proving, and the benefits offered by each, and then outline the work being done in St Andrews on one of them.