Symbolic Computation: Computer Algebra and Logic

Abstract

In this paper we present our personal view of what should be the next step in the development of symbolic computation systems. The main point is that future systems should integrate the power of algebra and logic. We identify four gaps between the future ideal and the systems available at present: the logic, the syntax, the mathematics, and the prover gap, respectively. We discuss higher order logic without extensionality and with set theory as a subtheory as a logic frame for future systems and we propose to start from existing computer algebra systems and proceed by adding new facilities for closing the syntax, mathematics, and the prover gaps. Mathematica seems to be a particularly suitable candidate for such an approach. As the main technique for structuring mathematical knowledge, mathematical methods (including algorithms), and also mathematical proofs, we underline the practical importance of functors and show how they can be naturally embedded into Mathematica.