\def\arctanD{\underbrace{\mathop{\rm arctan}\nolimits{}}_{\mathop{\rm Derive}\nolimits}}
\def\arctanM{\underbrace{\mathop{\rm arctan}\nolimits{}}_{\mathop{\rm Maple}\nolimits}}
\def\Arccot{\mathop{\rm Arccot}\nolimits}
\def\arccot{\mathop{\rm arccot}\nolimits}
\def\eq{\mathrel{{\tt eq}}}
\def\equal{\mathrel{\hbox{\tt =}}}
\def\interval#1#2{[#1,#2]}
\def\ttinterval#1#2{\hbox{\tt[}#1,#2\hbox{\tt]}}
\def\GF{{\rm GF}}
\def\factor{{\rm factor}}
\def\trdeg{{\rm tr.deg.}}
\def\atan{{\rm atan}}
\def\deg{{\rm deg}}
\def\signum{{\rm signum}}
\def\dx{\,{\rm d}x}
\def\Z{{\bf Z}}
\def\C{{\bf C}}
\def\Q{{\bf Q}}
\def\R{{\bf R}}
\def\RR{\R\rightarrow\R}
\documentclass{llncs}
\usepackage{amsmath}
\newtheorem{Proposition}{Proposition}
\newtheorem{Definition}{Definition}
\newtheorem{Theorem}{Theorem}
\begin{document}
\title{Mathematical Knowledge Representation\\(Extended Abstract)}
\author{James H. Davenport\thanks{Partially supported by the E.U. OpenMath
Thematic Network}}
\institute{Department of Computer Science,
University of Bath, Bath BA2 7AY, England\\
\email{J.H.Davenport@bath.ac.uk}}
\maketitle
\begin{abstract}\noindent
Mathematical knowledge manipulation requires mathematical knowledge
representation. This is not as easy as it seems, and there are various
ambiguities in mathematics as commonly described. This paper describes
some of these, and, where relevant, outlines how the OpenMath Content
Dictionary mechanism can handle them. 
\end{abstract}
\section{Introduction}
Before we can talk about the ``management'' of mathematical knowledge,
we have to talk about its representation, and the problems of doing this. 
Here we discuss some of the
pitfalls that the author has encountered, ranging from the concrete to
the more philosophical (and fundamental). These are generally
described from an OpenMath \cite{OpenMath} point of view, but the majority
of the problems are inherent to the representation of mathematical knowledge,
rather than accidents of OpenMath.
\section{Exactly which $\ldots$ do you mean?}
Mathematical notation is not quite as unambiguous as we would like
(and as mathematicians like to pretend). This is a problem that
pervades much of mathematics, and we give just a couple of examples.
\begin{description}
\item[Branch cuts]Whenever a function $f$ from $\C$ to $\C$ (or
$\R\rightarrow\R$) is not injective, the inverse needs to be defined
on only a subset of $\C$ (or $\R$), typically defined by taking some
injective subset of $f$, i.e. $f$ defined on some subset of $\C$ (or
$\R$) by some ``branch cuts''. There is no fully logical way to
choosing these branch cuts, and some standard decision has to be
taken, e.g. as in \cite{AS}. These decisions are not always clear, and
many alternative choices can be justified: e.g. it is common these days to have
$-\pi<\Im\log z\le\pi$, but the author was originally taught the range
$0\le\Im\log z<2\pi$.
\par
For the inverse trigonometric and hyperbolic functions, this issue is
discussed in \cite{CDJW}. They quote the amusing example of arccot in
table 1.
% table \ref{arccottable}.
% Doesn't work: no idea why
\par\noindent
\begin{table}\label{arccottable}
\caption{value of $\arccot(-1)$ in various sources}
\begin{tabular}{llrl}
\cite{AS}&1st printing&$3\pi/4$&inconsistent\\
\cite{AS}&9th printing&$-\pi/4$\\
\cite{GR}&5th edition&?&inconsistent\\
\cite{CRC}&30th edition&$3\pi/4$&inconsistent\\
Maple&V release 5&$3\pi/4$\\
Axiom&2.1&$3\pi/4$\\
Mathematica&\cite{Mma}&$-\pi/4$\\
Reduce&3.4.1&$-\pi/4$&in floating point\\
Matlab&5.3.0&$-\pi/4$&in floating point\\
Matlab&5.3.0&$3\pi/4$&symbolic toolbox\\
\end{tabular}\end{table}
\par
The OpenMath solution to this problem is to be very explicit in the
Content Dictionaries for these functions, defining them all in terms
of the branch cut for $\log$, so that $\arccot$, as the symbol
\begin{verbatim}
<OMS name="arccot" cd="transc1">
\end{verbatim}
is defined as $\arccot(z)=\frac1{2i}\ln\left(\frac{z+i}{z-i}\right)$.
\par
There are other differences: for example Derive and Maple differ in their
definition of inverse tangents, so that
$$
\arctanD(z) =\overline{\arctanM(\overline z)}.
$$
Here the difference is only on the branch cuts, a set of measure zero, so
the difference is less likely to be noticed in testing.
\par
Of course, it would be possible to have other CDs, and the author is
contemplating writing one for the multivalued versions\footnote{The
reasons why these are not the fundamental OpenMath functions are given
in \cite{AISC}.} of these, so that
\begin{verbatim}
<OMS name="Arccot" cd="transc3">
\end{verbatim}
would be defined as $\Arccot(z)=\{w \mid \cot(w)=z\}$.
\item[Algebraic Structures]
Most algebraic structures have names, and we are generally happy
working with these --- we all know what ${\rm PSL}(3,\Z)$ is (though
some of us might write it as ${\rm PSL}_3(\Z)$, which explains some of
the difficulty of translating a presentation-oriented language such as
\LaTeX{} or MathML--presen\-tation \cite{MathML} into a content-oriented
language such as OpenMath \cite{OpenMath}). It is the OpenMath view that
there is one abstract mathematical object, say
\begin{verbatim}
<OMA>
  <OMS name="PSL" cd="lineargroups"/>
  <OMI> 3</OMI>
  <OMS name="Z" cd="setname1"/>
