%\documentstyle[a4]{article}
\documentclass{article}
\usepackage{a4}

\def\marginlineno#1{\strut\llap{\rlap{\footnotesize #1}\hskip 2.5em}}
\def\lineref#1#2{ ({\rm line #1\/})#2}
\def\linerange#1#2#3{ ({\rm lines #1--#2\/})#3}
\def\alt{'}
\def\markhere{$\times$}
\def\twolinedisplay#1#2{\dimen0=\hsize\advance\dimen0 by -2.4pt
{\hbox to\dimen0{$\displaystyle#1\hfill$}\atop\displaystyle\hfill#2}}


\title{Conditional Computing\\
{\Large (what proof checking needs from computer algebra)\\}}
\author{Freek Wiedijk\\
Nijmegen University\\
{\tt <freek@cs.kun.nl>}}
\date{}

\begin{document}
\maketitle

\begin{abstract}\noindent
We show that current computer algebra systems are not suitable for use in proof
checking, because they don't answer the right kind of question.  By analyzing the
calculations from a sample formalization, we find that calculations as they occur in proof
checking make use of results of previous calculations ({\em conditions\/}). 
We list a number of such conditional calculation problems and argue that because of
these conditions, current computer algebra packages like Maple and Mathematica are not
able to solve them.
\end{abstract}


\section{Introduction}

The discipline of {\em proof checking\/} is about encoding mathematics inside a computer
in such detail that the computer can check its correctness.  Such a `computer proof' can be
guaranteed to be free of mistakes, and because it contains all the details of
the mathematics there will be no
room for ambiguity.  However, coding all the details of a mathematical development inside
a computer tends to get very tedious because all the steps have to be entered in full detail.
Hence, automation is needed.
One particular area where one would like to have computer assistance
is the formalization of calculations.

Mathematics consists of two quite different kinds of activity.  On the one
hand there is {\em calculating,} and on the other hand there's {\em reasoning\/}
(defining notions and proving propositions.)  The experience with proof assistants is
that it's much less work to formalize reasoning than it is to formalize calculation.

The field of {\em computer algebra\/} is about making the computer do symbolic calculations.
So the natural thing would be to have a computer algebra system fill in the
details of the calculations.  However, this turns out to be more difficult than
one would expect.  We propose an explanation why this is the case (with a number of examples.) 

There already are a number of reasons (which are reasonably well accepted) why the current generation
of computer algebra packages aren't very suitable to be interfaced to proof
checkers/theorem provers:
\begin{itemize}
\item Computer algebra systems (like Mathematica and Maple)
are semantically very sloppy \cite{bee:95}.
It is easy to derive nonsensical equations from them.  Even when just trying to use them
to get {\em answers,}
one is occasionally bitten by this.
\item Computer algebra systems don't know much about logic, so for problems that need {\em reasoning\/}
(most problems) they're not adequate.
\item Computer algebra systems just produce answers and no proofs.  Hence, they can't
be used to find out {\em why\/} a certain answer is what it is.
\item Computer algebra systems are focused on {\em evaluation\/} instead of on {\em verfication.}
So, it is not so easy to use them to verify equations that are given beforehand.
\end{itemize}
However, we here try to make a different point:
\begin{itemize}
\item Computer algebra systems are not designed to calculate when there are given equations
({\em conditions\/}) that have to be used to be able to get to the answer.
\end{itemize}
Note that this point is not about logic (the conditions are just a list of equalities
and inequalities, without logical structure) and also that it is not about the difference between evaluation and verification
(unconditional verification of equations is not very useful to solve problems involving conditions.)

To give a characteristic example, suppose that (in a proof of the irrationality of $\sqrt{2}$) we are given that:
$$\sqrt{p}={m\over n}$$
and that we need to establish that:
$$m\cdot m=p\cdot n^2.$$
Now a calculation that proves this is:
$$m\cdot m=\left({m\over n}\right)^2\cdot n^2=(\sqrt{p})^2\cdot n^2=p\cdot n^2.$$
We could do the first and the third steps of this calculation in a computer algebra system.  However,
the way this calculation is structured -- to make it possible to apply the given equation --
can {\em not\/} be found by a computer algebra system.  This is not satisfactory, as the idea of
interfacing to a computer algebra system is that we do not want to have to think about calculations like
this at all.

The point of this note is that this situation is typical, and that it is the primary reason why it is
difficult to use computer algebra systems from proof checkers and theorem provers.


\section{A Small Mizar Article}

Consider the following proof (taken from \cite{wie:99:0}, line numbers added for reference),
which is a Mizar%
\footnote{There is no good reference for the current version of the Mizar system, which
is a very nice proof checker by Andrzej Trybulec from Poland.  For
instance, it doesn't have a reference manual: only \cite{muz:93} comes close, and
it is rather hard to understand.  In \cite{wie:99:1} we give a brief impression of Mizar.
The website for the Mizar project is {\tt <http://www.mizar.org/>}.}
version of the classic proof of the irrationality of $\sqrt{2}$.
\begin{verse}
\verb| reserve m, m1, n, n1, p for Nat;|\\
\verb| reserve i, i1 for Integer;|\\
\medskip
\verb|theorem T1:|\\
\verb| p is prime implies |$\surd$\verb|p is irrational|\\
\marginlineno{{\hskip.5em}5}\verb|proof|\\
\verb| assume H1: p is prime;|\\
\verb| then H2: p>1 by INT_2:def 5;|\\
\verb| then H3: p>0 by AXIOMS:22;|\\
\verb| assume |$\surd$\verb|p is rational;|\\
\marginlineno{10}\verb| then consider i, n such that H4: n<>0 & |$\surd$\verb|p=i/n &|\\
\verb|   for i1, n1 st n1<>0 & |$\surd$\verb|p=i1/n1 holds n|$\,\le\,$\verb|n1|\\
\verb|  by RAT_1:25;|\\
\verb| H5: i=|$\surd$\verb|p|$\,\cdot\,$\verb|n by REAL_2:73,H4;|\\
\verb| |$\surd$\verb|p|$\,\ge\,$\verb|0 & n|$\,\ge\,$\verb|0 by SQUARE_1:87,NAT_1:18,H3;|\\
\marginlineno{15}\verb| then i|$\,\ge\,$\verb|0 by REAL_2:121,H5;|\\
\verb| then reconsider m = i as Nat by INT_1:16;|\\
\verb| H6: m|${}^2$\verb| = (|$\surd$\verb|p|$\,\cdot\,$\verb|n)|${}^2$\verb| by H5|\\
\verb|  .= (|$\surd$\verb|p)|${}^2\,\cdot\,$\verb|n|${}^2$\verb| by SQUARE_1:68|\\
\verb|  .= p|$\,\cdot\,$\verb|n|${}^2$\verb| by SQUARE_1:88,H3;|\\
\marginlineno{20}\verb| then p|$\,|\,$\verb|m|${}^2$\verb| by NAT_1:def 3;|\\
\verb| then p|$\,|\,$\verb|m|$\,\cdot\,$\verb|m by SQUARE_1:58;|\\
\verb| then p|$\,|\,$\verb|m by NAT_LAT:95,H1;|\\
\verb| then consider m1 such that H7: m=p|$\,\cdot\,$\verb|m1 by NAT_1:def 3;|\\
\verb| n|${}^2$\verb| = m|${}^2$\verb|/p by REAL_2:72,H3,H6|\\
\marginlineno{25}\verb|  .= (p|$\,\cdot\,$\verb|m1)|${}^2$\verb|/p by H7|\\
\verb|  .= p|${}^2\,\cdot\,$\verb|m1|${}^2$\verb|/p by SQUARE_1:68|\\
\verb|  .= p|$\,\cdot\,$\verb|p|$\,\cdot\,$\verb|m1|${}^2$\verb|/p by SQUARE_1:58|\\
\verb|  .= p|$\,\cdot\,$\verb|(p|$\,\cdot\,$\verb|m1|${}^2$\verb|)/p by AXIOMS:16|\\
\verb|  .= p|$\,\cdot\,$\verb|m1|${}^2$\verb| by REAL_2:62,H3;|\\
\marginlineno{30}\verb| then p|$\,|\,$\verb|n|${}^2$\verb| by NAT_1:def 3;|\\
\verb| then p|$\,|\,$\verb|n|$\,\cdot\,$\verb|n by SQUARE_1:58;|\\
\verb| then p|$\,|\,$\verb|n by NAT_LAT:95,H1;|\\
\verb| then consider n1 such that H8: n=p|$\,\cdot\,$\verb|n1 by NAT_1:def 3;|\\
\verb| n1<>0 by H4,H8;|\\
\marginlineno{35}\verb| then H9: n1>0 by NAT_1:19;|\\
\verb| then m1/n1 = (p|$\,\cdot\,$\verb|m1)/(p|$\,\cdot\,$\verb|n1) by REAL_2:55,H3|\\
\verb|  .= m/n by H7,H8|\\
\verb|  .= |$\surd$\verb|p by H4;|\\
\verb| then H10: n|$\,\le\,$\verb|n1 by H4,H9;|\\
\marginlineno{40}\verb| p|$\,\cdot\,$\verb|n1>1|$\,\cdot\,$\verb|n1 by REAL_2:199,H2,H9;|\\
\verb| then n>n1 by H8;|\\
\verb| hence contradiction by H10;|\\
\verb|end;|
\end{verse}

\noindent
In normal language this proof becomes something like this:
\begin{quote}
We are going to prove that if $p$ is a prime number then $\sqrt{p}$ is irrational\linerange{3}{5}{.}
For suppose that it is not, then $\sqrt{p}$ is rational\lineref{9}{} and can be written as a
fraction $m/n$\lineref{10}{.}  Moreover, this fraction can be chosen to be simplified, so with minimal
$n$\lineref{11}{.}

Now from $m^2 = p\cdot n^2$ we get that $m^2$ is divisible by $p$\linerange{17}{20}{}
and because $p$ is prime, this implies that $m$ is divisible by $p$\linerange{21}{22}{,}
and so we can write $m = p\cdot m\alt$\lineref{23}{.}  Then $n^2 = p\cdot{m\alt}^2$\linerange{24}{29}{}
and so for the same reasons we also can write $n = p\cdot n\alt$\linerange{30}{33}{.}
But then ${m\alt/n\alt} = {m/n}$\linerange{36}{38}{} and because $n\alt<n$
we get a contradiction with the fact that $m/n$ was simplified\linerange{39}{42}{.}

So this means that the assumption that $\sqrt{p}$ was rational
can't be true, and therefore that $\sqrt{p}$ is irrational. 
\end{quote}

\noindent
The Mizar proof itself is almost completely straight-forward.  The only unexpected element is that
the divisibility conditions have to be expressed for natural numbers, as \verb|NAT_LAT:95|, the relevant lemma in the
Mizar library:
\begin{verse}
\verb|     for i st i is prime holds|\\
\verb|for m,n holds  i |$\,|\,$\verb| m |$\,\cdot\,$\verb| n implies (i|$\,|\,$\verb|m or i|$\,|\,$\verb|n);|
\end{verse}
is (unnecessarily) restricted to natural numbers.  This explains the `cast' to a natural number
(an object of type \verb|Nat|) in line 14.


\section{Taking Out the Calculations}\label{calculations}

Now this Mizar proof contains a number of `calculations' that are rather low-level.
For instance the deduction of $n^2 = p \cdot{m\alt}^2$ (which uses the `\verb|.=|'
construction) in lines 22--27:
$$n^2 = {m^2\over p} = {(p\cdot m\alt)^2\over p} = {p^2\cdot{m\alt}^2\over p} = {(p\cdot p)\cdot{m\alt}^2\over p} = {p\cdot(p\cdot{m\alt}^2)\over p} = p\cdot{m\alt}^2$$
seems quite involved.  Apart from these calculations, the proof
is almost exactly on the level of the informal English language proof.

It seems natural to look what happens when one isolates these calculations in a
number of `calculation lemmas'.  The statements of these lemmas then turn out to be (where
\verb|m|, \verb|m1|, \verb|n|, \verb|n1| and \verb|p| are declared to be natural numbers and
\verb|i| is delared integer):
\begin{verse}
\verb|C1: n<>0 & |$\surd$\verb|p=i/n implies i|$\ge$\verb|0;|\\
\verb|C2: n<>0 & |$\surd$\verb|p=m/n implies m|$\,\cdot\,$\verb|m=p|$\,\cdot\,$\verb|n|${}^2$\verb|;|\\
\verb|C3: p>1 & m|$\,\cdot\,$\verb|m=p|$\,\cdot\,$\verb|n|${}^2$\verb| & m=p|$\,\cdot\,$\verb|m1 implies n|$\,\cdot\,$\verb|n=p|$\,\cdot\,$\verb|m1|${}^2$\verb|;|\\
\verb|C4: n<>0 & n=p|$\,\cdot\,$\verb|n1 implies n1>0;|\\
\verb|C5: n<>0 & m=p|$\,\cdot\,$\verb|m1 & n=p|$\,\cdot\,$\verb|n1 & |$\surd$\verb|p=m/n implies |$\surd$\verb|p=m1/n1;|\\
\verb|C6: p>1 & n1>0 & n=p|$\,\cdot\,$\verb|n1 implies n>n1;|
\end{verse}
With these calculations supplied, the proof of \verb|T1| becomes (where the $\times$ signs mark
the lines where the lemmas are applied):
\begin{verse}
\verb|theorem T1:|\\
\verb| p is prime implies |$\surd$\verb|p is irrational|\\
\verb|proof|\\
\verb| assume H1: p is prime;|\\
\verb| then H2: p>1 by INT_2:def 5;|\\
\verb| assume |$\surd$\verb|p is rational;|\\
\verb| then consider i, n such that H4: n<>0 & |$\surd$\verb|p=i/n &|\\
\verb|   for i1, n1 st n1<>0 & |$\surd$\verb|p=i1/n1 holds n|$\le$\verb|n1|\\
\verb|  by RAT_1:25;|\\
\marginlineno{\markhere}\verb| i|$\ge$\verb|0 by C1,H4;|\\
\verb| then reconsider m = i as Nat by INT_1:16;|\\
\marginlineno{\markhere}\verb| H6: m|$\,\cdot\,$\verb|m=p|$\,\cdot\,$\verb|n|${}^2$\verb| by C2,H4;|\\
\verb| then p|$\,|\,$\verb|m|$\,\cdot\,$\verb|m by NAT_1:def 3;|\\
\verb| then p|$\,|\,$\verb|m by NAT_LAT:95,H1;|\\
\verb| then consider m1 such that H7: m=p|$\,\cdot\,$\verb|m1 by NAT_1:def 3;|\\
\marginlineno{\markhere}\verb| n|$\,\cdot\,$\verb|n=p|$\,\cdot\,$\verb|m1|${}^2$\verb| by C3,H2,H6,H7;|\\
\verb| then p|$\,|\,$\verb|n|$\,\cdot\,$\verb|n by NAT_1:def 3;|\\
\verb| then p|$\,|\,$\verb|n by NAT_LAT:95,H1;|\\
\verb| then consider n1 such that H8: n=p|$\,\cdot\,$\verb|n1 by NAT_1:def 3;|\\
\marginlineno{\markhere}\verb| H9: n1>0 by C4,H4,H8;|\\
\marginlineno{\markhere}\verb| |$\surd$\verb|p=m1/n1 by C5,H4,H7,H8;|\\
\verb| then H10: n|$\le$\verb|n1 by H4,H9;|\\
\marginlineno{\markhere}\verb| n>n1 by C6,H2,H8,H9;|\\
\verb| hence contradiction by H10;|\\
\verb|end;|
\end{verse}
which is shorter than the original, and much more on the level of abstraction of the natural
language version.

The statements of the calculation lemmas are almost exactly determined by the way they
are used.  If one omits all quantified
conjuncts from the premisses of the lines that use them,
one gets something close to the conditions from the statement of the lemma.  For instance,
the line in which lemma \verb|C3| is used:
\begin{verse}
$\ldots$\quad\verb|n|$\,\cdot\,$\verb|n=p|$\,\cdot\,$\verb|m1|${}^2$\verb| by C3,H2,H6,H7;|\quad$\ldots$
\end{verse}
refers to:
\begin{verse}
\verb|H2: p>1;|\\
\verb|H6: m|$\,\cdot\,$\verb|m=p|$\,\cdot\,$\verb|n|${}^2$\verb|;|\\
\verb|H7: m=p|$\,\cdot\,$\verb|m1;|
\end{verse}
so the statement for that line would be:
\begin{verse}
\verb|p>1 & m|$\,\cdot\,$\verb|m=p|$\,\cdot\,$\verb|n|${}^2$\verb| & m=p|$\,\cdot\,$\verb|m1 implies n|$\,\cdot\,$\verb|n=p|$\,\cdot\,$\verb|m1|${}^2$
\end{verse}
which happens to be exactly the statement of lemma \verb|C3|.

The variables in these calculation lemmas are typed, but
this is only used for deducing that a variable \verb|n| that has type \verb|Nat| satisfies \verb|n|$\ge$\verb|0|.
Apart from this the type of the variables is not
relevant, and the lemmas could have been quantified over variables of type \verb|Real| just as well.


\section{Current Computer Algebra}

There's no easy way to verify the truth of calculation lemmas like this with current
computer algebra systems (like Macsyma, Maple \cite{mon:ged:hea:lab:vor:97} or Mathematica \cite{wol:96})
because those systems don't have a way to enter and use the conditions that have to be used in the
calculations.

(The Mathematica system can
have conditions on parameters of integrals with \verb|Assumptions|, and it can check for
conditions when applying rewrite rules with \verb|Condition|, but those mechanisms are not suitable for
the general use that we are writing about here.)

The basic mechanism most general purpose computer algebra packages use to manipulate expressions
is {\em rewriting.}
The rewrite system that it applies can be modified by the user, but it does not depend
on the expression that is being evaluated.  When one presents `condition' equations for solving
a problem, those equations somehow have to be combined with the rewrite system.  There seems no
easy way to do that, as both sides of these equations can be quite intricate, and in order to
be able to use them a lot of formula rearrangement might be necessary.  The manipulations necessary
for that strongly
depend on the shape of the condition, and are not in a form that is easily implemented by a
rewrite system.


\section{Some More Examples}\label{examples}

If we are sloppy about the `domain conditions' of partial functions
like division and square root, and omit the premisses which are only present for that,
and furthermore if we replace typing information like $n:{\rm N}$ by
inequalities like $n\ge 0$, then the calculation lemmas from section \ref{calculations}
become:
%1
$$n\ge 0\;,\; \sqrt{p}=i/n\;\vdash\; i\ge 0$$
$$\sqrt{p}=m/n\;\vdash\; m\cdot m=p\cdot n^2$$
$$p>1\;,\; m\cdot m=p\cdot n^2\;,\; m=p\cdot m\alt\;\vdash\; n\cdot n=p\cdot {m\alt}^2$$
$$n\alt\ge 0\;,\; n\ne 0\;,\; n=p\cdot n\alt\;\vdash\; n\alt>0$$
$$m=p\cdot m\alt\;,\; n=p\cdot n\alt\;,\; \sqrt{p}=m/n\;\vdash\; \sqrt{p}=m\alt/n\alt$$
$$p>1\;,\; n\alt>0\;,\; n=p\cdot n\alt\;\vdash\; n>n\alt$$
These are the kind of questions that we would like to see solved automatically. 
More examples in this format (also from \cite{wie:99:0}) are:
%2
$$x=\sqrt{2}\;\vdash\; (x^x)^x=2$$
%6
%$$\twolinedisplay{l=n-(k+1)\;,\; l\alt=n-k\;,\; {n!\over k!\,(k+1)\,(l\alt!/l\alt)}={l\alt\over k+1}\cdot{n!\over k!\,l\alt!}\;\vdash\;}
%{{n\choose k+1}={n-k\over k+1}\,{n\choose k}}$$
$$k+1\le n\;\vdash\; {n\choose k+1}={n-k\over k+1}\,{n\choose k}$$
$$n-k=0\;\vdash\; {n\choose k+1}={n-k\over k+1}\,{n\choose k}$$
$$k>n\;\vdash\; {n\choose k+1}={n-k\over k+1}\,{n\choose k}$$
%7
%$$\twolinedisplay{n^{-(k+1)}={n^{-k}\over n}\;,\; {n\choose k+1}={n-k\over k+1}\,{n\choose k}\;\vdash\;}
%{{n\choose k+1}\,n^{-(k+1)}={1\over k+1}\cdot{n\choose k}\,n^{-k}\cdot{n-k\over n}}$$
$${n\choose k+1}={n-k\over k+1}\,{n\choose k}\;\vdash\; {n\choose k+1}\,n^{-(k+1)}={1\over k+1}\cdot{n\choose k}\,n^{-k}\cdot{n-k\over n}$$
%9
$${k\over n}\ge 0\;\vdash\; \left|{n-k\over n}-1\right|={k\over n}$$
%13
%$$\twolinedisplay{\lim_{n\to\infty}\left({1\over k+1}\cdot{n\choose k}\,n^{-k}\right)={1\over(k+1)!}\;,\; \lim_{n\to\infty}{n-k\over n}=1\;\vdash\;}
%{\lim_{n\to\infty}\left({1\over k+1}\cdot{n\choose k}\,n^{-k}\cdot{n-k\over n}\right)={1\over(k+1)!}}$$
$$\lim_{n\to\infty}{n\choose k}\,n^{-k}={1\over k!}\;\vdash\; \lim_{n\to\infty}\left({1\over k+1}\cdot{n\choose k}\,n^{-k}\cdot{n-k\over n}\right)={1\over(k+1)!}$$
%20
%$$i\alt=k\;,\; l=n-k\;\vdash\; {n\choose i\alt}x^l y^{i\alt}={n\choose k}x^{n-k} y^k$$
%32
$$x=i/n\;,\; n=m+1\;\vdash\; n!\cdot x=i\cdot m!$$
%39
%$$x={1\over n+1}\;\vdash\; {n!\over(n+1)!}=x$$
$$x={1\over n+1}\;,\; {n!\over(n+k+1)!}\le x^{k+1}\;\vdash\; {n!\over(n+(k+1)+1)!}\le x^{(k+1)+1}$$
%$$x={1\over n+1}\;\vdash\; {n!\over(n+k+1)!}\le x^{k+1}$$
%41
$$n\ge 2\;,\; x={1\over n+1}\;\vdash\; {x\over 1-x}<1$$
Some of these examples might seem silly, but they actually appear naturally in the
proofs and all are quite a bit of work when doing them in Mizar.

Note that some conditions in these examples aren't informative.  For instance, the relation:
$${n\choose k+1}={n-k\over k+1}\,{n\choose k}$$
is provable without conditions too (but because $n\choose k$ is defined with a case split
on $k\le n$, it would involve doing logic, and the point of this note is that
the inability of computer algebra systems to do logic is {\em not\/} the real problem.)
Also note that conditions can be derivable, like:
$$\lim_{n\to\infty}{n\choose k}\,n^{-k}={1\over k!}$$
However, because the conditions from these example calculations
are ones that were used in the Mizar proof, we feel that an automated system also should be allowed to
refer to them.
And really, as the examples become more involved, it might be unrealistic to require a solution without
using superfluous conditions.  For instance:
$$\lim_{n\to\infty}\left({1\over k+1}\cdot{n\choose k}\,n^{-k}\cdot{n-k\over n}\right)={1\over(k+1)!}$$
is true without the condition, but maybe too difficult for an automated system to solve all by itself.
(Mathematica 3.0 isn't able to compute the left hand side of this equality and complains about `essential singularities' of the
$\Gamma$ function.)


\section{Concluding Remarks}

The balance between user intervention and automation in a proof checker/the\-o\-rem prover is a delicate
one.  If there's not enough automation present then using the system becomes very tedious, while if
there's too much automation then one is not able to control the system well enough.
Ideally one would like the `conscious' parts of a proof to be entered by the user of the system
(so that the user can keep control of the proof), while the `unconscious' parts of the proof are
handled automatically.  We feel that the kind of calculational inferences that we describe here are
of the second kind, and should be handled by an automated computer algebra system.

What this note doesn't present, and what we are looking for, is an approach for automatically doing the
conditional calculations as presented in this paper.  Once such an approach has been found,
interfacing computer algebra systems and theorem proving systems will become quite interesting.

There is a difference  between having a system decide whether an inference is true, and having
a system present a chain of calculation steps that show {\em why\/} the inference is true.
We feel that the first problem
is much harder than the second: if an algorithm can be found that determines whether a conditional
calculation problem is solvable, distilling an algorithm from it that gives an explicit solution should be
relatively easy.


\paragraph{Acknowledgements}  Thanks to Henk Barendregt, Wieb Bosma and Herman Geuvers
for valuable comments on this note.


%\bibliographystyle{plain}
%\bibliography{cc}

\begin{thebibliography}{1}

\bibitem{bee:95}
M.~Beeson.
\newblock Using nonstandard analysis to ensure the correctness of symbolic
  computations.
\newblock {\em International Journal of Foundations of Computer Science},
  6(3):299--338, 1995.

\bibitem{mon:ged:hea:lab:vor:97}
M.~Monagan, K.~Geddes, K.~Heal, G.~Labahn, and S.~Vorkoetter.
\newblock {\em Maple V Programming Guide for Release 5}.
\newblock Springer-Verlag, Berlin/Heidelberg, 1997.

\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.
\newblock URL: \verb|<http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz>|.

\bibitem{tar:51}
A.~Tarski.
\newblock {\em A Decision Method for Elementary Algebra and Geometry}.
\newblock University of California Press, Berkeley/Los Angeles, 1951.

\bibitem{wie:99:0}
F.~Wiedijk.
\newblock Irrationality of $e$.
\newblock {\em Journal of Formalized Mathematics}, 11, 1999.
\newblock MML Identifier: \verb|IRRAT_1|.

\bibitem{wie:99:1}
F.~Wiedijk.
\newblock Mizar: An impression.
\newblock Unpublished,\hfill\break URL:
  \verb|<http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz>|, 1999.

\bibitem{wol:96}
S.~Wolfram.
\newblock {\em The Mathematica book}.
\newblock Cambridge University Press, Cambridge, 1996.

\end{thebibliography}


\appendix
\section{Mathematica Syntax}

To show that the problems from section \ref{examples} involve expressions
in the domain of computer algebra, here are the same examples in the syntax
of the Mathematica system \cite{wol:96}:
\begin{verse}
{\footnotesize\verb|In[1]:=  |}\verb|Implies[n>=0 && Sqrt[p]==i/n, i>=0]|\\
{\footnotesize\verb|In[2]:=  |}\verb|Implies[Sqrt[p]==m/n, m*m==p*n^2]|\\
{\footnotesize\verb|In[3]:=  |}\verb|Implies[p>1 && m*m==p*n^2 && m==p*m1, n*n==p*m1^|\\
{\footnotesize\verb|         |}\verb|2]|\\
{\footnotesize\verb|In[4]:=  |}\verb|Implies[n1>=0 && n!=0 && n==p*n1, n1>0]|\\
{\footnotesize\verb|In[5]:=  |}\verb|Implies[m==p*m1 && n==p*n1 && Sqrt[p]==m/n, Sqrt|\\
{\footnotesize\verb|         |}\verb|[p]==m1/n1]|\\
{\footnotesize\verb|In[6]:=  |}\verb|Implies[p>1 && n1>0 && n==p*n1, n>n1]|\\
{\footnotesize\verb|In[7]:=  |}\verb|Implies[x==Sqrt[2], (x^x)^x==2]|\\
{\footnotesize\verb|In[8]:=  |}\verb|Implies[k+1<=n, Binomial[n,k+1]==(n-k)/(k+1)*|\\
{\footnotesize\verb|         |}\verb|Binomial[n,k]]|\\
{\footnotesize\verb|In[9]:=  |}\verb|Implies[n-k==0, Binomial[n,k+1]==(n-k)/(k+1)*|\\
{\footnotesize\verb|         |}\verb|Binomial[n,k]]|\\
{\footnotesize\verb|In[10]:= |}\verb|Implies[k>n, Binomial[n,k+1]==(n-k)/(k+1)*|\\
{\footnotesize\verb|         |}\verb|Binomial[n,k]]|\\
{\footnotesize\verb|In[11]:= |}\verb|Implies[Binomial[n,k+1]==(n-k)/(k+1)*Binomial[n,|\\
{\footnotesize\verb|         |}\verb|k], Binomial[n,k+1]*n^(-(k+1))==1/(k+1)*(|\\
{\footnotesize\verb|         |}\verb|Binomial[n,k]*n^(-k))*(n-k)/n]|\\
{\footnotesize\verb|In[12]:= |}\verb|Implies[k/n>=0, Abs[(n-k)/n-1]==k/n]|\\
{\footnotesize\verb|In[13]:= |}\verb|Implies[Limit[Binomial[n,k]*n^(-k),n->Infinity]=|\\
{\footnotesize\verb|         |}\verb|=1/k!, Limit[1/(k+1)*(Binomial[n,k]*n^(-k))*(n-k|\\
{\footnotesize\verb|         |}\verb|)/n,n->Infinity]==1/(k+1)!]|\\
{\footnotesize\verb|In[14]:= |}\verb|Implies[x==i/n && n==m+1, n!*x==i*m!]|\\
{\footnotesize\verb|In[15]:= |}\verb|Implies[x==1/(n+1) && n!/(n+k+1)!<=x^(k+1), n!/(|\\
{\footnotesize\verb|         |}\verb|n+(k+1)+1)!<=x^(k+1+1)]|\\
{\footnotesize\verb|In[16]:= |}\verb|Implies[n>=2 && x==1/(n+1), x/(1-x)<1]|
\end{verse}
Note that these problems don't restrict themselves to the basic set of the comparison relations
\verb|Equal|, \verb|Unequal|, \verb|Less|,
\verb|LessEqual|, \verb|Greater| and \verb|GreaterEqual| together with the basic
arithmetical operations
\verb|Plus|, \verb|Subtract|, \verb|Times| and \verb|Divide| (which is a pity, as Tarski
has shown in \cite{tar:51} that the first order theory of these operations on the real numbers is
decidable.)  Even the first examples refer to the \verb|Sqrt| operation, while
the others also refer to \verb|Power|, \verb|Factorial|, \verb|Binomial|, \verb|Abs|, \verb|Limit|
and \verb|Infinity|.


\end{document}