\documentclass[runningheads]{llncs}
\usepackage{amssymb,url,alltt,eurosym,color,supertabular,graphics}
\raggedbottom
\advance\textwidth by 6em
\advance\oddsidemargin by -3em
\advance\evensidemargin by -3em
\advance\textheight by 11.5em
\advance\topmargin by -3em
\def\aands{\emph{Abra\-mo\-witz \& Stegun}}
\def\fear{F.A.R.}
\def\fear{F.E.A.R.}
\def\hisproject{he {\fear} project}
\def\Ln{\mathop{\rm Ln}\nolimits}
\def\calculemus{{\small CALCULEMUS}}
\definecolor{lightgray}{rgb}{.9,.9,.9}
\definecolor{gray}{rgb}{.8,.8,.8}
\definecolor{darkgray}{rgb}{.6,.6,.6}
\begin{document}
\authorrunning{F.~Wiedijk}
\titlerunning{T{\hisproject}}
\title{}
\author{}
\institute{}
\maketitle
\vspace{-1.1cm}
\begingroup
\begin{itemize}
\item[1a)] \textbf{Project Title.}
%Formalizing Analysis Rigorously.
Formalizing Elementary Analysis Rigorously.
\item[1b)] \textbf{Project Acronym.}
{\fear}
\item[1c)] \textbf{Principal Investigator.}
Freek Wiedijk.
\end{itemize}
\endgroup
\begin{itemize}
\item[2a)] \textbf{Summary.}
\begingroup
\parindent=1em
Two classes of systems exist for working with mathematical formulas
on a computer:
`computer algebra' programs (of which Mathematica is the best known)
and `proof assistants' (programs for the verification of
mathematical proofs).
The first kind of system (computer algebra) manipulates formulas that
do not necessarily have a precise mathematical meaning
(those formulas do not have a `semantics').
The second kind of system (proof assistants) manipulates formulas
that \emph{do} have a precise meaning, but those often do not much resemble
the formulas that one encounters in mathematical textbooks.
T{\hisproject} will design a language of formulas
that have a precise semantics, but still resemble the
traditional formulas found in textbooks.
We will do this by translating a section from a classic
handbook of mathematical formulas (the
\emph{Handbook of Mathematical Functions} by Abramowitz \& Stegun)
into a proof assistant.
Since the formulas will be entered in a proof assistant, a sound
semantics is guaranteed.
Also it will be easy to judge whether the translation sufficiently resembles the
original formulas from the handbook.
\endgroup
\smallskip
\item[2b)] \textbf{Abstract for laymen (in Dutch).}
\begingroup
\parindent=1em
Er zijn twee soorten systemen om met wiskundige formules
op de computer te werken:
de `computer algebra' programma's (waarvan Mathematica de bekendste
is) en de `bewijsassistenten'
(programma's om wiskundige be\-wij\-zen mee te verifi\"eren).
Het eerste soort systeem (computer algebra) manipuleert formules die niet
altijd een precieze wiskundige betekenis hebben
(die formules hebben geen `semantiek').
Het tweede soort systeem (bewijsassistenten) manipuleert formules
die wel een precieze betekenis hebben, maar vaak niet lijken
op wat je in wiskundeboeken tegenkomt.
Het {\fear} project zal een vorm ontwerpen voor formules in de computer
zo dat die w\`el een precieze betekenis hebben, maar t\`och lijken op
de traditionele formules uit de wiskundeboeken.
We zullen dit doen door \'e\'en van de secties uit een klassiek
tabellenboek met wiskundige formules (het telefoonboek-dikke
\emph{Handbook of Mathematical Functions} van Abramowitz \& Stegun)
voor een bewijsassistent
te vertalen.
Omdat die formules in de bewijsassistent worden ingevoerd
is dan een goede semantiek gegarandeerd.
Maar ook zal het duidelijk zijn of de vertaling voldoende lijkt op
de originele formules uit het tabellenboek.
\endgroup
\end{itemize}
\begin{itemize}
\item[3)] \textbf{Classification.}
Multidisciplinary: computer science \& mathematics. \\
%\smallskip
Discipline: 6.5 Formal Methods. \\
NOAG-i 2001-2005: Algorithms and Formal Methods (AFM). \\
MSC2000: 03B35, 13Pxx, 26-xx, 30Dxx, 68T15.
\end{itemize}
\begin{itemize}
\item[4)] \textbf{Composition of the Research Team.}
\begin{center}
\vspace{-\smallskipamount}
\begin{tabular}{rclcl}
\emph{name} && \emph{specialty} && \emph{university} \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
prof.~dr.~H.P.~Barendregt &$\enskip$& \emph{type theory} &$\enskip$& Radboud University Nijmegen \\
\emph{promotor} \\
\noalign{\smallskip}
prof.~dr.~M.J.~Beeson && \emph{computer algebra} && San Jos\'e State University \\
&& \emph{theorem proving} \\
\noalign{\smallskip}
dr.~W.~Bosma && \emph{computer algebra} && Radboud University Nijmegen \\
\noalign{\smallskip}
dr.~J.H.~Geuvers && \emph{type theory} && Radboud University Nijmegen \\
&& \emph{theorem proving} \\
\noalign{\smallskip}
dr.~F.~Wiedijk && \emph{theorem proving} && Radboud University Nijmegen \\
\noalign{\smallskip}
\emph{PhD student} && && Radboud University Nijmegen \\
\noalign{\smallskip}
\hline
\end{tabular}%
%$\hspace{-2em}$
\end{center}
\end{itemize}
\begin{itemize}
\item[5)] \textbf{Research Schools.}
Dutch Research School in Logic (OZSL),
Institute for Programming research and Algorithmics (IPA),
Mathematical Research Institute (MRI).
\end{itemize}
\begin{itemize}
\item[6)] \textbf{Description of the Proposed Research.}
\begingroup
\parindent=1em
We will first present the background of this research.
For a presentation of the specifics of the project, skip to
\emph{Core of the Project} on page~\pageref{core}.
When in the text below we refer to {\aands}, we mean the well-known
\emph{Handbook of Mathematical Functions} \cite{abr:ste:64}
by Milton Abramowitz and Irene Stegun.
\medskip\noindent
The research of t{\hisproject} is related to two kinds
of system:
\emph{proof assistants} (theorem proving systems)
and
\emph{computer algebra systems}.
\medskip\noindent
\textbf{Proof assistants} are systems for the verification of
mathematical proofs with the computer.
Major proof assistants are PVS, ACL2, Theorema, $\rm\Omega$mega, IMPS, HOL,
Isabelle, Coq, NuPRL and Mizar \cite{wie:03}.
%
Proof assistants have two main application areas:
\begin{itemize}
\smallskip
\item
The main application is
`formal methods':
checking proofs that occur in the verification of the
correctness of computer systems.
This kind of verification is done
when correctness is of the utmost importance, like in
medical systems,
systems embedded in spacecraft,
systems for public transport
(e.g., software controlling driverless trains),
and systems that will be used in huge numbers
(e.g., subsystems of commercial microprocessor chips,
or programs running on smart cards).
\smallskip
\item
A secondary, more distant, application of these systems
is to support mathematics.
Currently proof assistants are not powerful enough to be
useful in mathematical research,
but in the future these systems might change the way
we do mathematical proofs.
Mathematics might then be routinely
proof checked.
In that case when a mathematical paper is submitted to a journal,
referees will not need to be concerned with its
correctness (because the computer will already have
checked this), but just with the question of whether it is
new and interesting.
This -- potentially very important, but currently rather
utopian -- application of proof assistants
is nicely described in the so-called QED manifesto \cite{qed:94}.
\end{itemize}
\smallskip\noindent
The main weakness of current proof assistants is that mathematically they
are not powerful enough.
They are very good at keeping track of all of the details
of a mathematical proof:
one routinely checks proofs using these systems that have
hundreds, or even thousands, of cases.
However, they are currently not very good at taking
by themselves steps that a human mathematician considers to be
trivial.
One of the most important
class of steps that are not supported well are %algebraic
problems that a high school student can solve without difficulty.
We call these \emph{high school problems}.
Examples of this kind of problem (where $\vdash$ denotes logical consequence) are:
\begin{eqnarray*}
n\ge 2\;,\!\!\quad x={1\over n+1} &\vdash& {x\over 1-x}<1 \\
\noalign{\smallskip}
%n\ne 0\;,\!\!\quad
x=i/n\;,\!\!\quad n=m+1 &\enskip\vdash\enskip& n!\cdot x=i\cdot m! \\
\noalign{\smallskip}
%n\ne 0\;,\!\!\quad
{k\over n}\ge 0 &\vdash& \left|{n-k\over n}-1\right|={k\over n}
\end{eqnarray*}
\noindent
When one encounters problems like this in
a proof assistant, one would like
not to spend any time on it, but just to say
to the system `you know how to do this'.
Currently this is not possible.
We consider this to be the main weakness of current proof
assistants.
\medskip\noindent
\textbf{Computer algebra systems} are systems for the calculation
of answers to algebraic problems with the computer.
Major computer algebra systems are Matlab, Mathematica,
Maple, Magma, GAP, Axiom and MathXpert.
%
Computer algebra systems have two main application areas:
\begin{itemize}
\smallskip
\item
Solving algebraic problems, like the calculation
of the size of an algebraic structure, or an explicit
enumeration of instances of such a structure.
The algebraic objects that these calculations deal with
are generally finite and explicitly given.
\smallskip
\item
Solving problems in elementary analysis (`calculus').
These include simplification of expressions,
calculation of differentials and integrals, and solution
of ordinary and differential equations.
The name `computer algebra' is misleading for this application,
as these problems are not of an algebraic nature.
However, these problems are often solved via
a translation into an algebraic problem.
\end{itemize}
\smallskip
The main weakness of current computer algebra systems is
that for these `calculus' problems they often
give incorrect answers.
For instance the latest version of Maple evaluates the
following expressions (due to Jacques Carette of McMaster University):
\begingroup
\footnotesize
\def\but#1{\eqno{\hspace{5cm}\llap{\rlap{{#1}}\hspace{5.5cm}}}}
\begin{verbatim}
> value(eval(Sum(z^n/n!,n=0..infinity),z=0));
\end{verbatim}
$$0
\but{should be $1$ {\rm (}Maple simplified $0^n$ to $0${\rm )}}$$
\begin{verbatim}
> residue(1/(csgn(z)*z),z=0);
\end{verbatim}
$${1\over\mbox{csgn}(z)}
\but{should not have $z$ free {\rm (}$z$ was bound{\rm )}}$$
\begin{verbatim}
> eval(int(1/(x-a),x=0..1),a=1/2);
\end{verbatim}
$$\pi i
\but{should not be complex {\rm (}real integral{\rm )}}$$%{\rm (}either $0$ or undefined{\rm )}}$$
\begin{verbatim}
> Int(sin(x),x=0..Pi);
\end{verbatim}
$$\int_0^\pi \sin(x)\,dx
\but{\vbox to 0pt{{\parindent=0pt
%\vspace{-6.4pt}
\vspace{2pt}
these two integrals should be equal \\
(change of variables) but they are not; \\
the first is $2$ but the second is $0$ %\\
%(injectivity of the function not checked)
\vss}}}$$
\begin{verbatim}
> student[changevar](sin(x)=t,%,t);
\end{verbatim}
$$\int_0^0 -{t\over (1 - t^2)^{1\over 2}}\,dt
\medskip
\but{}$$%\but{$\!\!\!\!${\dots} this {\rm (}change of variable{\rm )}, but it is not}$$%{\rm (}$0$ instead of $2${\rm )}}$$
\endgroup
\noindent
The reason for this behavior is, that it is much more difficult to always
give a fully mathematically correct answer than
a somewhat plausible one.
In the tension between the ability to transform expressions
for the user as much as possible, and the correctness of
what the computer algebra system is doing, the makers of
these systems take an intermediate position.
The most blatant errors that users complain about are
removed, but more subtle `errors' are ignored.
The idea is that the user should pay attention and
judge for himself whether the program behaves reasonably.
Related to this problem of incorrect answers from computer
algebra system is
the lack of a formal semantics
for the expressions of those systems.
For instance in formulas like:
\begin{eqnarray*}
\ln(\infty) &=& \infty \\
\int {1\over z}\,dz &=& \ln(z)
\end{eqnarray*}
(both Mathematica and Maple calculate like this)
it is not fully clear what the semantics of the symbols $\infty$ and $\int$
%(and maybe $=$)
are (in the second case the question is: where is the constant of integration?)
In particular those symbols are not \emph{defined} in terms of
some foundational system.
For this reason it is sometimes not even possible to say that
the answer of a computer algebra system is incorrect, because
that might depend on the intended semantics of the symbols.
As an example, it is not a priori clear whether
$${x + x\over x} = 2$$
is correct -- because one is calculating in a field $K(x)$ --
or incorrect -- because for $x = 0$ the left hand side is $0/0$,
which probably is not $2$ in any way of dealing with $0/0$, and so
the (partial) function $\lambda x. {x + x\over x}$ differs from
the (total) function $\lambda x. 2$.
Summarizing:
computer algebra systems structurally give incorrect answers,
and the users of these programs do not even have the possibility
to criticize these `errors'
because the expressions manipulated by these programs
do not have an explicit semantics.
We consider this to be the main weakness of current computer
algebra systems.
\medskip\noindent
Related to the lack of semantics for `analysis' expressions
in a computer algebra system is the meaning of expressions
in languages that have been designed for the interchange
of mathematical expressions between different systems.
The two major languages of this kind are MathML \cite{car:ion:min:pop:03} and OpenMath \cite{bus:cap:car:dew:gae:koh:04}.
In practice these languages do not always conserve the
meaning of expressions.
For example, imagine encoding a formula in MathML to be able to
move it between various proof assistants (like Coq, HOL or PVS).
Then the following table shows that in that case the same MathML expression
might get completely different meanings \cite{wie:zwa:03}:
\begin{center}
\smallskip
%\begin{tabular}{lclcl}
%\hline
%\noalign{\smallskip}
%&$\enskip$& $1/0$ &$\enskip$& $1/0 = 0$ \\
%\noalign{\smallskip}
%\hline
%\noalign{\smallskip}
%\emph{PVS} && not a correct term && not a correct formula \\
%\emph{IMPS} && correct, undefined && negation provable \\
%\emph{Coq} && correct, defined, unknown && not provable, negation not provable \\%$\hspace{-5.3pt}$ \\
%\emph{HOL/Mizar} && correct, defined, 0 && provable \\
%\noalign{\smallskip}
%\hline
%\end{tabular}$\hspace{-1em}$
\begin{tabular}{lclcl}
\hline
\noalign{\smallskip}
&$\quad$& $1/0 = 0$ \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
\emph{PVS} && not a correct formula \\
\emph{IMPS} && negation provable \\
\emph{Coq} && not provable, negation not provable \\%$\hspace{-5.3pt}$ \\
\emph{HOL/Mizar} && provable \\
\noalign{\smallskip}
\hline
\end{tabular}$\hspace{-1em}$
\end{center}
\smallskip\noindent
Apparently if one uses MathML or OpenMath to communicate
even a simple equation like `$1/x = x$'
between systems, the meaning changes!
The aim of t{\hisproject} is to
design a small expression language like MathML or OpenMath, but one
that has a very explicit and well-defined semantics.
\medskip\noindent
This project simultaneously addresses the two problems
that we noted:
\begin{itemize}
\smallskip
\item
Proof assistants are not powerful enough, as they cannot do
`high school problems' by themselves.
\smallskip
\item
Computer algebra systems are not fully correct; worse, they
even lack a semantics that makes discussion of correctness meaningful.
\end{itemize}
\smallskip
Our approach to solve these problems will be to design
an expression language for the kind of expressions that
one encounters in a computer algebra system, but \emph{with an
explicit semantics}.
This semantics will not just be given in a traditional
mathematical style.
To make sure that it is solid
we will define it inside
one of the major proof assistants.
Proof assistants are built
on a small logical foundation, which has a simple notion of
`model'. So formalizing in a proof assistant
leads directly to a `semantics' inside that same model.
This way we make the style of doing calculus in a computer algebra
system -- which can do `high school mathematics' by itself --
available to proof assistants.
And, by providing a proper semantics, we get the possibility
of having a computer algebra system that is fully correct.
%
(Our project will lead to more
complicated terms than one finds in Maple, with more subtle
distinctions and embeddings and liftings and so on.
Therefore, it will not give a semantics for Maple expressions
the way they are today.
But the idea is that one could, in the future,
implement a correct Maple-like program based on this research.
The project is necessary for that, but not sufficient.
Without a proper focus on semantics we will never get correct
computer algebra.)
\medskip\noindent
It is relatively easy to render the meaning of formulas
from elementary analysis in a proof assistant.
However, to design an expression language in such a
way that it also is close to the formulas that one
encounters in normal mathematics textbooks is more difficult.
If one looks at the statements from elementary analysis that
are present in the libraries of the current proof assistants,
then they are sometimes remarkably different in style from the way
that one would write them in normal mathematical texts.
The reason for this is two-fold:
\begin{itemize}
\smallskip
\item
\emph{The proof assistants do not have the features that one
needs to render mathematics reasonably.}
%
For instance, in the HOL system all functions are total.
Therefore, the limit operation when
modeled as a function would always have a value,
even if the limit does not exists.
For this reason, the limit operator in the standard HOL library
is modeled as a relation, instead of as a function.
But that is not the way that limits are written
customarily, and not as practical at that.
%Another example: in the Coq system partial functions are
%modeled by having `proof objects' as arguments.
%For this reason the formulas in this system contain
%`proof object' subterms that one won't see in normal
%mathematics.
%
%Still another example: in the Mizar system there are
%no binders.
%Therefore one cannot write
%
% ...
%
%\noindent
%but instead has to `circumscribe' this as
%
% ...
\smallskip
\item
\emph{In mathematics one often uses imprecise notations.}
%
Examples of this are calculations with `infinity',
indefinite integration where one omits `constants of
integration',
`multi-valued functions' in the complex plane where one
leaves unspecified what branch one is on,
etc.
In informal practice this works perfectly, but in a
situation where precision counts this is problematical.
%\begin{center}
%\medskip
%\smallskip
%*
%\end{center}
%\bigskip
\end{itemize}
%\smallskip
%The project's main goal is to find an
%expression language that combines a precise semantics in
%a proof assistant with a close similarity to the way the
%mathematics would be written normally.
%%
%To make this specific we will focus on {\aands}.
%We claim that the formulas from this well-known book
%should be representable
%%in a reasonable way
%in a proof assistant
%if that proof assistant is to be useful for doing mathematics.
%Therefore we have the following
%
%\bigskip\noindent
\newpage\noindent
\textbf{Core of the Project.}\label{core}\emph{
We will formalize a section from {\aands}
in a modern proof assistant.
The expressions in the formalization will be made to resemble
the original expressions as found in {\aands} as closely as possible.
The formalization will be complete, except for the proofs.
In particular, all the symbols that are used will be fully defined
in terms of the foundations of the proof assistant.
Although we will not encode all necessary proofs in the formalization,
we will show in the traditional mathematical style
that the formalization might be completed that way.
}
\medskip\noindent
Two choices will be made during the first phase of the project:
\begin{itemize}
\smallskip
\item
\emph{Which proof assistant?}
The most natural choice is to take Coq \cite{coq:04}.
In Nijmegen a large Coq library has been created \cite{cru:geu:wie:04}
and there is a large amount of Coq expertise available there.
Coq is also one of the most expressive systems for formalization of
mathematics in the world today.
%However after initial experimentation
%it might turn out that Coq is not the best system to use.
%In that case we might decide to switch to a different system like
Other possible choices would be
HOL \cite{gor:mel:93,har:00,nip:pau:wen:02}, Mizar \cite{muz:93} %,wie:99:1}
or PVS \cite{owr:rus:sha:92}.
The HOL and Mizar systems have impressive
libraries of mathematics that we could base our work on.
PVS is the most popular proof assistant in computer
science, and it supports partial functions in a way
that the other three systems cannot.
\smallskip
\item
\emph{Which section of \emph{{\aands}}?}
The most natural choice is to take the first relevant section:
Section 4.1,
which gives a list of formulas about the natural logarithm.
It is reproduced as an appendix to this proposal on pages \pageref{4.1-start}--\pageref{4.1-stop}.
It contains 57 formula entries which correspond to 74 inferences.
Section 4.1 contains interesting challenges for
a semantical treatment of the formulas.
It distinguishes between `$\ln(z)$' (the main branch of the
complex natural logarithm) and `$\Ln(z)$'
(the `multi-valued function').
It also contains `fuzzy' mathematical statements
like $\ln(0) = -\infty$ (equation 4.1.13).
An important kind of expression that Section 4.1 does not
contain is order symbols (`big-O notation').
The semantics for formulas like those in Section 4.1
ideally will give a meaning to a
formula that contains infinity, constants of integration, multi-valued
functions and order symbols, all at the same time.
\end{itemize}
%\begin{center}
%*
%\vspace{-\smallskipamount}
%\end{center}
\bigskip
\noindent
In \cite{bee:wie:02} we defined a rigorous semantics for formulas in
elementary analysis that contain the symbol $\infty$.
We did this by interpreting expressions that contain this
symbol as \emph{filters} over the underlying set of numbers.
Part of the current project can be seen as an extension of this
work.
If one follows the approach from \cite{bee:wie:02} then one gets a proliferation
of types, with coercion functions between them.
For instance, the number $0$ can then both be interpreted as a number,
or as the filter
corresponding to that number.
When one extends this approach to cover multi-valued functions, it also
can be interpreted as a set of numbers (a singleton set).
The challenge of t{\hisproject} is how to define all these types
-- numbers, filters, sets --
such that they fit together in a way that leads to practical formulas.
Writing the formulas from {\aands} using a signature similar to
that of MathML is straight-forward.
However, it is then clearly impossible to give a semantics to the
symbols from that signature in such a way that the formulas become
meaningful.
For instance formulas 4.1.1 and 4.1.4 from {\aands} are
$\ln z = \int_1^z {dt\over t}$ and $\Ln z = \int_1^z {dt\over t}$.
Clearly the symbol $\int$ means something different in those two formulas.
%But even Content MathML has only one entity for the concept of `integral'.
The approach that we will follow in the project is to take
a MathML-like encoding of the formulas, and then systematically \emph{disambiguate}
the symbols.
For every symbol we will have various versions with various
types (on numbers, filters, sets, etc.)
Also we will have to insert coercion functions in the expressions to
have them well-typed.
Finally, to get from a `naive' MathML-like encoding of the
formulas to a semantically meaningful disambiguation
%and back
will be non-trivial.
Therefore we will build automated support for this task.
In this implementation
the formulas will be encoded using the OpenMath/OMDoc standard \cite{bus:cap:car:dew:gae:koh:04,koh:00,koh:04}.
\medskip\noindent
%\newpage\noindent
This project will involve work on three different levels:
\begin{itemize}
\smallskip
\item
First of all it will give a mathematical definition of a signature
for the formulas of elementary analysis, and
a formal definition of an expression language using that signature.
This will then be written in the form of a normal mathematical
article.
\smallskip
\item
After that it will create a formalization of these definitions.
This will be work with a proof assistant.
As working in a proof assistant tends to be time consuming,
we expect this to be the main part of the project.
\smallskip
\item
Finally there will be an implementation component.
A converter will be written between formulas in the proof assistant and
a -- system independent -- OpenMath/OMDoc encoding of the
same expressions.
Also software will be written to help transform a naive rendering
of the formulas into a semantically meaningful encoding.
\end{itemize}
\medskip\noindent
\textbf{Related Work.}
\smallskip\noindent
Relating proof assistants to computer algebra systems is
the subject of various projects, like the {\calculemus} project \cite{cal:04},
the FoC project \cite{bou:har:hir:men:rio:99}, and the MathScheme project \cite{far:mor:03}.
(The Foundations group in Nijmegen is a participant of the {\calculemus} network.)
These projects focus on implementation of frameworks that combine those
two kinds of system.
They do not primarily focus on the semantical questions that are the subject of
t{\hisproject}.
There are projects that aim to create databases that are electronic versions
of {\aands}, like the NIST's Digital Library of Mathematical Functions project
\cite{loz:mil:sau:99,mil:you:03}
and
INRIA's Encyclopedia of Special Functions project
\cite{meu:sal:03}
(which is part of its Algorithms Project).
We could have based our project on formulas from those
databases instead of on {\aands}.
However, the formulas from those sources do not relate as much to
semantics of computer algebra as the `informal' formulas from {\aands}.
Prof. Davenport has written papers
\cite{bra:cor:dav:jef:wat:02,cor:dav:jef:wat:00}
that are closely related to the
topic of this proposal.
At various {\calculemus} meetings he has given talks in which he
stated that the notion of \emph{branch cut} from complex function
theory has never been given a formal definition.
He claimed to have searched many textbooks, and that the notion
of branch cut is always just presented by example
instead of being formally defined.
It will be part of our project to provide Prof. Davenport
with the formal definition he is looking for.
\medskip\noindent
In the Foundations group in Nijmegen we have much expertise with formalization
of mathematics.
We have built a large library -- called the C-CoRN library \cite{cru:geu:wie:04} -- of digital mathematics in the proof assistant Coq.
The Foundations group participates in various European projects like the
{\calculemus} project,
the TYPES working group, the MoWGLI project and the MKM network.
The project proposed here will fit seamlessly into the research of
the Foundations group.
\medskip\noindent
\textbf{Some Questions \& Answers.}
\smallskip\noindent
\emph{Is this project about mathematics or about computer science?}
\smallskip\noindent
About both!
From the point of view of mathematics, the project is conceptual:
it focuses on definitions.
However, it will need a deep understanding of what mathematical
meaning is.
Also the project will generate mathematical
problems that, even if not `deep', still will
need mathematical proof.
(It should be pointed out that
Prof. Davenport has repeatedly claimed at the {\calculemus}
meetings that the mathematical problems inherent in the subject
of this proposal are \emph{not} trivial.)
In computer science, proof assistants are an important tool
in the field of \emph{formal methods}.
A main goal of the project is to improve proof assistants.
The project will heavily use proof assistants, and define a
formal language to be used in proof assistants.
For this formal language a translation system will be
implemented to convert this language between encodings
inside proof assistants and a system independent OpenMath
encoding.
\medskip\noindent
\emph{Is the formalization of a few pages of mathematics -- and
without full proofs at that -- not too small an endeavor
for a PhD project that will take four years?}
\smallskip\noindent
Formalizing the \emph{content} of those pages -- without proofs --
is not too hard.
The difficulty is finding a form for those formulas that
combines a solid semantics with a similarity to the
informal formulas of {\aands} (which are similar to
the one that one finds in computer algebra systems).
From preliminary experiments with development of such an
encoding, this appears to be far from trivial.
%Also, at the end the project there might be time to investigate how the
%core part of the work extends in various directions.
%See the Work Programme on page \pageref{workprogramme:extensions} below.
\medskip\noindent
\emph{Aiming for large-scale formalization of mathematics is rather utopian:
why should we support a project that reaches for such a far-away goal?}
\smallskip\noindent
The goal of the project is to improve proof assistants and
computer algebra systems.
Using proof assistants for checking mathematics is only
\emph{one} of its applications.
The use of proof assistants for the verification of critical
computer systems is an important field of research, and
not utopian at all.
\medskip\noindent
\emph{{\emph{\aands}} is not real mathematics, but `mathematics for engineers':
surely it is not important to mimic this style
of doing calculus?}
\smallskip\noindent
The way {\aands} write their formulas is
close to the way that computer algebra systems represent
those same formulas.
The basic techniques of computer algebra systems work
best when the formulas are closed algebraic equations or
inequalities, instead of more complex logical formulas.
If one would represent the mathematics in the traditional
way to make it rigorous, then the formulas would not have this simple
shape anymore.
%Therefore, the reason to follow the style of {\aands}
%%is not that we think it is important by itself, but
%%more that
%is that it is a form for the mathematics that lends
%itself better to the algorithms of computer algebra systems.
Another reason for following the `informal' way of doing
calculus from {\aands} is that it is closer to the
way a mathematician will reason on a piece of paper.
When presenting his mathematics formally he might not use
this style, but when doing the calculations himself he
certainly will.
This is an important reason for following the style of {\aands}:
%we have the goal in mind that
we want to improve the proof assistants in such a way that
they become more attractive to mathematicians \cite{wie:04}.
\medskip\noindent
\emph{Elementary analysis is basic mathematics: surely for
a competent mathematician it is a triviality to represent
this kind of formulas?}
\smallskip\noindent
The goal of having formal formulas that are close to the
informal style of doing calculus is more a conceptual
problem than a mathematical problem.
To be able to do this project one not only needs mathematical
competence, but also an understanding of formalization.
Of course if a competent mathematician has this understanding
he can work on this project.
But we do not expect it to be trivial:
if it was trivial, the computer algebra systems would
already use an expression language like the one that this
project is aiming for.
%And they do not.
\medskip\noindent
\emph{Why won't the project aim at formalizing the proofs too?}
\smallskip\noindent
Although the formulas from {\aands} are
elementary mathematics, formalizing their proofs would take a large
amount of work.
For the main goals of the project that work is
irrelevant.
It will just take effort away from the more important parts
of the project.
(And note that we \emph{will} formalize some of the proofs,
we just do not want to take the time to formalize \emph{all} proofs.)
\medskip\noindent
\emph{NIST is currently creating a database called
the Digital Library of Mathematical Functions.
%\cite{loz:mil:sau:99,mil:you:03}.
That is a formal version of \emph{{\aands}}, isn't it?
So hasn't your project already been done by them?}
\smallskip\noindent
The database that is being created by NIST will serve a similar
purpose as {\aands}, but it is \emph{not} a direct translation.
Therefore it will not need to have counterparts to the
informal formulas that one finds in {\aands} and in computer algebra
(like $\ln(\infty) = \infty$).
Also, the people that create this database do not worry about
formal semantics -- it is on the level of computer algebra in this
respect -- and so will put formulas like $\int\!{1\over z}\,dz = \ln(z)$
in it without seeing a problem.
For these reasons, NIST's project does not face the problems of proof assistants
and computer algebra systems like we will do.
\medskip\noindent
\emph{You claim that the current formulas in proof assistants often
look different from their informal counterparts: but why do you think you can do
better as you will be using those same proof assistants as well?}
\smallskip\noindent
The reason that those formulas look different from the formulas of informal
calculus is that it is \emph{hard} to make them look similar.
The people who did those formalizations were only interested in the
\emph{content} of the mathematics, and not in the shape of the formulas.
We will spend a whole PhD project on this problem.
That has not been done before.
\endgroup
\end{itemize}
\begin{itemize}
\item[7)] \textbf{Work Programme.}\label{workprogramme}
\bigskip
\begin{quote}
\begingroup
%\footnotesize
%\it
\setlength{\unitlength}{.31mm}
\begin{picture}(400,230)(0,160)
%\put(0,160){\framebox(400,230){}}
\put(0,380){\makebox(0,0)[lb]{\emph{year 1}}}
\put(100,380){\makebox(0,0)[lb]{\emph{year 2}}}
\put(200,380){\makebox(0,0)[lb]{\emph{year 3}}}
\put(300,380){\makebox(0,0)[lb]{\emph{year 4}}}
\put(0,160){\textcolor{darkgray}{\line(0,1){210}}}
\put(100,160){\textcolor{darkgray}{\line(0,1){210}}}
\put(200,160){\textcolor{darkgray}{\line(0,1){210}}}
\put(300,160){\textcolor{darkgray}{\line(0,1){210}}}
\put(400,160){\textcolor{darkgray}{\line(0,1){210}}}
\put(0,370){\makebox(0,0)[lt]{\textcolor{gray}{\rule{100\unitlength}{20\unitlength}}}}
\put(0,360){\makebox(0,0)[l]{\strut\ getting acquainted}}
\put(0,340){\makebox(0,0)[lt]{\textcolor{gray}{\rule{200\unitlength}{20\unitlength}}}}
\put(0,330){\makebox(0,0)[l]{\strut\ mathematical description}}
\put(50,310){\makebox(0,0)[lt]{\textcolor{gray}{\rule{250\unitlength}{20\unitlength}}}}
\put(50,300){\makebox(0,0)[l]{\strut\ formalization}}
\put(200,280){\makebox(0,0)[lt]{\textcolor{gray}{\rule{150\unitlength}{20\unitlength}}}}
\put(200,270){\makebox(0,0)[l]{\strut\ OpenMath conversion}}
\put(200,250){\makebox(0,0)[lt]{\textcolor{lightgray}{\rule{200\unitlength}{20\unitlength}}}}
\put(200,240){\makebox(0,0)[l]{\strut\ investigating extensions}}
\put(50,210){\makebox(0,0)[lt]{\textcolor{gray}{\rule{300\unitlength}{20\unitlength}}}}
\put(50,200){\makebox(0,0)[l]{\strut\ conference papers}}
\put(200,180){\makebox(0,0)[lt]{\textcolor{gray}{\rule{200\unitlength}{20\unitlength}}}}
\put(200,170){\makebox(0,0)[l]{\strut\ writing thesis}}
%\put(100,150){\makebox(0,0)[lt]{\textcolor{lightgray}{\rule{100\unitlength}{20\unitlength}}}}
%\put(100,140){\makebox(0,0)[l]{\strut\ summer school}}
\end{picture}
\endgroup
\smallskip
\end{quote}
\begin{flushleft}
\begin{tabular}{lp{27.5em}}
\emph{year 1} &
Getting acquainted with the relevant proof assistants.
Getting acquainted with the relevant mathematics. \\
\emph{year 1--2}$\quad$ &
Abstract mathematical description of signature \& semantics. \\
\emph{year 2--3} &
Formalization of signature/definitions in the primary proof assistant. \\
\emph{year 3} &
Definition of OpenMath CD for the signature.
Implementation of conversion from OMDoc to input format of the primary proof assistant. \\
\label{workprogramme:extensions}
\emph{year 3--4} &
Investigation of the effort needed to complete the formalization with proofs.
Investigation of the effort needed to treat other sections in {\aands} similarly.
Investigation of the effort needed for formalization in other proof assistants. \\
\noalign{\medskip}
\emph{year 1--3} &
Papers in conferences or workshops. \\
\emph{year 3--4} &
Writing the thesis. \\
%\emph{year 2} &
%Visit to a relevant summer school.
\end{tabular}
\end{flushleft}
\noindent
The PhD student in this project will be part of the
Institute for Programming research and Algorithmics (IPA).
In addition to educational activities organized by IPA, the
student will follow local courses at the University of Nijmegen,
and participate in one or two summer schools.
The primary supervisor will be Wiedijk, with Barendregt as
the second supervisor and promotor.
The research
group has a good track record in supervising PhD students and hosts
a good mix of PhD students and more experienced postdoc researchers
and staff.
\end{itemize}
\begin{itemize}
\item[8)] \textbf{Expected Use of Instrumentation.}
Symbolic manipulation programs like proof assistants and computer algebra
systems are notoriously resource hungry.
For this reason we will dedicate a special computer to the project.
On this system the major proof assistants and computer algebra
systems will be installed. % for experimentation.
\begin{quote}
\begin{tabular}{lclcrr}
\noalign{\medskip\smallskip}
\hline
\noalign{\smallskip}
\emph{hardware} &$\quad$& dual processor system &$\qquad$& \euro{} & 5,000 \\
&& maintenance contract && \euro{} & 360 \\
\noalign{\medskip}
\emph{software} && license, Magma version 2.11 && \euro{} & 950 \\
&& license, Maple version 9.5 && \euro{} & 400 \\
&& license, Mathematica version 5.1 && \euro{} & 1,460 \\
&& license, MathXpert version 3 && \euro{} & 80 \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
\emph{total} &&&& \euro{} & 8,250 \\
\noalign{\smallskip}
\hline
\end{tabular}
\end{quote}
\end{itemize}
\newpage
\begin{itemize}
\item[9)] \textbf{Literature.}
\begingroup
\def\section#1#2{}
%\def\small{}
\smallskip
%\bibliographystyle{plain}
%\bibliography{frk}
\begin{thebibliography}{10}
\bibitem{abr:ste:64}
M.~Abramowitz and I.A. Stegun, editors.
\newblock {\em Handbook of Mathematical Functions With Formulas, Graphs, and
Mathematical Tables}, volume~55 of {\em National Bureau of Standards Applied
Mathematics Series}.
\newblock United States Department of Commerce, Washington, D.C., June 1964.
\newblock 10th Printing, December 1972, with corrections.
\url{}.
\bibitem{bar:geu:01}
Henk Barendregt and Herman Geuvers.
\newblock {Proof-assistants Using Dependent Type Systems}.
\newblock In Alan Robinson and Andrei Voronkov, editors, {\em Handbook of
Automated Reasoning}. Elsevier Science Publishers B.V., 2001.
\newblock \url{}.
\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.
\newblock
\url{}.
\bibitem{bee:wie:02}
M.~Beeson and F.~Wiedijk.
\newblock {The Meaning of Infinity in Calculus and Computer Algebra Systems}.
\newblock In Jacques Calmet, Belaid Benhamou, Olga Caprotti, Laurent Henocque,
and Volker Sorge, editors, {\em Artificial Intelligence, Automated Reasoning,
and Symbolic Computatiation, Proceedings of the Joint International
Conferences, AISC 2002 and Calculemus 2002, Marseille}, volume 2385 of {\em
LNAI}, pages 246--258, 2002.
\newblock \url{}.
\bibitem{bos:can:pla:97}
Wieb Bosma, John Cannon, and Catherine Playoust.
\newblock {The Magma algebra system. I. The user language}.
\newblock {\em Journal of Symbolic Computation}, 24:235--265, 1997.
\bibitem{bou:har:hir:men:rio:99}
S.~Boulm\'e, T.~Hardin, D.~Hirschkoff, V.~M\'enissier-Morain, and R.~Rioboo.
\newblock {On the way to certify Computer Algebra Systems}.
\newblock In {\em Proceedings of the Calculemus workshop of FLOC'99 (Federated
Logic Conference, Trento, Italie)}, volume~23 of {\em ENTCS}. Elsevier, 1999.
\newblock
\url{}.
\bibitem{qed:94}
R.~Boyer et~al.
\newblock {The QED Manifesto}.
\newblock In A.~Bundy, editor, {\em Automated Deduction -- CADE 12}, volume 814
of {\em LNAI}, pages 238--251. Springer-Verlag, 1994.
\newblock \url{}.
\bibitem{bra:cor:dav:jef:wat:02}
R.J. Bradford, R.M. Corless, J.H. Davenport, D.J. Jeffrey, and S.M. Watt.
\newblock Reasoning about the elementary functions of complex analysis.
\newblock {\em Annals Maths Artificial Intelligence}, 36:303--318, 2002.
\newblock \url{}.
\bibitem{bus:cap:car:dew:gae:koh:04}
S.~Buswell, O.~Caprotti, D.P. Carlisle, M.C. Dewar, M.~Ga{\"e}tano, and
M.~Kohlhase.
\newblock {The OpenMath Standard, v.~2.0}, 2002.
\newblock \url{}.
\bibitem{cal:04}
{The CALCULEMUS Initiative}.
\newblock \url{}.
\bibitem{car:ion:min:pop:03}
David Carlisle, Patrick Ion, Robert Miner, and Nico Poppelier.
\newblock {Mathematical Markup Language (MathML) Version 2.0 (Second Edition)},
2003.
\newblock \url{}.
\bibitem{cor:dav:jef:wat:00}
R.M. Corless, J.H. Davenport, D.J. Jeffrey, and S.M. Watt.
\newblock {According to Abramowitz and Stegun}.
\newblock {\em SIGSAM Bulletin}, 34:58--65, 2000.
\newblock \url{}.
\bibitem{cru:geu:wie:04}
L.~Cruz-Filipe, H.~Geuvers, and F.~Wiedijk.
\newblock {C-CoRN: the Constructive Coq Repository at Nijmegen}.
\newblock To appear in LNCS 3119, Proceedings of MKM 2004, Bia{\l}owieza,
Poland. \url{}, 2004.
\bibitem{far:mor:03}
W.M. Farmer and M.~v. Mohrenschildt.
\newblock {An overview of a Formal Framework for Managing Mathematics}.
\newblock {\em Mathematical Knowledge Management, special issue of Annals of
Mathematics and Artificial Intelligence}, 38:165--191, 2003.
\newblock \url{}.
\bibitem{gor:mel:93}
M.J.C. Gordon and T.F. Melham, editors.
\newblock {\em Introduction to HOL}.
\newblock Cambridge University Press, Cambridge, 1993.
\bibitem{har:00}
John Harrison.
\newblock {\em The HOL Light manual (1.1)}, 2000.
\newblock \url{}.
\bibitem{koh:00}
M.~Kohlhase.
\newblock {OMDoc: Towards an Internet Standard for the Administration,
Distribution and Teaching of mathematical Knowledge}.
\newblock In Eugenio~Roanes Lozano, editor, {\em Proceedings of Artificial
Intelligence and Symbolic Computation, AISC'2000}, number 1930 in LNAI.
Springer-Verlag, 2000.
\newblock \url{}.
\bibitem{koh:04}
Michael Kohlhase.
\newblock {OMDoc, An Open Markup Format for Mathematical Documents (Version
1.2)}.
\newblock Technical report, School of Engineering and Sciences, International
University Bremen, 2004.
\newblock \url{}.
\bibitem{loz:mil:sau:99}
D.W. Lozier, B.R. Miller, and B.V. Saunders.
\newblock {Design of a Digital Mathematical Library for Science, Technology and
Education}.
\newblock In {\em {Proceedings of the IEEE Forum on Research and Technology
Advances in Digital Libraries; IEEE ADL '99, Baltimore, Maryland}}, 1999.
\newblock \url{}.
\bibitem{meu:sal:03}
Ludovic Meunier and Bruno Salvy.
\newblock {ESF: An automatically generated encyclopedia of special functions}.
\newblock In J.R. Sendra, editor, {\em Symbolic and Algebraic Computation,
Proceedings of ISSAC'03}, pages 199--205. ACM Press, 2003.
\newblock \url{}.
\bibitem{mil:you:03}
B.R. Miller and A.~Youssef.
\newblock {Technical Aspects of the Digital Library of Mathematical Functions}.
\newblock {\em Annals of Mathematics and Artificial Intelligence -- Special
Issue on Mathematical Knowledge Management}, 38:121--136, 2003.
\newblock
\url{}.
\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.
\newblock \url{}.
\bibitem{nip:pau:wen:02}
T.~Nipkow, L.C. Paulson, and M.~Wenzel.
\newblock {\em Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
volume 2283 of {\em LNCS}.
\newblock Springer, 2002.
\newblock
\url{}.
\bibitem{owr:rus:sha:92}
S.~Owre, J.~Rushby, and N.~Shankar.
\newblock {PVS: A Prototype Verification System}.
\newblock In D.~Kapur, editor, {\em 11th International Conference on Automated
Deduction (CADE)}, volume 607 of {\em LNAI}, pages 748--752, Berlin,
Heidelberg, New York, 1992. Springer-Verlag.
\newblock
\url{}.
\bibitem{coq:04}
{The Coq Development Team}.
\newblock {\em The Coq Proof Assistant Reference Manual}, 2004.
\newblock
\url{}.
\bibitem{wie:03}
F.~Wiedijk.
\newblock {Comparing mathematical provers}.
\newblock In Andrea Asperti, Bruno Buchberger, and James Davenport, editors,
{\em Mathematical Knowledge Management, Proceedings of MKM 2003}, volume 2594
of {\em LNCS}, pages 188--202. Springer, 2003.
\newblock \url{}.
\bibitem{wie:04}
F.~Wiedijk.
\newblock {Formal Proof Sketches}.
\newblock In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, {\em
Types for Proofs and Programs: Third International Workshop, TYPES 2003,
Torino, Italy, April 30 -- May 4, 2003, Revised Selected Papers}, volume 3085
of {\em LNCS}, pages 378--393, 2004.
\newblock \url{}.
\bibitem{wie:zwa:03}
F.~Wiedijk and J.~Zwanenburg.
\newblock {First Order Logic with Domain Conditions}.
\newblock In David Basin and Burkhart Wolff, editors, {\em Theorem Proving in
Higher Order Logics, Proceedings of TPHOLs 2003}, volume 2758 of {\em LNCS},
pages 221--237. Springer, 2003.
\newblock \url{}.
\end{thebibliography}
\makeatletter
\newcounter{oldenumiv}
\setcounter{oldenumiv}{\c@enumiv}
\makeatother
\def\small{}
\medskip\noindent
\textbf{Key Publications of the Research Team:}
\cite{bar:geu:01}
\cite{bee:95}
\cite{bee:wie:02}
\cite{bos:can:pla:97}
\cite{cru:geu:wie:04}
%\smallskip
%\begin{thebibliography}{1}
%\makeatletter
%\setcounter{enumiv}{\c@oldenumiv}
%\makeatother
%
%\end{thebibliography}
\endgroup
\end{itemize}
\begin{itemize}
\item[10)] \textbf{Requested Budget (in Dutch).}
\begin{flushleft}
\begin{tabular}{lclcrcrcrr}
\hline
\noalign{\smallskip}
\emph{OiO} && \emph{aanstelling} &$\quad$& 1 fte &$\times$& 157.683 &$\enskip=\enskip$& \euro{} & 157.683 \\
&& \emph{benchfee} && 1 fte &$\times$& 4.538 &$=$& \euro{} & 4.538 \\
&& \emph{additioneel reisbudget} && && && & --- \\
&& \emph{apparatuur} (incl.~BTW) && && && \euro{} & 8.250 \\
\emph{overig} && && && && & --- \\
\emph{investeringen} && && && && & --- \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
\emph{totaal} && && && && \euro{} & 170.471 \\
\noalign{\smallskip}
\hline
\end{tabular}
\end{flushleft}
\end{itemize}
\iffalse
\begin{itemize}
\item[] \textbf{Suggested Referees}
\begin{flushleft}
\begin{supertabular}{lcl}
Andrea Asperti && \emph{University of Bologna, Italy} \\
&& \url{asperti@cs.unibo.it} \\
&& \url{http://www.cs.unibo.it/~asperti/} \\
\noalign{\medskip}
James Davenport && \emph{University of Bath, UK} \\
&& \url{J.H.Davenport@bath.ac.uk} \\
&& \url{http://www.bath.ac.uk/~masjhd/} \\
\noalign{\medskip}
William M.~Farmer &$\enskip$& \emph{McMaster University, Ontario, Canada} \\
&& \url{wmfarmer@mcmaster.ca} \\
&& \url{http://imps.mcmaster.ca/wmfarmer/} \\
\noalign{\medskip}
John Harrison && \emph{Intel Corporation, Oregon, US} \\
&& \url{johnh@ichips.intel.com} \\
&& \url{http://www.cl.cam.ac.uk/users/jrh/} \\
\noalign{\medskip}
Michael Kohlhase && \emph{International University Bremen, Germany} \\
&& \url{m.kohlhase@iu-bremen.de} \\
&& \url{http://www.faculty.iu-bremen.de/mkohlhase/} \\
\noalign{\medskip}
Andrzej Trybulec && \emph{University of Bia{\l}ystok, Poland} \\
&& \url{trybulec@math.uwb.edu.pl} \\
&& \url{http://math.uwb.edu.pl/~trybulec/} \\
\noalign{\medskip}
Bernd Wegner && \emph{Technischen Universit\"at Berlin \& Zentralblatt f\"ur} \\
&& \emph{Mathematik, Germany} \\
&& \url{wegner@math.tu-berlin.de} \\
&& \url{http://www.zblmath.fiz-karlsruhe.de/people/} \\
&& \quad \url{wegner.html} \\
\end{supertabular}
\end{flushleft}
\end{itemize}
\fi
\newpage
\begin{center}
\textbf{The pages from \emph{{\aands}} containing Section 4.1}
\label{4.1-start}
\vbox to 0pt{
\medskip
$\hspace{-3cm}$\fbox{\includegraphics{/home/freek/papers/oc2004/aands/0067.eps}}$\hspace{-3cm}$
\vss
}
\end{center}
\newpage
\begin{center}
\vbox to 0pt{
$\hspace{-3cm}$\fbox{\includegraphics{/home/freek/papers/oc2004/aands/0068.eps}}$\hspace{-3cm}$
\vss
}
\end{center}
\newpage
\begin{center}
\vbox to 0pt{
$\hspace{-3cm}$\fbox{\includegraphics{/home/freek/papers/oc2004/aands/0069.eps}}$\hspace{-3cm}$
\vss
}
\label{4.1-stop}
\end{center}
\newpage
\begin{center}
\textbf{(Page 86, as Formula 4.1.40 refers to Figure 4.7)}
\vbox to 0pt{
\medskip
$\hspace{-3cm}$\fbox{\includegraphics{/home/freek/papers/oc2004/aands/0086.eps}}$\hspace{-3cm}$
\vss
}
\end{center}
\end{document}