</OMA>
\end{verbatim}
and that whether it is rendered as ${\rm PSL}(3,\Z)$ or ${\rm PSL}_3(\Z)$
is up to the configuration of the browser, just as  the rendering of
\begin{verbatim}
<OMA>
  <OMS name="interval_oc" cd="interval1"/>
  <OMI> 3</OMI>
  <OMI> 4</OMI>
</OMA>
\end{verbatim}
as $(3,4]$ or $]3,4]$ depends on whether the browser has been configured to
produce English or French notation.
\par However, there are still several ambiguities. We all accept that
$C_6$ acts on six elements, and has size six, but what of $D_6$? Does
it act on six elements (and therefore have size 12) or have size 6
(and therefore act on three elements, and be isomorphic to $S_3$)? The
situation is described in \cite{CHM} as follows.
\begin{quotation}\noindent
A name of the form $\langle\langle X(n)\rangle\rangle$ denotes the
$n$-th member of a family as a permutation group on $n$ points. The
same group is denoted by $\langle\langle X_n\rangle\rangle$ if it
occurs as an abstract group, but not necessarily with this
action. Exceptions are dihedral and Frobenius groups, for which
traditionally the {\it size\/} is indicated by an index. Thus
$\langle\langle D(4)\rangle\rangle = \langle\langle
D_8(4)\rangle\rangle$ is the dihedral group of size 8.
\end{quotation}
However, this convention is far from universal. Furthermore, the
notational scheme described in \cite{CHM} (itself based on that in
\cite{Atlas}) can lead (inevitably) to several names for the same
group, e.g. $F_{18}(6)=[3^2]2=3\wr 2$ or
$E(8):A4=[\frac13A(4)^2]2=e(4):6$.
\par
Again, the remedy would be that of being very clear in the CDs
describing these objects, with Formal Mathematical Properties to
express (at least some of) the alternative names for groups.
\end{description}
\section{Just how constructive are we?}
For the moment, let us assume that an integral domain is a well-known
concept (though we will see later that there are problems with
this). then we can define two concepts specialising this.
\begin{description}
\item[GCD domain]An integral domain $R$ is a GCD domain if, and only if,
for any two elements $a$ and $b$ of $R$, there is an element $g$ of
$R$ such that:
\begin{enumerate}
\item $g|a$ and $g|b$;
\item if $c|a$ and $c|b$, then $c|g$.
\end{enumerate}
\item[Unique factorisation domain]An integral domain $R$ is a unique
factorisation domain if, and only if: 
\begin{enumerate}
\item any $r\in R\setminus\{0\}$ has a representation as
$u\prod_{i=1}^n p_i$, where $u$ is a unit of $R$ and the $p_i$ are
irreducible non-unit elements of $R$, i.e. divisible only by their
associates; 
\item any such representation of $r$ is unique up to re-ordering and
multiplication by units.
\end{enumerate}
\end{description}
It is well known that these two concepts are in fact identical.

