An Integrated Framework for Computer Algebra and Computer Theorem Proving

Sound mathematics is essential in all modern technological developments. As we build increasingly complex systems, mathematical reasoning becomes more difficult and errorprone. Therefore, a computer system is needed that mechanizes the process of doing mathematics. There are two main kinds of mechanized mathematics systems: computer algebra systems that perform many kinds of symbolic computations, and computer theorem proving systems, which support the construction of machine-checked proofs. The objective of this project is to develop a new approach to mechanized mathematics in which computer algebra and computer theorem proving are merged without sacrificing power or soundness. This project completed in March 2003.