\documentstyle[11pt]{article}



\voffset=-2.6cm
\hoffset=-2.6cm
\textwidth=15.5cm
\textheight=24cm

\begin{document}

\title{Symbolic Computation:\\
Computer Algebra and Logic}


\author{Bruno Buchberger\\
Research Institute for Symbolic Computation\\
A4232 Schlo{\ss} Hagenberg, Austria\\
Bruno.Buchberger@risc.uni-linz.ac.at}

\maketitle



\begin{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. 



\end{abstract}



\section{The Next Goal for Symbolic Computation}

By the work of researchers in various areas, we now have powerful  
tools available that support various aspects of problem solving by  
computer:

\begin{itemize}
\item numerical libraries
\item special purpose systems for simulation, CAD, robotics, neural  
network design,  $\ldots$
\item ``symbolic computation'' systems for computer algebra, computer  
analysis, $\ldots$
\item rewrite labs, logic programming systems, constraint solvers,  
$\ldots$
\item special and general theorem provers, theorem generators,  
theorem checkers, $\ldots$
\item program verification, transformation, and synthesis systems,  
$\ldots$
\item advanced software technology tools in all theses systems,
\item graphics, animation, sound, typesetting, notebook, and  
hyperlink tools in these systems,
\item links between these systems, access through the web, electronic  
user communities, $\ldots$
\end{itemize}

 The availability of these systems has drastically enhanced our  
problem solving potential. However, we want more. Who is ``we''? In  
this paper, I address people who
  \begin{itemize}
   \item        explore,
    \item         invent,
    \item         apply,
    \item         teach,
     \item        study, and
    \item         publish
\end{itemize}
mathematics or, in other words, people who are ``doing'' mathematics.  
In this paper, I do not address people who are casual users of  
mathematics as a ``black box''.
I think that the next natural goal ``we'' should go for is to do all  
of mathematics in one system. Here, by a ``system'', I mean both
\begin{itemize}
\item  a {\em logical} system, which should be a sound and uniform  
frame for all of our mathematical activities and
\item a {\em software} system, which supports these activities.
\end{itemize}

Although there are systems on the market that advertise explicitly  
that they are systems for ``doing'' mathematics, see (Wolfram 1988), I  
think that there are still significant gaps between what we have and  
what we want. Basically, I see four gaps:
 \begin{itemize}
   \item the logic gap,
\item the syntax gap,
\item the mathematics gap, and
\item the prover gap.
\end{itemize} 


I will analyze these gaps in Section 2. Then I will argue, in Section  
3, why Mathematica seems to be a good starting point for developing a  
rapid prototype system that may overcome these gaps. (I will not  
argue, however, that Mathematica  is ``the'' ideal future symbolic  
computation system. In my view, this would only be possible if the  
designers of Mathematica made some basic changes in the design of  
their system.) In Sections 4 to 7, I will then sketch my proposal how  
one may overcome the logic, the syntax, the mathematics, and the  
prover gap, respectively.

\section{The Present Gaps}

\subsection{The Logic Gap}

At present, officially, there is one uniform logic system in use as  
one uniform frame of mathematics (although, inofficially, this frame  
is not at all applied uniformly in the every-day practice of  
mathematicians): The system of ``Bourbakism'', which is first order  
predicate logic plus set theory formulated as a first order theory  
(which is called ``Zermelo Fraenkel set theory''). The problem with  
the Bourbakistic system as a frame for all of mathematics, including  
``algorithmic'' mathematics, is that in this system functions are  
sets. Hence, by the extensionality axiom for sets, functions defined  
by different algorithms but having identical input/output behavior  
are identical. This is not appropriate for the needs of algorithmic  
mathematics where we do not only want to discuss the input/output  
behavior of functions but also properties of the definitions of  
functions (the ``algorithms'') and properties of their computational  
behavior, for example their complexity.
Of course, we could circumvent this problem by defining a specific  
programming language in the frame of ZF (Zermelo-Fraenkel set  
theory). For this, what we had to do is basically to define a binary  
function $I$, the ``interpreter'' of the programming language, within  
ZF. (The object $I( p, d)$ is the ``result of applying the program  
$p$ of the given programming language to the input data $d$''.) Then,  
of course, it is well possible that we have distinct programs $p_1  
\neq p_2$ with identical input/output behavior, i.e. such that
$\forall d ( I( p_1, d) = I( p_2, d)). $

However, this solution is not very natural because, for example in a  
textbook on algorithmic polynomial ideal theory, we would not like to  
spend an additional chapter on introducing an extra programming  
language. Rather, we would like to use certain predicate logic  
formulae, for example equalities, directly for defining certain  
algorithmic functions and predicates.

As an alternative we could use higher order predicate logic. However,  
the problem remains as soon as we introduce an extensionality axiom  
in such a logic as this is done in most of the usual textbooks on  
higher order predicate logic, see for example (Andrews 1986).  
Therefore, in recent years, some authors proposed to use higher order  
predicate logic without extensionality as a frame for mathematics,  
see for example CIC (Huet 1995) and NuPRL (Constable 1995). This is a  
very promising approach. The problem with the present implementations  
of this idea is that it seems to be quite hard to carry over the  
results from Bourbakistic mathematics into these systems. This is,  
however, important because these results are not only of aesthetical  
value but are indispensable for specifying problems, and describing a  
hierarchy of increasingly powerful solutions to problems, even in  
algorithmic mathematics. For example, when describing the membership  
decision problem for polynomial ideals, it is necessary first to  
define the non-algorithmic notion of ``ideal'' and ``residue  class  
domain''. Also, when developing an algorithmic solution for this  
problem, for example by ``Groebner bases'' (Buchberger 1985), it is  
absolutely necessary to carry out proofs for the correctness of the  
solution that involve non-algorithmic concepts of set theory. Also,  
there is still a practical problem with the present implementations  
of higher order predicate logic without extensionality: Their  
practical potential for algebraic computation is not very high.
 

\subsection{The Syntax Gap}

Notation used in ``mathematical'' software systems is still far from  
the usual mathematical notation. For example, in Mathematica, the  
function definition

\begin{verbatim}
      f[ { }] := { } 

      f[ { x1_, x2___}] := Prepend[ f[ { x2}], { x1, x1}] 

\end{verbatim}

\noindent and the function call

\begin{verbatim}
      Integrate[ Sin[ Sqrt[ y + a^2]], y]
\end{verbatim}

\noindent look quite different from the corresponding formulae

\begin{eqnarray*}  f( \langle  \rangle) &:= & \langle  \rangle  \\
   f( \langle x_1, x_2, \ldots \rangle) &:=& \langle x_1, x_1 \rangle  
\smile f( \langle x_2 \rangle ) 
\end{eqnarray*}

\noindent and

    \[ \int{ \sin ( \sqrt{ y + a^2   }) \,dy }\]

\noindent as they may appear in an ordinary mathematical text.  
Syntax, however, {\em is} quite important for practical problem  
solving.

In fact, the next version of Mathematica will provide ``ordinary''  
syntax for mathematical input and output of amazing sophistication,  
see (Soiffer 1995). However, some unpleasant gaps will still remain.  
For example, still, brackets will be used for function application,  
braces will denote tuples instead of sets, and underscores will be  
used in order to declare variables and  ``sequence variables''. 


\subsection{The Mathematics Gap}

For algorithmic mathematics, the traditional algebraic notions are  
too coarse. For example, the following three algebraic structures are  
``equal'' from the point of view of algebra:
\newline

\noindent {\bf Residue Domain Modulo 3:}

\noindent Carrier:
\[ \{\{ 0 + 3 x \mid x \in {\bf I} \}, \{ 1 + 3 x \mid x \in {\bf I}  
\},
    \{ 2 + 3 x \mid x \in {\bf I} \} \}. \]
\noindent Operation:
 \[ \{ y + 3 x \mid x \in {\bf I} \} \oplus_3 \{ z + 3 x \mid x \in  
{\bf I} \} :=
     \{ y + z + 3 x \mid x \in {\bf I} \}. \]
\newline

\noindent {\bf Simplified Residue Domain Modulo 3:}

\noindent Carrier:
\[ \{ 0, 1, 2\}. \]
\noindent Operation:
\[y +_3 z :=
     {\rm remainder}\,( y + z, 3). \]
\newline

\noindent {\bf ``Smallest''  Simplified Residue Domain Modulo 3:}

\noindent Carrier:
\[ \{ -1, 0, 1\}. \]
\noindent Operation:
\[  y \, \overline{+_3}\, z :=
     {\rm smallest\,\, remainder}\,( y + z, 3). \]

From the algorithmic point of view the three structures are  
significantly different. The first structure is non-algorithmic. It  
results from the integers with addition by application of the  
non-algorithmic ``functor'' ``residue class formation modulo a  
congruence relation''. The resulting carrier contains elements that  
are infinite sets and the operation operates on infinite sets and  
produces infinite sets. The second and the third structures are both  
algorithmic, i.e. the objects of the carrier are finitary and can be  
stored in a computer and the operations are computer-realizable. Both  
structures result from the integers with addition by applying the  
functor ``simplification modulo a canonical simplifier''. However,  
the two structures are not identical and, in fact, the complexity of  
the two operations is (slightly) different.

When we ``do'' mathematics, we want to live in both worlds:
\begin{itemize}
\item the world of (non-algorithmic) theorems and proofs,
\item the world of algorithms and computation.
\end{itemize}

\noindent {\bf The World of Theorems and Proofs}: For example, when  
doing Groebner bases theory, we will start with the {\em definition}

\[ G {\rm \ is \ a \ Groebner\ basis}  :\Longleftrightarrow \forall f  
\in
   {\rm Ideal}( G) \ ( f \longrightarrow_G 0) \]

\noindent and will want to prove the following {\em theorem}:

\[ G {\rm \ is \ a \ Groebner\ basis}  \Longleftrightarrow \forall f,  
g \in
    G \ ( {\rm S\!\!- \!\!polynomial} ( f, g) \longrightarrow_G 0).  
\]

\noindent The proof will involve various non-algorithmic proof  
techniques of predicate logic, in particular those for handling  
quantifiers, and non-algorithmic concepts from set theory.

\noindent {\bf The World of Algorithms and Computation}: In the  
example of  Groebner bases theory, the above theorem can be used  
unchanged as an {\em algorithm}

\[ G {\rm \ is \ a \ Groebner\ basis}  :\Longleftrightarrow \forall f  
\in
   {\rm Ideal}( G) \ ( f \longrightarrow_G 0) \]

\noindent The following proposition can now be ``evaluated'' by using  
the above theorem/algorithm and a subset of the predicate logic proof  
techniques, namely equational logic, as ``evaluation machine'': When  
we enter

\[ \{ x^2 y - 3 x, x y^2 - 2 x y + 4\}  {\rm \ is \ a \ Groebner\  
basis}. \]

\noindent The result of the evaluation will be ``no''.

In the future, we would like to live in both worlds within one  
uniform logic and software system!


\subsection{The Prover Gap}

The available universal theorem provers (e.g.\ those based on  
resolution) are general and, therefore, often too inefficient for  
supporting practical theorem proving in a wide range of mathematical  
areas. Also, most times, they are available only as stand-alone  
systems that are not well connected with computer algebra/analysis  
systems.

The same is true also for special provers (proof checkers, proof  
generators) that may be quite efficient for particular mathematical  
theories. However, again, they are rarely integrated with current  
algebra/analysis software systems.

What we need is the integration of both universal and special  
computer-supported theorem proving with the current computer  
algebra/analysis systems so that, when ``doing'' mathematics, one can  
switch between computer-supported theorem/algorithm development and  
algorithm application.

\section{Mathematica is a Good Starting Point}

For filling the gaps analyzed in the preceding section, i.e.\ for   
supporting all aspects of ``doing'' mathematics or, in other words,  
for reaching a new level of sophistication in ``symbolic  
computation'' by combining computer algebra and logic, one can adopt  
one of the following strategies:

\begin{enumerate}
\item One can start from successful proving systems like CIC, NuPRL,  
etc. and add the potential of current computer algebra systems like  
Maple, Mathematica, Macsyma etc.
\item One can start from one of the practically powerful computer  
algebra systems and add the potential of current provers.
\item One could design a completely new system.
\end{enumerate}

I do not suggest the third possibility, at least not at this moment,  
because tremendous work would go into repeating the effort for  
implementing the wonderful man-machine interfaces current algebra and  
proof systems already have. The construction of completely new  
systems or, at least, completely new systems kernels may become  
reasonable and necessary in the future, after we will have  
experimented with various early prototypes of combined algebra/logic  
systems. Rather, I suggest that, at the moment, these experiments  
should be based on either the first or the second possibility.

In this paper, I argue for basing such an experiment for constructing  
an early prototype for a combined algebra/logic system on  
Mathematica. The main reasons can be structured according to the  
analysis of gaps described in Section 2:

\begin{enumerate}
\item Although apparently this was not the intention of the  
Mathematica designers, a close inspection of the Mathematica language  
reveals that, in fact, the innermost part of {\em Mathematica can be  
viewed as  nothing else than directed higher order equational logic  
without extensionality} and, thus, Mathematica can be viewed as a  
programming language inside logic. This feature is unique among all  
existing computer algebra systems.
\item Mathematica has an amazing man/machine interface. Its next  
version will also have wonderful typesetting facilities and, what is  
more, there will be facilities that {\em allow the user to define his  
own syntax} so that higher order logic with quantifiers and the  
programming part of this language can be presented as executable code  
to the system.
\item Using Currying and the module construct, {\em  "functors" can  
be programmed within Mathematica}. This fact is little known but is  
essential for structuring non-algorithmic and algorithmic mathematics  
within a uniform system frame.
\item The directed equational logic facilities of Mathematica are  
available ``twice'' in the system: First, at the basic level, they  
constitute the programming language. Second, at the metalevel, these  
facilities can also be applied to programs (sets of equalities) at  
the first level. This allows one, within Mathematica, to program  
``provers'' for proving properties of the programs defined on the  
first level. Together with the functor principle, well structured  
provers that combine special provers tailored to the various functors  
can be built up.
\end{enumerate}

Of course, it may turn out that basing a uniform logic frame for all  
of mathematics on top of Mathematica may result in intolerable loss  
of speed because some of the more advanced language features must be  
simulated by the available features in Mathematica. If this is the  
case, in a later stage, a new and specially designed kernel should  
replace the present Mathematica kernel. Thus, we repeat, the present  
proposal is only meant as a proposal for implementing a rapid  
prototype of an algebra/logic system as quickly as possible in order  
to be able to study the logical, mathematical, algorithmic, and  
practical implications and gain the necessary experience in using  
such a combined system for inventing and presenting mathematics. 


In the next sections we describe in more detail how we want to  
overcome the logic, syntax, mathematics, and prover gap by adding  
features to higher order logic and implementing them in the frame of  
Mathematica.

\section{Overcoming the Logic Gap}

We start from higher order logic without extensionality. The  
fundamental concept of this logic is ``application'' of an object (a  
``function'') $f$ to some other object $x$, denoted by

   \[ f(x). \]

\noindent Since we do not have extensionality, this (logic instead of  
set-theoretic) notion of a function remains ``fine grain'' (i.e.\   
functions with the same input/output behavior are not necessarily  
identical), which is indispensable for the algorithmic aspects of  
mathematics.

In this paper, we do not discuss the subtle question of using  
``types'' in such a logic. Of course this question is very important  
for obtaining sound proof rules in such a logic. This question is  
deemed to be important also for the practical work within such a  
system when building up the ``tower of mathematical domains''.  
However, in Section 6, we show how functors can be built up in such a  
way that we do not need types for the practical mathematical work  
within the system. Rather, we work with one uniform equality all over  
the system and, in compensation, we give explicit descriptions of the  
objects in the various domains.

We observe that (the innermost kernel of) Mathematica can be viewed  
as an (efficient) implementation of the (directed) equational part of  
higher order logic without extensionality. For example, the induction  
definition (in the syntax of Version 2.2 of Mathematica)

\begin{verbatim}
     apply[ f_, { x1_}]  :=  x1
     apply[ f_, { x1_, x2___}] := f[ x1, apply[ f, { x2}]]
\end{verbatim}

\noindent can be viewed as  two  higher-order logic equalities and,  
at the same time, as an algorithm whose computations for  
variable-free input terms are nothing else than proofs using  
substitution and replacement as inference rules and using the  
equalities in the direction from left to right. (Do not bother about  
the strange syntax of the above Mathematica equalities. In the next  
version (3.0) of Mathematica, the user will be able to define his own  
syntax and may choose to use the usual mathematical syntax. Variables  
with three underscores are ``sequence variables'', i.e.\ variables for  
which arbitrary finite sequences of terms may be substituted. In  
principle, sequence variables are dispensable. However, we think that  
they are practically attractive and useful. Thus, we propose to have  
them in our system. Appropriate changes must then be made to the  
usual proof rules of higher order logic.)

Thus, higher order logic without extensionality contains a practical  
programming language (efficiently implemented as Mathematica) as a  
sub-language. The question is: How can we retain Bourbakistic  
mathematics within this system?

I think that, in addition to the fundamental  ``$\in$''  predicate,   
it suffices to add one more predicate ``is set'' so that we can  
restrict all set-theoretic axioms to those objects that satisfy ``is  
set''. For example, extensionality can be stipulated for objects that  
are sets:

\[ A {\rm \ is\ a\ set} \wedge  B {\rm \ is\ a\ set}  \Longrightarrow
   ( A  =  B  \Longleftrightarrow  
        \forall x ( x \in A  \Longleftrightarrow  x \in B).\]

Similarly, the other axioms of set theory guaranteeing the existence  
of various sets constructed from given sets can be formulated. In the  
same way, we can also introduce the set braces as special quantifier.  
From there on, we can develop (carry over) all of Bourbakistic  
mathematics including the set-theoretic (as opposed to the above  
logic) notion of ``function'' and ``function application''. Of  
course, for set-theoretic function application, we have to introduce  
a new notation. For example, we can introduce the binary function  
constant ``$`$'' and may write ``$f ` x$'' for ``the set-theoretic  
function $f$ applied to x''. One may then prove for example, within  
the system,  that if $f$ is a set-theoretic function and $x$ is in  
the domain of $f$ then the pair $(x,f`x)$ is in $f$. Note again  
that extensionality will remain to be restricted for the  
set-theoretic notion of function application whereas, by intention,  
it is not available for the original, logical, notion of function  
application. For example, if

\begin{eqnarray*} f( x) & := & x + 1 \\
   g( x) & := & x + 2 -1
\end{eqnarray*}  


\noindent then, of course,

    \[ \forall x  \ f( x) = g( x) \]

\noindent and also, for example, 


     \[ \{ ( x, f( x)) \mid x \in {\bf N} \}  =
              \{ ( x, g( x)) \mid x \in {\bf N} \} \]
        

\noindent can be proved. However, 


     \[ f = g \]

\noindent cannot be proved in the system.


\section{Overcoming the Syntax Gap}

The syntax used in the present version of Mathematica (Version 2.2) is quite
different from the usual mathematical notation. The next version of
Mathematica (Version 3.0) will have an amazingly powerful syntax that comes
quite close to ordinary mathematical notation. It will have \TeX \ quality, it
is wysiwyg {\em and} at the same time is formal, i.e.\ the formulae allowed in
Mathematica have (formal although not formally defined) semantics as
executable code and new formulae can be created whose semantics can be
defined. For example, if one does not like that Mathematica uses braces for
denoting tuples rather than sets, the following instruction will introduce
angle brackets for denoting tuples:

\begin{verbatim}
   MakeExpression[ RowBox[ { "<", x___, ">"}], StandardForm] :=
        MakeExpression[ RowBox[ { "{" x, "}"}], StandardForm]
\end{verbatim}

\noindent A similar instruction will also let Mathematica print angle  
brackets instead of braces. Similarly, we can teach the system to  
take the set braces for denoting set construction instead tuple  
construction, to use parentheses instead of brackets for denoting  
function application, and to replace the use of underscores for  
identifying variables and sequence variables by some other  
convention, see the examples  in Section 6.

\section{Overcoming the Mathematics Gap}

\subsection{Building Up Mathematics by Functors}

Both from a structural and a problem solving point of view, I think  
it is important to build up computer-supported mathematics by  
``functors'' that construct new domains from given ones. Structuring  
mathematics by functors has also an immediate implication for  
structuring provers as will be made explicit in Section 7.

The functor view of mathematics can equally well be applied to both  
non-algorithmic and algorithmic mathematics and, in fact, it is the  
unifying view for both worlds. As explained above non-algorithmic  
mathematics and algorithmic mathematics are strongly intermingled  
when ``doing'' mathematics and,  often, the transition from the  
non-algorithmic to the algorithmic context is the actual challenge of  
mathematics and of course is the main challenge of what is called  
``symbolic computation''.

\subsection{Representing Domains}

We view a domain $D$ to be a function that defines functions for
certain ``operators''. For example, the following object $Z$ is a
simple domain:

\begin{eqnarray*}
    Z( o) & := & Plus,\\
      Z( e)   & := &  0,
\end{eqnarray*}

\noindent where ``Plus'' and ``$0$'' are the ``built-in'' addition
and the built-in integer zero of our system, which as we said above
contains the innermost kernel of Mathematica. For syntactic
simplicity, we introduce the convention that ``$o_D$'' etc. stands
for ``$D( o)$'' etc. Thus, we could write, for example,

\[ 2 \ o_Z  \ 2 \]

\noindent which, with the above definitions, evaluates to

\[ 4. \]

\noindent Note that such a notation will be perfectly  possible in a
user-modified syntax of Mathematica 3.0 and the above evaluation can,
hence, be done automatically in Mathematica.

Also we will add the following unary operator ``$\epsilon$'' to any
domain with the convention that, for any domain $D$, $D( \epsilon )$
is a decision function which yields ``True'' for exactly the objects
we consider to be in the ``carrier'' of $D$. For example, we could
define

\[ Z( \epsilon) := {\rm \ IntegerQ} \]

\noindent where ``IntegerQ'' is the built-in decision algorithm for
integers. Note that the symbol ``$\epsilon$'' is different from the
symbol ``$\in$'' that denotes the element predicate of set theory.


\subsection{Representing Functors}

Now, in our terminology (which is basically the terminology used, for
example, also in ML), a functor is just a function that maps domains into
domains. Thus, a functor is an object $F$ that takes $D$ as an argument
and produces $F(D)$ with the view that $F( D)$ can now be applied to any
operation symbol $o$ yielding an operation in the domain $F( D)$. In
particular, $F( D)( \epsilon)$ is a decision function for the objects which we
want to be in the carrier of $F( D)$. Also, normally, one will think of
any operation $F( D)( o)$ to be reasonably applied only to objects in the
carrier of $F( D)$, i.e. objects for which $F( D)( \epsilon)$ yields
``True''.

For clarifying notation, let us first give a trivial example: We define a
functor $F$ that, for any given domain $D$ with any operations $o$ defines the
Cartesian product. Staying within higher order predicate logic, this
functor could be defined as follows:

\begin{tabbing}
space \= space \=  space \= \kill
   \>$F( D) :=$ the $N$ such that\\
    \>\>$\forall d_1, d_2\;\;
     \langle d_1, d_2 \rangle \epsilon_N  :\Longleftrightarrow
         d_1 \epsilon_D \wedge d_2 \epsilon_D,$ \\
     \>\>$\forall o, d_1, d_2, e_1, e_2\;\;
     \langle d_1, d_2 \rangle o_N \langle e_1, e_2 \rangle  :=
       \langle d_1 o_D e_1, d_2 o_D e_2 \rangle.$
\end{tabbing}

Instead, we introduce a new quantifier ``Functor'' that binds $N$ and also
the other quantified variables that appear in the above definition so that
the following definition can be seen as nothing else than an abbreviation of
the above definition:

\begin{tabbing}
space \= space \=  space \= \kill
   \>$F( D_.) :=$ \\
    \>Functor $( \langle N, d_1, d_2, e_1, e_2, o \rangle,$ \\
     \\
    \>\>$\langle d_{1.}, d_{2.} \rangle \epsilon_N  :\Longleftrightarrow
         d_1 \epsilon_D \wedge d_2 \epsilon_D;$ \\
      \>\>$\langle d_{1.}, d_{2.} \rangle o_{.N} \langle e_{1.}, e_{2.}
        \rangle  :=
       \langle d_1 o_D e_1, d_2 o_D e_2 \rangle;$ \\ \\
       \>\>$N$\\
       \> \>$).$
\end{tabbing}

Note that, at certain places, we use a dot after a symbol as a notation
for declaring the symbol to be a variable and not a constant. The
respective convention is an adaptation  to the syntax of Mathematica
 and has no deeper
relevance. Note, in
particular, that ``$o$'' is a variable in this definition. Thus, the
definition applies to any operator $o$ in the ``signature'' of $D$.
We could define the signature of a domain explicitly. We omit this in
order not to overload the presentation in this expository paper.


Now, as a matter of fact, the construct ``Module'' of Mathematica, if
restricted to algorithmic operations, has exactly the semantics of the
``Functor'' construct as defined above. Thus, when restricted to
algorithmic functors, application of this construct yields executable code
in Mathematica.

\subsection{An Example of a Non-Algorithmic Functor}

We define a functor that ``constructs'' the residue class domain of a
domain $D$ that is equipped with a binary operator ``$\sim$'' (which
normally will be a congruence relation):

\begin{tabbing}
space \= space \=  space \= \kill
   \>Residue-Domain$( D_.) :=$ \\
    \>   Functor$( \langle R, r, s, d, e, o, C \rangle,$ \\
            \\
     \> \> $r_. \ \epsilon_R :\Longleftrightarrow
           \exists d \ \epsilon_D  \  ( r = C( d));$\\



      \> \> $r_. \  o_{.R} \ s_.  := C( {\rm Choose}( r) \ o_D \
         {\rm Choose}( s));$ \\
          \\
       \> \> $C( d_.) := \{ e \mid e \  \epsilon_D \ \wedge \ e
\sim_D  d \};$\\
       \\
       \> \> $ R$ \\
       \> \>$).$
\end{tabbing}

This functor is non-algorithmic in many respects. First, for defining
whether or not an object $r$ is in the residue domain $R$, we need
the existential quantifier: $r$ is in the carrier of $R$ iff there
exists a $d$ in the given domain $D$ such that $r$ is the residue
class of $d$. Second, for the
definition of the residue class $C( d)$ of a given $d$ we need the
set quantifier. And, finally, for defining the result of applying the
operation $o$ in $R$ to the two residue classes $r$ and $s$ we need
the ``Choose'' function that chooses one element from the argument
set.

In many areas of mathematics, non-algorithmic functors are the best
one can do for solving very general problems. For the above functor,
one can at least prove that if $D( \sim)$ is a congruence the residue
domain of $D$ has ``similar'' properties as $D$ and, in addition, may
have some new desirable properties, namely that certain objects exist
that  solve some  problem at hand.

In a concrete situation it may be a trivial, an easy, a non-trivial,
a very difficult, or an impossible task to come up with an {\em
algorithmic} functor that constructs a domain which is isomorphic to
the domain constructed by the above {\em non-algorithmic} functor.


\subsection{An Example of an Algorithmic Functor}

In contrast to the previous functor, the following functor is
algorithmic and, under certain conditions, constructs a domain which
is isomorphic to a residue domain. For this functor we suppose that
$D$ is equipped with a unary operator $\sigma$ (which normally will
be a ``canonical simplifier'' for the congruence $D( \sim)$):

\begin{tabbing}
space \= space \=  space \= \kill
   \>Simplified-Domain$( D_.) :=$ \\
    \>   Functor$( \langle S, o, s, t \rangle,$ \\
            \\
     \> \> $s_. \ \epsilon_S  :\Longleftrightarrow
        s \epsilon_D \ \wedge  \  \sigma_D( s) = s;$\\



      \> \> $s_. \  o_{.S} \ t_.  := \sigma_D( s \ o_D \ t);$ \\
           \\
       \> \> $ S$ \\
       \> \>$).$
\end{tabbing}

This functor is algorithmic in the sense that, if all the operations
of $D$ are algorithmic, then also all the operations in $S$ are
algorithmic, i.e. the functor ``preserves'' computability.  First, in
order to determine whether a given $s$ is in the carrier of $S$, we
only have to check whether $s$ is in $D$ and whether $D( \sigma)$,
the function associated with the operator $\sigma$ in $D$, applied to
$s$ is identical to $s$. Hence, under the assumption that $D(
\epsilon)$ and $D( \sigma)$ are algorithmic functions, this is an
algorithmic process. Similarly, under the assumption that $\sigma_D$
and $o_D$ are algorithmic, also $o_S$ is algorithmic.

The main theorem which one can prove about the functor
``Simplified-Domain''  is the fact that, if $\sigma_D$ is a
``canonical simplifier'' w.r.t. $\sim_D$ then the Simplified-Domain$(
D)$ is isomorphic to Residue-Domain$(D)$. In fact, the function $C$
defined locally in the functor Residue-Domain is an isomorphism.

Of course, these two functors are pervasive in mathematics and the
construction of algorithmic canonical simplifiers is one of the main
methods for turning an inconstructive part of mathematics into a
constructive one. Finding canonical simplifiers can be trivial, easy,
non-trivial, difficult, or shown to be non-existent. For example, for
the residue domain modulo 3, it is trivial to find a canonical
simplifier. Just take

\[\sigma_Z \ z_. :=  Mod( z, 3).\]

\noindent If we now call

 \[Z3 = {\rm Simplified}-{\rm Domain}\ ( Z)\]

\noindent then, for example, entering

\[2  \ o_{Z3}  \ 2\]

\noindent evaluates to

\[ 1.\]

For the residue domain of a multivariate polynomial ring modulo a
polynomial ideal, as another example, the construction of a canonical
simplifier is non-trivial (and it had been conjectured to be
algorithmically unsolvable for quite some years) and needs the theory
of Groebner bases. If $P$ is some polynomial domain (over field
coefficients or other suitable coefficient domains) and $F$ is a
(finite) set of polynomials in $P$,

\[\sigma_P \  p_. := {\rm Normal}-{\rm Form} \ ( p, {\rm
Groebner}-{\rm Basis} \ (F))\]

\noindent is a canonical simplifier for the residue domain of $P$
modulo the ideal generated by $F$ and

\[Q = {\rm Simplified}-{\rm Domain} \ ( P) \]

\noindent constructs an algorithmic isomorphic realization of this
residue domain.

Note that the above sequences of statements are not only a
mathematical description of the construction but are {\em executable}
code in our system based on Mathematica. This is so mainly because of
the fact that (the innermost kernel of) Mathematica is nothing else
than an implementation of the equational part of higher order logic
without extensionality and because of the following two features of
Mathematica:

\begin{itemize}
\item Mathematica allows Currying. Thus, it is perfectly possible to
handle terms like ``$D( o)( s, t)$''.
\item The ``Module'' construct of Mathematica has exactly the semantics of
the above ``Functor'' construct and, in fact, one can
teach Mathematica the Functor construct by just defining ``Functor =
Module''.
\end{itemize}

Of course, the functor construct is available also in a few other
programming languages, notably in ML. However, in the above
realization, Functor is much more flexible because it allows one to
define (decision predicates for) arbitrary carrier sets. Also, the
above realization of the functor concept is smoothly embedded into a
full-fledged computer algebra system with its practical computational
power. Unfortunately, neither the fact that Mathematica is
essentially higher order equational logic nor the fact that Currying
is allowed and Module can be used as Functor, is explicitly mentioned
or observed anywhere in the manual (Wolfram 89) nor in the rich
literature on Mathematica. One may also add that, surprisingly, the
above implementation of the functor principle in Mathematica is quite
efficient: Generating code for the operations in a domain by functors
of the above kind is hardly slower than hand-coding the operations
for a particular domain. The only practical disadvantage of the above
realization of functors is that the tracing and debugging facilities
of Mathematica, of course, are not tailored for this particular way
of structuring code for towers of domains. Anyway, with some
experience, it is satisfactorily possible to use the existing
debugging tools of Mathematica for debugging mathematical software
written in the functor style.


\section{Overcoming the Proof Gap}

At present, nearly no proving capabilities are available in general  
computer algebra systems. The ``directed'' equational proving  
capabilities of Mathematica are normally used only for computation.  
Sophisticated special provers, as for example Collins' prover for the  
theory of real closed fields, see (Collins 1975) and the collection of  
articles on his algorithm in Vol.5/1-2 of the Journal of Symbolic  
Computation, are stand-alone systems. 


As a first step for combining algebra and logic on the system level,  
one should of course make these special provers available from within  
general computer algebra systems like Mathematica. This is not really  
a problem any more because we can use the MathLink facility for  
accessing independent systems. Thus, if we encounter a formula like

\[ \forall x \in {\bf R} \ \exists y \in {\bf R}  \ ( y^2 = x) \]

\noindent we should be able to call Collins' algorithm from within  
Mathematica and obtain the answer

\[ {\rm False}.\]

\noindent  Similarly, if we encounter 


\[ x \in {\bf R} \ \wedge \  \exists y \in {\bf R} \ ( y^2 = x) \]

\noindent a call to Collins' algorithm would yield the equivalent  
quantifier-free formula

\[ x \in {\bf R} \wedge x \geq 0.\]

\noindent Note that Collins' algorithm goes far beyond the present  
``simplification capabilities'' in ordinary computer algebra systems  
and, hence, the available of this and other sophisticated special  
provers will greatly expand the potential of these systems.

Similarly, at present, universal theorem provers are not smoothly  
linked to computer algebra systems. Of course, it is very much  
desirable to have access to universal theorem provers, notably of the  
natural deduction type, from within computer algebra systems. For  
example if, in the development of some piece of mathematics, say in a   
``computerized'' text book, we want to prove that

\[\sim {\rm \ is \ an  \ equivalence  \ on \ } S  \Longrightarrow
     S/\sim  {\rm \ is \ a \ partition  \ on \ } S \]

\noindent then, given the present state of proving technology, it  
should be possible to produce the proof of this proposition  
automatically and to print the proof out in a way that closely  
resembles a proof generated by a human. In fact, the proof of such  
theorems hardly needs any special trick nor intuition and can  
basically be done by ``expanding'' the definition using the natural  
deduction rules for quantifiers and propositional connectives plus  
some ``simplification'', i.e.\ manipulation of quantifier-free terms  
and atomic formulae. Thus, given a proposition of the above type, we  
would wish to be able to call a natural deduction prover from within  
a computer algebra system and would expect that it produces just the  
answer 


\[{\rm True}\]

\noindent or, with the option ``verbose'', the answer

\begin{verbatim}
    Let ~ be an equivalence on S. 

    By the definition of S\~ we have to show that
    ...
\end{verbatim} 


It seems that one major obstacle that still makes this desire  
unrealistic is the fact that
\begin{itemize}
\item mathematical knowledge must be well organized so that, in a given  
proof situation, only relevant knowledge and all relevant knowledge  
is available and
\item in a given area of mathematics, in addition to the universal  
natural deduction proof techniques,  relevant special proof  
techniques should be available.
\end{itemize}

One of the main points I would like to make in this paper is that I  
think that the functor principle is not only crucial for structuring  
mathematical knowledge and mathematical methods (including  
algorithms) but it is also the key for structuring proof techniques.   
Namely, the first part of any functor in the above realization is a  
definition of the elements in the carrier by describing its  
characteristic function (which is algorithmic in the case of  
algorithmic functors). The structure of the description of this  
characteristic function naturally suggests a special prover for  
properties of the objects in the domain generated by the functor. For  
example, if the characteristic function is described inductively, a  
corresponding inductive proof technique is naturally connected with  
the functor. If the characteristic function is defined using set  
braces then the usual set-theoretic proof techniques will naturally  
apply, etc.

We give an example which is trivial (sorry for that!) but,  
nevertheless, is surprisingly powerful: We take the parameterless  
functor that defines one particular realization of the natural  
numbers and define addition in the resulting domain:

\begin{tabbing}
space \= space \=  space \= \kill
   \>Natural-Numbers$( ) :=$ \\
    \>   Functor$( \langle N, n, m \rangle,$ \\
            \\
   \>\> $0  \ \epsilon_N :\Longleftrightarrow {\rm True};$ \\
  \>\> $s( n_.) \ \epsilon_N :\Longleftrightarrow  n \  \epsilon_N$;  
\\
  \> \> $n_.  \epsilon_N :\Longleftrightarrow  {\rm False};$\\
       \\
    \> \>$n_. +_N 0 := n;$ \\
     \> \>$n_. +_N s( m_.) := s( n +_N m);$\\
           \\
       \> \> $ N$ \\
       \> \>$).$
\end{tabbing}

\noindent Here, ``0'' and ``$s$'' are ``arbitrary but fixed  
constants''. The third clause in the inductive definition of the  
``$\epsilon_N$'' predicate is a clause that handles,  the default  
case of any objects not having the format ``$s( s( ... s( 0)))$''.  
This is possible since Mathematica treats the clauses in equational  
inductive definitions successively.

Now we describe, in Mathematica,  a simple inductive prover that can  
handle formulae of the form

\[  \forall x_1 \forall x_2 \ldots \forall x_n  \ l( x_1, \ldots,  
x_n) =
    r( x_1, \ldots, x_n)  \]

\noindent where ``$l$'' and ``$r$'' are terms containing the free  
variables ``$x_1$'', $\ldots$, ``$x_n$''. The structure of the prover  
naturally reflects the induction scheme by which the above  
characteristic function for the natural numbers in the  
0/$s$-representation is defined. In fact, at a higher level of the  
system, provers of this kind could be automatically generated from  
the inductive definition of the respective characteristic function.  
The prover proceeds by, first, trying to prove the formula by  
equational simplification. If this fails, ``$x_1$'' is taken as the  
induction variable. The base case for this induction is generated  
and, again, a proof by simplification is attempted. If it fails,  
recursively, an induction over ``$x_2$'' (with ``$x_1$'' replaced by  
0) is started. If it succeeds, the induction hypothesis and the  
formula to be proved in the induction step for (arbitrary but fixed)  
``$x_1$'' are generated and a proof by simplification is attempted.  
If it fails, recursively, an induction over ``$x_2$'' (with ``$x_1$''  
arbitrary but fixed) is started. If it succeeds we are done.

In Mathematica (with Version 2.2 syntax), this recursive induction  
prover can be described in a few lines:

\begin{verbatim}
     ProofByInduction[ 

       (* of the *) equality_,
       (* w.r.t. the induction variables *) { v1_, v2___},
       (* using the *) equalities_] :=
   

       ProofByInduction0[ equality, { v1, v2}, { }, equalities]
    

     ProofByInduction0[ equality_, { v1_, v2___}, 

         (* arbitrary but fixed *) { w1___}, 

         equalities_] :=
     Module[ 

        { ... (* local variables *)},
   

         equalitySimplified = equality //. equalities;
         

         If[ LeftHandSide[ equalitySimplified] === 

                RightHandSide[ equalitySimplified],
             Return[ True]
             ];
         

         equality0 = equality /. v1 -> 0; 

         equality0Simplified = equality0 //. equalities;
         inductionHypothesis = 

              Generalized[ LeftHandSide[ equality], { v1, w1}] ->         

                  RightHandSide[ equality];
         equalitiesForInductionStep = 

              Append[ equalities, inductionHypothesis];
         equalitySv1 = equality /. v1 -> s[ v1];
         equalitySv1Simplified = 

              equalitySv1 //. equalitiesForInductionStep;
         

         inductionBasisProved = False;
         inductionStepProved = False;
          

         If[  LeftHandSide[ equality0Simplified] === 

                  RightHandSide[ equality0Simplified],
              inductionBasisProved = True
              ];
         If[  LeftHandSide[ equalitySv1Simplified] === 

                   RightHandSide[ equalitySv1Simplified],
              inductionStepProved = True
              ];
         

         If[  ! inductionBasisProved,
              inductionBasisProved =
                  ProofByInduction0[ 

                     equality0Simplified, 

                     { v2}, { v1, w1}, equalities
                     ]
                   ];
                   

         If[  ! inductionStepProved,
               inductionStepProved =
                  ProofByInduction0[ 

                      equalitySv1Simplified, 

                      { v2}, { v1, w1}, 

                      equalitiesForInductionStep, 

                      ]
                   ];
          

          inductionBasisProved && inductionStepProved
          ]
         

    ProofByInduction0[ 

       equality_, {}, { w1___},  equalities_, options___
       ] := False
\end{verbatim}

\noindent In this description of the recursive induction prover we  
left out all the lines for printing the proof. The prover is so  
simple that it hardly needs an explanation. ``Generalized'' is a  
procedure that replaces a universally quantified variable by an  
``arbitrary but fixed constant''. ``/.'' is the Mathematica operator  
for applying, once, rewrite rules (i.e.\ directed equalities) to  
terms. ``//.'' is repeated application of ``/.'' until the term does  
not change any more. Correspondingly, as a technical detail, the  
equalities that constitute the inductive definitions of operations  
like, for example, ``$+$'' must be presented in the form of  
``rules''. For example, if we want to apply the prover to the domain  
generated by the above functor, we must extract the defining  
equalities from the functor so that they are available, say, as the  
value of some constant ``NN'', which (in Version 2.2 syntax) could be  
done by an instruction of the kind

\begin{verbatim}
     NN = 

       { sum[ x_, 0]] :> 0, 

         sum[ x_, s[ y_]] :> s[ sum[ x, y]]}
\end{verbatim}

\noindent Now, if we enter

\begin{verbatim}
     ProofByInduction[
        sum[ x, sum[ y, z]] == sum[ sum[ x, y], z],
        { x, y, z},
        NN
        ]
\end{verbatim}


\noindent we obtain the following inductive proof of the  
associativity of addition over the natural numbers:

\begin{verbatim}
Simplification proof of:
for all( x, y, z, ( ( x + ( y + z)) = ( ( x + y) + z))).
------------------------------------
 

 . .Simplification of left-hand side:
 . .( x0 + ( y0 + z0))
 

 . .Simplification of right-hand side:
 . .( ( x0 + y0) + z0)
Not proved  by simplification.
 

Induction proof of: 

for all( x, y, z, ( ( x + ( y + z)) = ( ( x + y) + z))).
Induction variable: x.
******************************
 

 .Prove induction basis (i. e. formula with x -> 0):
 .for all( y, z, ( ( 0 + ( y + z)) = ( ( 0 + y) + z))).
 .Simplification proof of:
 .for all( y, z, ( ( 0 + ( y + z)) = ( ( 0 + y) + z))).
 .------------------------------------
 

 . . .Simplification of left-hand side:
 . . .( 0 + ( y0 + z0))
 

 . . .Simplification of right-hand side:
 . . .( ( 0 + y0) + z0)
 .Not proved  by simplification.
 

 .Induction proof of: 

 .for all( y, z, ( ( 0 + ( y + z)) = ( ( 0 + y) + z))).
 .Induction variable: y.
 .******************************
 

 . .Prove induction basis (i. e. formula with y -> 0):
 . .for all( z, ( ( 0 + ( 0 + z)) = ( ( 0 + 0) + z))).
 . .Simplification proof of:
 . .for all( z, ( ( 0 + ( 0 + z)) = ( ( 0 + 0) + z))).
 . .------------------------------------
 

 . . . .Simplification of left-hand side:
 . . . .( 0 + ( 0 + z0))
 

 . . . .Simplification of right-hand side:
 . . . .( ( 0 + 0) + z0)
 . . . . = ( 0 + z0)
 . .Not proved  by simplification.
 

 . .Induction proof of: 

 . .for all( z, ( ( 0 + ( 0 + z)) = ( ( 0 + 0) + z))).
 . .Induction variable: z.
 . .******************************
 

 . . .Prove induction basis (i. e. formula with z -> 0):
 . . .for all( ( ( 0 + ( 0 + 0)) = ( ( 0 + 0) + 0))).
 

 . . . .Simplification of left-hand side:
 . . . .( 0 + ( 0 + 0))
 . . . . = ( 0 + 0)
 . . . . = 0
 

 . . . .Simplification of right-hand side:
 . . . .( ( 0 + 0) + 0)
 . . . . = ( 0 + 0)
 . . . . = 0
 . . .Proved induction basis with z -> 0.
 

 . . .Let z0 be arbitrary but fixed.
 . . .Induction hypothesis (i. e. formula with z -> z0):
 . . .for all( ( ( 0 + ( 0 + z0)) = ( ( 0 + 0) + z0))).
 

 . . .Prove induction step formula (i. e. formula with z -> 

 

  z0'):
 . . .for all( ( ( 0 + ( 0 + z0')) = ( ( 0 + 0) + z0'))).
 

 . . . .Simplification of left-hand side:
 . . . .( 0 + ( 0 + z0'))
 . . . . = ( 0 + ( 0 + z0)')
 . . . . = ( 0 + ( 0 + z0))'
 . . . . = ( ( 0 + 0) + z0)'
 . . . . = ( 0 + z0)'
 

 . . . .Simplification of right-hand side:
 . . . .( ( 0 + 0) + z0')
 . . . . = ( ( 0 + 0) + z0)'
 . . . . = ( 0 + z0)'
 . . .Proved induction step formula with z -> z0'.
 . .Proved by induction over z.
 . .Proved induction basis with y -> 0.
 

 . .Let y0 be arbitrary but fixed.
 . .Induction hypothesis (i. e. formula with y -> y0):
 . .for all( z, ( ( 0 + ( y0 + z)) = ( ( 0 + y0) + z))).
 

 . .Prove induction step formula (i. e. formula with y -> y0'
 

  ):
 . .for all( z, ( ( 0 + ( y0' + z)) = ( ( 0 + y0') + z))).
 . .Simplification proof of:
 . .for all( z, ( ( 0 + ( y0' + z)) = ( ( 0 + y0') + z))).
 . .------------------------------------
 

 . . . .Simplification of left-hand side:
 . . . .( 0 + ( y0' + z0))
 

 . . . .Simplification of right-hand side:
 . . . .( ( 0 + y0') + z0)
 . . . . = ( ( 0 + y0)' + z0)
 . .Not proved  by simplification.
 

 . .Induction proof of: 

 . .for all( z, ( ( 0 + ( y0' + z)) = ( ( 0 + y0') + z))).
 . .Induction variable: z.
 . .******************************
 

 . . .Prove induction basis (i. e. formula with z -> 0):
 . . .for all( ( ( 0 + ( y0' + 0)) = ( ( 0 + y0') + 0))).
 

 . . . .Simplification of left-hand side:
..........
\end{verbatim} 


In many more lines, the proof works its way completely automatically  
through the recursion over the variables. Finally, it will return  
through all levels so that the last few lines look like this:

 

 \begin{verbatim}
 . . . .Simplification of left-hand side:
 . . . .( x0' + ( y0' + z0'))
 . . . . = ( x0' + ( y0' + z0)')
 . . . . = ( x0' + ( y0' + z0))'
 . . . . = ( ( x0' + y0') + z0)'
 . . . . = ( ( x0' + y0)' + z0)'
 . . . .Simplification of right-hand side:
 . . . .( ( x0' + y0') + z0')
 . . . . = ( ( x0' + y0') + z0)'
 . . . . = ( ( x0' + y0)' + z0)'
 . . .Proved induction step formula with z -> z0'.
 . .Proved by induction over z.
 . .Proved induction step formula with y -> y0'.
 .Proved by induction over y.
 .Proved induction step formula with x -> x0'.
Proved by induction over x.
\end{verbatim}

Of course, the crucial simplifications steps in the proof are exactly  
the ones that would be produced by the well-known test case method, see for
example (Kapur {\em et al.} 1991).  
However, it is interesting that this prover evolves from a completely  
natural approach that does nothing more than reflecting the inductive  
definition of the particular representation of the natural numbers,  
it also allows to produce a natural language easy verbose  
presentation of the proof and it gets along without any human  
interaction. Most importantly, this prover is fully integrated and in  
fact programmed in the language of a full-fledged computer algebra  
system and can hence be used in intimate interaction with  
computation. It also should be mentioned that, of course, the  
sequence of the universally quantified variables may drastically  
influence the length of the proof. This is a phenomenon that has  
often been reported in the literature. In fact, in the above example,  
considering the variables in the order ``$z$'', ``$y$'', ``$x$''  
produces a very short proof that succeeds in the simplest possible  
way. This is of course supported by the heuristics that the variable  
which is the induction variable in the inductive definition of the  
functions involved should also be treated first in an inductive  
proof. In more complicated examples, the proof may be stuck at  
certain points producing an equality which is ``not yet known''. Such  
equalities are often the appropriate guess for a lemma that should be  
proved (by the above prover) before the main proof can be attempted  
once more. In fact, this side step can be called automatically so  
that quite impressive proofs can be handled completely automatically.  
More details can be found in the preliminary report (Buchberger 1995).

\section{Conclusion}

In this paper we argued that the combination of the potential of  
computer algebra and logic systems is the next natural step for  
enhancing the problem solving power of ``symbolic computation''  
systems. For closing the gap between the ``ideal'' future system and  
the systems available at present we suggested to start from a  
computer algebra system and to add logic and, in particular, proving  
power. For quite a few reasons which we discussed in some detail,  
Mathematica seems to be particularly appealing as a starting point  
for such an approach. We tried to illustrate that the functor view  
seems to be crucial for structuring mathematical knowledge,  
mathematical methods (including algorithms) and mathematical proofs  
in  future symbolic computation systems. Thus, the implementation of  
a well designed system of basic and advanced functors (encompassing  
both the computation and the prover details for each functor) is the  
essence of building up a future system. Currently, at the RISC  
institute, we work on a project that elaborates the details  of the  
approach described in this paper.

{\bf Acknowledgement}: This paper was written in the frame of a  
research contract with Fujitsu Labs, Numazu, Japan.

\section*{References}

(Andrews 1986) P.B. Andrews: {\em An Introduction to Mathematical Logic and  
Type Theory: To Truth Through Proof}. Academic Press, London.

\noindent (Buchberger 1985) B. Buchberger: Groebner Bases: An Algorithmic  
Method in Polynomial Ideal Theory. Chapter 6 in: {\em  
Multidimensional Systems Theory}, (N.K. Bose ed.). D. Reidel  
Publishing Company, Dordrecht.

\noindent (Buchberger 1995) B. Buchberger: Induction Proofs in Equational Logic:  
A Case Study Using Mathematica. {\em Internal Technical Report}, The  
RISC Institute,
A4232 Schloss Hagenberg, Austria.

\noindent (Collins 1975) G.E. Collins: Quantifier Elimination for Real Closed  
Fields by Cylindrical Algebraic Decomposition. Proceedings of the  
Second GI Conference on Automata Theory and Formal Languages. {\em  
Lecture Notes in Computer Science}, {\bf 33}, pp. 515-532, Springer,  
Heidelberg.

\noindent (Constable 1995) R. Constable: {\em The Nuprl System}. Lecture Notes  
of the Summer School on {\em Logic of Computation}, Marktoberndorf  
1995. Edited by Institut f{\"u}r Informatik, Technische  
Universit{\"a}t M{\"u}nchen.

\noindent (Huet 1995) G. Huet: {\em The CIC System}. Lecture Notes of the  
Summer School on {\em Logic of Computation}, Marktoberndorf 1995.  
Edited by Institut f{\"u}r Informatik, Technische Universit{\"a}t  
M{\"u}nchen.

\noindent (Kapur {\em et al.} 1991) D. Kapur, P. Narendran, H. Zhang:  Automating Inductionless Induction using 
Test Sets, {\em Journal of Symbolic Computation}, Vol. 11, No. 1\&2, February
1991, pp. 83-111.

\noindent (Soiffer 1995) N. Soiffer: {\em Mathematical Typesetting in  
Mathematica}. Proceedings of the ISSAC 1995 Conference, pp. 140-149.

\noindent (Wolfram 1988) S. Wolfram: {\em Mathematica: A System for Doing  
Mathematics by Computers}. Addison-Wesley Publishing Company,  
Redwood. 

\end{document}