However, we could ask for constructive versions of these.
\begin{description}
\item[Constructive GCD domain]A constructive integral domain $R$ is a
constructive GCD domain if, and only if, there is an algorithm which,
given any two elements $a$ and $b$ of $R$, computes an element $g$ of
$R$ such that:
\begin{enumerate}
\item $g|a$ and $g|b$;
\item if $c|a$ and $c|b$, then $c|g$.
\end{enumerate}
\item[Constructive unique factorisation domain]A constructive integral
domain $R$ is a constructive unique factorisation domain if, and only
if:
\begin{enumerate}
\item there is an algorithm which, given any $r\in R\setminus\{0\}$
computes a representation $r=u\prod_{i=1}^n p_i$, where $u$ is a unit
of $R$ and the $p_i$ are irreducible non-unit elements of $R$; 
\item any such representation of $r$ is unique up to re-ordering and
multiplication by units.
\end{enumerate}
\end{description}
As we might expect, the constructive versions are stronger than the
non-con\-structive versions. However, the two constructive versions are
different: every constructive unique factorisation domain is a
constructive GCD domain, but not {\it vice versa\/}. The example is
given in \cite{FS}. Let $\lambda_i$ be an infinite, recursively
enumerable, non-recursive sequence of elements from $\{1,-1\}$, and
let $R=\Q(\sqrt{\lambda_1},\ldots)[x]$. Then Euclid's algorithm demonstrates
that $R$ is a constructive GCD domain. However, it is not a
constructive unique factorisation domain, since the factorisation of
$x^2+1$ tells us whether (if it factors into two linears) or not (if
it is irreducible) there is a $-1$ in the sequence of $\lambda_i$,
which was assumed to be non-recursive\footnote{If one wishes to be
more formal, one lets $\lambda$ be a Kleene \cite{Kleene} function,
i.e. a recursive function defined on all positive integers which is an
injection such that $\{m:\exists n (\lambda(n)=m)\}$ is a non-recursive
class. Then let $K_m=\Q(\sqrt{x_1},\ldots)$, where $x_j={-1}$ if $j$ is
the least $n$ such that $\lambda(n)=m$, and $x_j=1$ otherwise. Then
$1+x^2$ is reducible over $K_m$ if, and only if, $\exists n
(\lambda(n)=m)$, and so an effective factorisation algorithm, or even an 
effective irreducibility test, gives us an algorithm to test membership in a
non-recursive set, a contradiction.}.
\par
This problem leads to the need for clear separation of the
constructive algebraic domains from the non-constructive ones,
probably in different CDs, so that one could distinguish
\begin{verbatim}
<OMS name="GCDdomain" cd="domain1">
\end{verbatim}
from
\begin{verbatim}
<OMS name="GCDdomain" cd="cdomain1">
\end{verbatim} 
(the latter being short for ``constructive domains'' to fit into the
eight-character limit for the names of CDs).
\section{What do we mean by Equality?}
This problem was discussed in \cite{Equality}. It was pointed out that
it is necessary to be precise about the question ``equal as what'',
since $\frac{x^2-2x+1}{x^2-1}$ and $\frac{x-1}{x+1}$ are equal as
elements of the mathematical type $\Q(x)$, but not as functions
$\Q\rightarrow\Q$, since the first is undefined at $x=1$, while the
latter yields $0$ there. In some sense this is a typing question, in that
the two expressions are equal/unequal depending on their type, but the
question is in practice more fundamental than that: do we really want a
flag on every expression that says ``a g.c.d. has been performed, therefore
you may not use {\tt eval}''?
\par
It is also necessary to distinguish between ``exactly equal'',
``approximately equal'' (meaning I have evaluated a certain number of
digits or series terms, but have no proof of equality), ``probably
equal'' (meaning I have performed some sort of Monte Carlo test, as in
\cite{Naylor} for straight-line programs \cite{FIK}, in which case one
has to ask what the probability of failure is\footnote{\cite{Naylor}
asks whether one should take an {\it a priori\/} or an {\it a
posteriori\/} approach to this. As far as the author knows, this
question has not generally been studied.}). Also does returning {\tt false}
merely mean ``I am unable to prove that they are equal'', as Maple
does with the following
\begin{equation}\label{arccos2}
\frac2i\ln\left(\sqrt\frac{1+z}2+i\sqrt\frac{1-z}2\right)
=-i\ln\left(z+i\sqrt{1-z^2}\right)
\end{equation}
example.
\par
In classical logic $(x=y)\lor(x\ne y)$ is always true, but this can
cease to be true in other logics, or in algorithmic systems that do
have complete decision procedures.
This point is brought up in \cite{FTA}, where it is pointed out that,
in their constructive logic, ``apartness'' (i.e. ``I can compute, in this
logic, that $a$ and $b$ are not equal'') is the more fundamental
concept.
\par
\cite{Hur,HD1,HD2} show that it is possible to have, at least for real
algebraic numbers, a constructive implementation of $\R$ for which
equality is decidable on this subset. It should be noted that knowing
an object is, say, an integral domain in the classical sense, is often
not sufficient computationally. For example, if we cannot
computationally decide whether a number is zero or not, we cannot use
fraction-free Gaussian elimination for finding determinants, but must
use Cramer's rule or the equivalent, an $O(n!)$ algorithm rather than
an $O(n^3)$ one.
\par
The current OpenMath CDs only define one meaning of equality, which is
intended to be ``I can prove that $a$ and $b$ are equal''. In some
sense, this OpenMath definition is circular, since rules such as
commutativity, which one might use in such a proof, are defined as
$a\times b=b\times a$. Furthermore, the definition of ``prove'' is not
stated, but, this author would argue, is implicitly that of classical
logic. Other notions of equality could clearly be defined in other
CDs.
\par
These debates over the meaning of equality could be dismissed (but
incorrectly in the author's view) as the hair-splitting of logicians, were
it not for the fact that these distinctions crop up in practice. There has
just (August 2001) been a debate on {\tt comp.soft-sys.maple} about the
difference between {\tt FAIL} and {\tt false} in Maple's {\tt testeq}
Monte-Carlo equality tester.
\section{Just what logic are you using, anyway?}
This is, in some ways, the most fundamental question of all. Many of
the rules of classical logic do not hold in some constructive, or even
intuitionistic, logics. At one level, this is trivially solved in
OpenMath: the {\tt logic1} CD clearly defines the operators of
classical logic, and other CDs would be needed to define other
concepts, e.g. a {\tt logic3} CD to define intuitionistic logic.
\par
However, this is the easy part. How do we know what logic was applied
to yield a piece of mathematical knowledge? This is an area that is
not really treated in OpenMath, where a Formal Mathematical Property
is defined in the OpenMath standard \cite{OpenMath} as follows.
\begin{quotation}
\noindent
It corresponds to a theorem of a theory in {\it some\/} formal system
\end{quotation}
(our italics).
Although this has not been fleshed out, it would be possible to use
CDGroups in a different way to their current use (as collections of
thematically-related CDs): they could be used to group together CDs
containing objects and the Formal Mathematical Properties that were
true in {\it the same\/} formal system.
\section{So, what use is OpenMath?}
In this workshop, \cite{Asperti et al.} wrote
\begin{quotation}
OpenMath's Content Dictionaries are not ``first class citizens''. They are
machine-readable, but not machine understandable; thir content is largely
informal preventing the possibility of any automatic elaboration of their
content. They are essentially conceived as background references for the
implementors of Phrase-books. 
\end{quotation}
\begin{enumerate}
\item Is this true?
\item Is this a bad thing?
\end{enumerate}
\subsection{Is this true?}
OpenMath CDs in practice define various sorts of symbols.
\begin{itemize}
\item Abstract operations, such as ``+'' --- not to be confused with ``+ on
{\tt Nat}''.
\item Operations with ill-defined semantics, or multiple semantics
among which an undefined choice has to be made, such as
\verb+<OMS name="int" cd="calculus1"/>+ --- Riemann, Riemann-Steltjes,
Lebesgue $\ldots$?
\item[]Other CDs can define more specific versions!
\item Operations that could be well-defined, and probably we could try
harder, such as $\log$.
\item[]Nevertheless, hard decisions are made, such as \verb+logic1+ havng
classical semantics.
\item Operations which are truly fixed by the CDs, e.g. $\arccot$.
\item[]These grow as we move out of the core, e.g. special functions,
groups.
\end{itemize}
This is a retrospective classification by the author, and maybe these
distinctions should be clearer, or even formally defined at all.
\subsection{Is this a bad thing?}
Clearly, the more precision OpenMath can bring, the better.
\par\noindent
But an attempt to define the semantics of, say, ``+'' would restrict
generality unacceptably.
\par\noindent
Any precision is better than none, and in many key areas of ambiguity,
OpenMath is faced with hard choices which it has to make.
\par\noindent
Is guidance to phrasebook writers not worth having?
\section{Conclusions}
Mathematical knowledge, or at least its common representations, is
less precise than is often thought --- see the entries marked
``inconsistent'' in table 1. We have pointed out several levels of
ambiguity, and noted that some of the problems are soluble through
clarity of definition, as in the OpenMath Content Dictionary
system. However, the fundamental ones of ``what equality do you mean''
and ``what logic is this in'' are deeper, and it is an open question
whether a formal approach can encompass more than one of these
properly.
\par\noindent
However, much confusion can be clarified --- ``what is $\arccot(-1)$'',
``what is the Ricci tensor'', ``how big is $D_8$'', ``is this `or'
intuitionistic'' etc.?
\begin{thebibliography}{99}
\bibitem{AS}
Abramowitz,M. \& Stegun,I.,
{\it Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical
Tables\/}.
US Government Printing Office, 1964.
10th Printing December 1972.
\bibitem{Asperti et al.}
Asperti,A., Padovani,L., Sacerdot Coen,C., Guidi,F. \& Schena,I.,
Mathematical Knowledge Management in HELM.
Proc. MKM 2001.
\bibitem{CHM}
Conway,J.H., Hulpke,A. \& McKay,J.,
On Transitive Permutation Groups.
{\it LMS J. Comput. Math.\/} {\bf1} (1998)
pp. 1--8. \verb+http://www.lms.ac.uk/jcm/lms96001+. 
\bibitem{Atlas}
Conway,J.H., Curtis,R.T., Norton,S.P. \& Parker,R.A.,
{\it ATLAS of finite groups\/}. Oxford University Press, 1985.
\bibitem{CDJW}
Corless,R.M., Davenport,J.H., Jeffrey,D.J. \& Watt,S.M.,
``According to Abram\-owitz and Stegun''.
{\it ACM SIGSAM Bulletin\/} {\bf30} (2000) 2, pp. 58--65.
\bibitem{AISC}
Corless,R.M., Davenport,J.H., Jeffrey,D.J., Litt,G. \& Watt,S.M.,
Reasoning about the Elementary Functions of Complex Analysis.
Artificial Intelligence and Symbolic Computation (ed. John A. Campbell \&
Eugenio Roanes-Lozano), Springer Lecture Notes in Artificial Intelligence
Vol. 1930, Springer-Verlag 2001, pp. 115--126.
\verb+http://www.apmaths.uwo.ca/~djeffrey/offprints.html+.
\verb+http://link.springer.de/link/service/series/0558/bibs/1930/19300115.htm+.
\bibitem{Equality}
Davenport,J.H.,
Equality in Computer Algebra and Beyond.
Proc. Calculemus 2001 (ed. S.A. Linton) pp. 120-129.
\verb+http://www-theory.+\allowbreak{}\verb+dcs.st-andrews.+\allowbreak{}\verb+ac.uk/~sal/CalcCD+
%\bibitem{Diamond}Davenport,J.H. \& Fischer,H.-C.,
%Manipulation of Expressions.
%{\it Improving Floating-Point Programming\/} (ed. P.J.L.~Wallis),
%Wiley, 1990, pp. 149--167.
%\bibitem{DT}
%Davenport,J.H. \& Trager,B.M.,
%Scratchpad's View of Algebra I: Basic Commutative Algebra.
%Proc.~DISCO '90 (Springer Lecture Notes in Computer Science Vol.
%429, ed.~A.~Miola), Springer-Verlag, 1990, pp. 40--54.
%A revised version is in Axiom Technical Report ATR/1, Nag Ltd., December 1992.
%\bibitem{DGT}
%Davenport,J.H., Gianni,P. \& Trager,B.M.,
%Scratchpad's View of Algebra II:
%A Categorical View of Factorization.
%Proc.~ISSAC 1991 (ed.~S.M.~Watt), ACM, New York, pp. 32--38.
%A revised version is in Axiom Technical Report ATR/2, Nag Ltd., December 1992.
%\bibitem{DST}
%Davenport,J.H., Siret,Y. \& Tournier,E.,
%{\it Computer Algebra\/} (2nd ed.).
%Academic Press, London, 1993.
%\bibitem{Dunstan}
%Dunstan,M.N.,
%Larch/Aldor - A Larch BISL for AXIOM and Aldor.
%Ph.D. Thesis, University of St.~Andrews, 1999.
%\bibitem{DKLM1}
%Dunstan,M., Kelsey,T., Linton,S. \& Martin,U.,
%Lightweight Formal Methods for Computer Algebra Methods.
%Proc.~ISSAC 1998 (ed.~O.~Gloor), ACM, New York, 1998, pp. 80--87.
%\bibitem{DKLM2}
%Dunstan,M., Kelsey,T., Linton,S. \& Martin,U.,
%Formal methods for extensions to CAS.
%FM '99 Vol.~II (Springer Lecture Notes in Computer Science Vol. 1709,
%ed.~J.W.J.~Wing, J.~Woodcock
%\& J.~Davies), Springer-Verlag, 1999, pp. 1758--1777.
%\bibitem{Edalat}
%Edalat,A., Potts,P.J. \& Escard\'o,M.H.,
%Semantics of exact computer arithmetic.
%Proc. 12th IEEE Symp. Logic in Computer Science (IEEE Computer Society Press,
%1997), pp. 248--257.
\bibitem{FIK}
Freeman,T., Imirzian,G. \& Kaltofen,E.,
A System for Manipulating Polynomials Given by Straight-Line Programs.
Proc. SYMSAC 86 (ACM, New York, 1986) pp. 169--175.
\bibitem{FS}
Fr\"ohlich,A. \& Shepherdson,J.C.,
Effective Procedures in Field Theory.
{\it Phil. Trans. Roy. Soc. Ser. A\/} {\bf248} (1955--6) pp. 407--432.
Zbl. 70,35.
MR 17,570d
\bibitem{FTA}
Geuvers,H., Pollack,R., Wiedijk,F. \&, Zwanenburg,J 
The algebraic hierarchy of the FTA project.
Proc. Calculemus 2001 (ed. S.A. Linton) pp. 13-29.
\verb+http://www-theory.dcs.st-andrews.ac.uk/~sal/CalcCD+.
%\bibitem{Gonnet}
%Gonnet,G.H.
%Determining Equivalence of Expressions in Random Polynomial Time.
%Proc. 16th ACM Symp. Theory of Computing, 1984, pp. 334-341. 
%\bibitem{Gosper}
%Gosper,R.W.,Jr.,
%Item 101b: Continued Fraction Arithmetic.
%HAKMEM, M.I.T. A.I. Memo 232, Feb. 1972, pp. 39--44.
\bibitem{GR}
Gradshteyn,I.S. \& Ryzhik,I.M. (ed A. Jeffrey),
{\it Table of Integrals, Series and Products\/}.
5th ed., Academic Press, 1994.
%\bibitem{Larch}
%Guttag,J.V. \& Horning,J.J.,
%{\it Larch: Languages and Tools for Formal Specification\/}.
%Texts and Monographs in Computer Science, Springer-Verlag, 1993.
%\bibitem{Harrington}
%Harrington,S.J.,
%Infinite Power Series.
%{\it Software --- Practice and Experience\/} {\bf 10} (1980) pp. 835--848.
%\bibitem{Hearn}
%Hearn,A.C.,
%{\it REDUCE User's Manual\/}, Version 3.4, July 1991.
%RAND Corporation Publication CP--78.
\bibitem{Hur}
Hur,N.,
{\it Exact Real Arithmetic in Computer Algebra\/}.
Ph.D. Thesis, University of Bath, 2001.
\bibitem{HD1}
Hur,N. \& Davenport,J.H.,
An Exact Real Algebraic Arithmetic with Equality Determination.
Proc.~ISSAC 2000 (ed.~C.~Traverso), pp. 169--174.
\bibitem{HD2}
Hur,N. \& Davenport,J.H.,
A Generic Root Operation for Exact Real Arithmetic.
Computability and Complexity in Analysis (ed. J. Blanck, V. Brattka \& 
P. Hertling), Springer Lecture Notes in Computer Science 2064, Springer-Verlag,
2001, pp. 82--87.
%\bibitem{LISPVM}
%IBM Corporation,
%{\it LISP/VM Reference Manual\/}.
%SH20--6477--0, IBM, 1984.
%\bibitem{JS}
%Jenks,R.D. \& Sutor,R.S.,
%{\it AXIOM: The Scientific Computation System\/}.
%Springer-Verlag, New York, 1992.
%\bibitem{JT}
%Jenks,R.D. \& Trager,B.M.,
%A Language for Computational Algebra.
%Proc.~SYMSAC 81, ACM, New York, 1981, pp. 6--13.
%Reprinted in {\it SIGPLAN Notices\/} {\bf16} (1981) No. 11, pp. 22--29.
%\bibitem{KT}
%Kaltofen,E. \& Trager,B.M.,
%Computing with Polynomials Given by Black Boxes for their Evaluations:
%Greatest Common Divisors, Factorization, Separation of Numerators and
%Denominators. 
%{\it J. Symbolic Comp.\/} {\bf9} (1990) pp. 301--320.
%\bibitem{Kelsey}
%Kelsey,T.W.,
%{\it Formal Methods and Computer Algebra:
%A Larch Specification of Axiom Categories and Functors\/}.
%Ph.D.~Thesis, St.~Andrews, 2000.
%\bibitem{KlunersMalle}
%Kl\"uners,J. \& Malle,G.,
%Explicit Galois Realization of Transitive Groups of Degree up to 15.
%{\it J. Symbolic Comp.\/} {\bf30} (2000) pp. 675--716.
%\bibitem{MM}
%M\'enissier-Morain,V.,
%{\it Arithm{\'e}tique exacte, conception, algorithmique et performances d'une
%impl{\'e}mentation informatique en pr{\'e}cision arbitraire\/}.
%Th{\`e}se, Universit{\'e} Paris 7, Dec. 1994.
\bibitem{Kleene}
Kleene,S.C.,
On Notation of Ordinal Numbers.
{\it Journal of Symbolic Logic\/} {\bf3} (1938) pp. 150--155.
\bibitem{Naylor}
Naylor,W.A.,
{\it Polynomial GCD Using Straight Line Program Representation\/}.
Ph.D. Thesis, University of Bath, 2000.
%\bibitem{Norman}
%Norman,A.C.,
%Computing with Formal Power Series.
%{\it ACM Trans. Mathematical Software\/} {\bf1} (1975) pp. 346--356.
\bibitem{OpenMath}
The OpenMath Consortium. OpenMath.
{\tt http://www.nag.co.uk/}\allowbreak{\tt projects/}\allowbreak{\tt
OpenMath/}.
%\bibitem{Rabin}
%Rabin,M.O.,
%Probabilistic Algorithm for Testing Primality.
%{\it J. Number Theory\/} {\bf12} (1980) pp. 128--138.
%\bibitem{Rioboo}
%Rioboo,R.,
%Real algebraic closure of an ordered field, implementation in Axiom.
%Proc. ISSAC '92, pp. 206--215.
%\bibitem{Rotman}
%Rotman,J.J.,
%An Introduction to the Theory of Groups.
%Springer Graduate Texts in Mathematics 148, Springer-Verlag, 1995.
%\bibitem{GAP}
%Sch\"onert,M. (together with H.U. Bessche, T. Breuer, F. Celler, B. Eick,
%V. Felsch, A. Hulpke, J. Mnich, W. Nickel, G. Pfeiffer, U. Polis, 
%K. Thei{\ss}en), updated by S.A. Linton,
%{\it GAP: Groups Algorithms and Programming\/} v. 3.4.4.
%Distributed Electronically with GAP, 18 April 1997.
%\bibitem{CL}
%Steele,G.L.,Jr.,
%{\it Common LISP: The Language\/}, 2nd. edition.
%Digital Press, 1990.
%\bibitem{Vuillemin}
%Vuillemin,J.E.,
%Exact real computer arithmetic with continued fractions.
%{\it IEEE Trans. Computing\/} {\bf39} (1990) pp. 1087--1105.
\bibitem{Mma}
Wolfram,S.,
{\it The Mathematica Book\/}.
Wolfram Media/C.U.P., 1999.
\bibitem{MathML}
World-Wide Web Consortium,
Mathematical Markup Language (MathML [tm]) Version 2.0.
W3C Recommendation of 21 February 2001.
{\tt http://www.w3.org/}\allowbreak{}{\tt TR/MathML2}.
\bibitem{CRC}
Zwillinger,D. (ed.),
{\it CRC Standard Mathematical Tables and Formulae\/}.
30th. ed., CRC Press, Boca Raton, 1996.
\end{thebibliography}
\end{document}
