\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}