unofficial copies [PDF], [PS]

by Robert L. Constable and Paul B. Jackson

The purpose of this paper is to report on our efforts to give a formal account of some of the algebra used in Computer Algebra Systems (CAS). In particular, we look at the concepts used in the so-called 3rd generation algebra systems, such as Axiom and Weyl. It is our claim that the Nuprl proof development system is especially well-suited to support this kind of mathematics. We have discovered in the course of our work some interesting ways in which Nuprl can internet with a CAS, and we want to illustrate these. Discovering those interactions presented us with new ways of looking at the role of theorem provers, proof development systems and problem solving environments. We hope that people find these observations a valuable complement to the technical results we present.

The starting point for us was an attempt to apply Nuprl in the realm of computational science. We were led by discussions with Conal Mannion to explore ways that we could provide a "semantics for computer algebra systems." This reminded us of remarks by Dana Scott and led to reading carefully the papers of Clarke and Zhao on Analytica. Finally we were led to looking in detail at Weyl and Axiom. We came to see a clear and deep connection between work in these systems and our own. Basically, the connection arises because these systems are very careful about the notion of an algebraic domain. They define such domains as we define types. There is an even deeper connection between Axiom and Nuprl in that both are concerned with constructive mathematics in one form or another.