1a) Project Title. Formalizing Elementary Analysis Rigorously. 1b) Project Acronym. F.E.A.R. 1c) Principal Investigator. Freek Wiedijk.

2a) Summary. 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 do have a precise meaning, but those often do not much resemble the formulas that one encounters in mathematical textbooks.

The F.E.A.R. project 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 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.

2b) Abstract for laymen (in Dutch). 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 bewijzen mee te verifiëren). 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 F.E.A.R. project zal een vorm ontwerpen voor formules in de computer zo dat die wèl een precieze betekenis hebben, maar tòch lijken op de traditionele formules uit de wiskundeboeken. We zullen dit doen door één van de secties uit een klassiek tabellenboek met wiskundige formules (het telefoonboek-dikke 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.

3) Classification. Multidisciplinary: computer science & mathematics.

Discipline: 6.5 Formal Methods. NOAG-i 2001-2005: Algorithms and Formal Methods (AFM). MSC2000: 03B35, 13Pxx, 26-xx, 30Dxx, 68T15.

4) Composition of the Research Team.

name specialty  university
prof. dr. H.P. Barendregt type theory  Radboud University Nijmegen

promotor

prof. dr. M.J. Beeson computer algebra San José State University

theorem proving

dr. W. Bosma computer algebra Radboud University Nijmegen
dr. J.H. Geuvers type theory  Radboud University Nijmegen

theorem proving

dr. F. Wiedijk theorem proving Radboud University Nijmegen
PhD student  Radboud University Nijmegen

5) Research Schools. Dutch Research School in Logic (OZSL), Institute for Programming research and Algorithmics (IPA), Mathematical Research Institute (MRI).

6) Description of the Proposed Research. We will first present the background of this research. For a presentation of the specifics of the project, skip to Core of the Project on page 5. When in the text below we refer to Abramowitz & Stegun, we mean the well-known Handbook of Mathematical Functions [1] by Milton Abramowitz and Irene Stegun.

The research of the F.E.A.R. project is related to two kinds of system: proof assistants (theorem proving systems) and computer algebra systems.

Proof assistants are systems for the verification of mathematical proofs with the computer. Major proof assistants are PVS, ACL2, Theorema, Ωmega, IMPS, HOL, Isabelle, Coq, NuPRL and Mizar [26]. Proof assistants have two main application areas:

• 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).

• 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 [7].

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 problems that a high school student can solve without difficulty. We call these high school problems. Examples of this kind of problem (where ⊢ denotes logical consequence) are:

n ≥ 2 , x = \frac{1}{n + 1} ⊢ \frac{x}{1 − x} < 1
x = i/n , n = m + 1 ⊢ n! · x = i · m!
\frac{k}{n} ≥ 0 ⊢ |\frac{n − k}{n} − 1| = \frac{k}{n}

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.

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:

• 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.

• 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.

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):

> value(eval(Sum(z^n/n!,n=0..infinity),z=0));

0  should be 1 (Maple simplified 0^{n} to 0)

> residue(1/(csgn(z)*z),z=0);

\frac{1}{csgn(z)}  should not have z free (z was bound)

> eval(int(1/(x-a),x=0..1),a=1/2);

πi  should not be complex (real integral)

> Int(sin(x),x=0..Pi);

∫_{0}^{π} sin(x) dx

these two integrals should be equal (change of variables) but they are not; the first is 2 but the second is 0

> student[changevar](sin(x)=t,%,t);

∫_{0}^{0} − \frac{t}{(1 − t^{2})^{\frac{1}{2}}} dt

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:

ln(∞) = ∞
∫ \frac{1}{z} dz = ln(z)

(both Mathematica and Maple calculate like this) it is not fully clear what the semantics of the symbols ∞ and ∫ are (in the second case the question is: where is the constant of integration?) In particular those symbols are not 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

\frac{x + x}{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 λx.\frac{x+x}{x} differs from the (total) function λ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.

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 [11] and OpenMath [9].

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 [28]:

1/0 = 0
PVS  not a correct formula
IMPS  negation provable
Coq  not provable, negation not provable
HOL/Mizar provable

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 the F.E.A.R. project is to design a small expression language like MathML or OpenMath, but one that has a very explicit and well-defined semantics.

This project simultaneously addresses the two problems that we noted:

• Proof assistants are not powerful enough, as they cannot do ‘high school problems’ by themselves.

• Computer algebra systems are not fully correct; worse, they even lack a semantics that makes discussion of correctness meaningful.

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 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.)

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:

• 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.

• In mathematics one often uses imprecise notations. Examples of this are calculations with ‘infinity’, indefinite integration where one omits ‘constants of integration’, ‘multivalued 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.

Core of the Project. We will formalize a section from Abramowitz & Stegun in a modern proof assistant. The expressions in the formalization will be made to resemble the original expressions as found in Abramowitz & Stegun 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.

Two choices will be made during the first phase of the project:

• Which proof assistant? The most natural choice is to take Coq [25]. In Nijmegen a large Coq library has been created [13] 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. Other possible choices would be HOL [15, 16, 23], Mizar [22] or PVS [24]. 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.

• Which section of Abramowitz & Stegun? 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 11–13. 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) = −∞ (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.

In [4] we defined a rigorous semantics for formulas in elementary analysis that contain the symbol ∞. We did this by interpreting expressions that contain this symbol as 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 [4] 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 the F.E.A.R. project 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 Abramowitz & Stegun 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 Abramowitz & Stegun are ln z = ∫_{1}^{z} \frac{dt}{t} and Ln z = ∫_{1}^{z} \frac{dt}{t}. Clearly the symbol ∫ means something different in those two formulas.

The approach that we will follow in the project is to take a MathML-like encoding of the formulas, and then systematically 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 will be non-trivial. Therefore we will build automated support for this task. In this implementation the formulas will be encoded using the Open-Math/OMDoc standard [9, 17, 18].

This project will involve work on three different levels:

• 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.

• 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.

• 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.

Related Work. Relating proof assistants to computer algebra systems is the subject of various projects, like the CALCULEMUS project [10], the FoC project [6], and the MathScheme project [14]. (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 the F.E.A.R. project.

There are projects that aim to create databases that are electronic versions of Abramowitz & Stegun, like the NIST’s Digital Library of Mathematical Functions project [19, 21] and INRIA’s Encyclopedia of Special Functions project [20] (which is part of its Algorithms Project). We could have based our project on formulas from those databases instead of on Abramowitz & Stegun. However, the formulas from those sources do not relate as much to semantics of computer algebra as the ‘informal’ formulas from Abramowitz & Stegun.

Prof. Davenport has written papers [8, 12] 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 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.

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 [13] – 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.

Some Questions & Answers. Is this project about mathematics or about computer science? 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 not trivial.)

In computer science, proof assistants are an important tool in the field of 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.

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? Formalizing the 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 Abramowitz & Stegun (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.

Aiming for large-scale formalization of mathematics is rather utopian: why should we support a project that reaches for such a far-away goal? The goal of the project is to improve proof assistants and computer algebra systems. Using proof assistants for checking mathematics is only 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.

Abramowitz & Stegun is not real mathematics, but ‘mathematics for engineers’: surely it is not important to mimic this style of doing calculus? The way Abramowitz & Stegun 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.

Another reason for following the ‘informal’ way of doing calculus from Abramowitz & Stegun 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 Abramowitz & Stegun: we want to improve the proof assistants in such a way that they become more attractive to mathematicians [27].

Elementary analysis is basic mathematics: surely for a competent mathematician it is a triviality to represent this kind of formulas? 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.

Why won’t the project aim at formalizing the proofs too? Although the formulas from Abramowitz & Stegun 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 will formalize some of the proofs, we just do not want to take the time to formalize all proofs.)

NIST is currently creating a database called the Digital Library of Mathematical Functions. That is a formal version of Abramowitz & Stegun, isn’t it? So hasn’t your project already been done by them? The database that is being created by NIST will serve a similar purpose as Abramowitz & Stegun, but it is not a direct translation. Therefore it will not need to have counterparts to the informal formulas that one finds in Abramowitz & Stegun and in computer algebra (like ln(∞) = ∞). 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 ∫ \frac{1}{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.

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? The reason that those formulas look different from the formulas of informal calculus is that it is hard to make them look similar. The people who did those formalizations were only interested in the 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.

7) Work Programme.

year 1  year 2  year 3  year 4 getting acquainted mathematical description formalization  OpenMath conversion investigating extensions conference papers  writing thesis

year 1 Getting acquainted with the relevant proof assistants. Getting

acquainted with the relevant mathematics.

year 1–2 Abstract mathematical description of signature & semantics.

year 2–3 Formalization of signature/definitions in the primary proof as-

sistant.

year 3 Definition of OpenMath CD for the signature. Implementation of conversion from OMDoc to input format of the primary proof assistant.

year 3–4 Investigation of the effort needed to complete the formalization with proofs. Investigation of the effort needed to treat other sections in Abramowitz & Stegun similarly. Investigation of the effort needed for formalization in other proof assistants.

year 1–3 Papers in conferences or workshops.
year 3–4 Writing the thesis.

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.

8) 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.

hardware dual processor system  5,000
maintenance contract  360
software license, Magma version 2.11  950
license, Maple version 9.5  400
license, Mathematica version 5.1  1,460
license, MathXpert version 3  80
total  8,250

9) Literature.

1. M. Abramowitz and I.A. Stegun, editors. Handbook of Mathematical Functions With Formulas, Graphs, and Mathematical Tables, volume 55 of National Bureau of Standards Applied Mathematics Series. United States Department of Commerce, Washington, D.C., June 1964. 10th Printing, December 1972, with corrections. <http://www.math.sfu.ca/~cbm/aands/>.

2. Henk Barendregt and Herman Geuvers. Proof-assistants Using Dependent Type Systems. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier

Science Publishers B.V., 2001. <ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBKassistants.
ps>.

3. M. Beeson. Using Nonstandard Analysis to Ensure the Correctness of Symbolic Computations. International Journal of Foundations of Computer Science, 6(3):299–338, 1995.

<http://www.mathcs.sjsu.edu/faculty/beeson/Papers/nsappt.ps.gz>.

4. M. Beeson and F. Wiedijk. The Meaning of Infinity in Calculus and Computer Algebra Systems. In Jacques Calmet, Belaid Benhamou, Olga Caprotti, Laurent Henocque, and Volker Sorge, editors, Artificial Intelligence, Automated Reasoning, and Symbolic Computatiation, Proceedings of the Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, volume 2385 of LNAI, pages 246–258, 2002. <http://www.cs.ru.nl/~freek/pubs/

limits.ps.gz>.

5. Wieb Bosma, John Cannon, and Catherine Playoust. The Magma algebra system. I. The user language. Journal of Symbolic Computation, 24:235–265, 1997.

6. S. Boulmé, T. Hardin, D. Hirschkoff, V. Ménissier-Morain, and R. Rioboo. On the way to certify Computer Algebra Systems. In Proceedings of the Calculemus workshop of FLOC’99 (Federated Logic Conference, Trento, Italie), volume 23 of ENTCS. Elsevier, 1999. <http:

//www1.elsevier.com/gej-ng/31/29/23/92/36/32/tcs23.3.006.ps>.

7. R. Boyer et al. The QED Manifesto. In A. Bundy, editor, Automated Deduction – CADE 12, volume 814 of LNAI, pages 238–251. Springer-Verlag, 1994. <http://www.cs.ru.nl/~freek/

qed/qed.ps.gz>.

8. R.J. Bradford, R.M. Corless, J.H. Davenport, D.J. Jeffrey, and S.M. Watt. Reasoning about the elementary functions of complex analysis. Annals Maths Artificial Intelligence, 36:303–

318, 2002. <http://www.apmaths.uwo.ca/~djeffrey/Offprints/AMAI.ps>.

9. S. Buswell, O. Caprotti, D.P. Carlisle, M.C. Dewar, M. Gaëtano, and M. Kohlhase. The Open-

Math Standard, v. 2.0, 2002. <http://www.openmath.org/cocoon/openmath/standard/>.
10. The CALCULEMUS Initiative. <http://www.calculemus.net/>.

11. David Carlisle, Patrick Ion, Robert Miner, and Nico Poppelier. Mathematical Markup Language (MathML) Version 2.0 (Second Edition), 2003. <http://www.w3.org/TR/MathML2/>.

12. R.M. Corless, J.H. Davenport, D.J. Jeffrey, and S.M. Watt. According to Abramowitz and Stegun. SIGSAM Bulletin, 34:58–65, 2000. <http://www.apmaths.uwo.ca/~djeffrey/

Offprints/couth.pdf>.

13. L. Cruz-Filipe, H. Geuvers, and F. Wiedijk. C-CoRN: the Constructive Coq Repository at Nijmegen. To appear in LNCS 3119, Proceedings of MKM 2004, Białowieza, Poland.

<http://www.cs.ru.nl/~lcf/pubs/paper5.ps>, 2004.

14. W.M. Farmer and M. v. Mohrenschildt. An overview of a Formal Framework for Managing Mathematics. Mathematical Knowledge Management, special issue of Annals of Mathematics and Artificial Intelligence, 38:165–191, 2003. <http://imps.mcmaster.ca/doc/

ffmm-overview.ps>.

15. M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL. Cambridge University Press, Cambridge, 1993.

16. John Harrison. The HOL Light manual (1.1), 2000. <http://www.cl.cam.ac.uk/users/jrh/

hol-light/manual-1.1.ps.gz>.

17. M. Kohlhase. OMDoc: Towards an Internet Standard for the Administration, Distribution and Teaching of mathematical Knowledge. In Eugenio Roanes Lozano, editor, Proceedings of Artificial Intelligence and Symbolic Computation, AISC’2000, number 1930 in LNAI. Springer-

Verlag, 2000. <http://www.faculty.iu-bremen.de/mkohlhase/papers/aisc.ps>.

18. Michael Kohlhase. OMDoc, An Open Markup Format for Mathematical Documents (Version 1.2). Technical report, School of Engineering and Sciences, International University Bremen,

2004. <http://www.mathweb.org/omdoc/omdoc1.2.ps>.

19. D.W. Lozier, B.R. Miller, and B.V. Saunders. Design of a Digital Mathematical Library for Science, Technology and Education. In Proceedings of the IEEE Forum on Research and Technology Advances in Digital Libraries; IEEE ADL ’99, Baltimore, Maryland, 1999.

<http://dlmf.nist.gov/about/publications/nistir6297.ps.gz>.

20. Ludovic Meunier and Bruno Salvy. ESF: An automatically generated encyclopedia of special functions. In J.R. Sendra, editor, Symbolic and Algebraic Computation, Proceedings of

ISSAC’03, pages 199–205. ACM Press, 2003. <http://algo.inria.fr/meunier/articles/
MeSa03.ps>.

21. B.R. Miller and A. Youssef. Technical Aspects of the Digital Library of Mathematical Functions. Annals of Mathematics and Artificial Intelligence – Special Issue on Mathematical

Knowledge Management, 38:121–136, 2003. <http://dlmf.nist.gov/about/publications/
MKM-Miller-Youssef.ps.gz>.

22. M. Muzalewski. An Outline of PC Mizar. Fondation Philippe le Hodey, Brussels, 1993.

<http://www.cs.ru.nl/~freek/mizar/mizarmanual.ps.gz>.

23. T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. <http://www.cl.cam.ac.uk/Research/

HVG/Isabelle/dist/Isabelle2004/doc/tutorial.pdf>.

24. S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of LNAI, pages 748–752, Berlin, Heidelberg, New York, 1992. Springer-Verlag. <http://www.csl.sri.

com/papers/c/a/cade92-pvs/cade92-pvs.ps.gz>.

25. The Coq Development Team. The Coq Proof Assistant Reference Manual, 2004. <ftp:

//ftp.inria.fr/INRIA/coq/current/doc/Reference-Manual.ps.gz>.

26. F. Wiedijk. Comparing mathematical provers. In Andrea Asperti, Bruno Buchberger, and James Davenport, editors, Mathematical Knowledge Management, Proceedings of MKM 2003, volume 2594 of LNCS, pages 188–202. Springer, 2003. <http://www.cs.ru.nl/~freek/

comparison/diffs.ps.gz>.

27. F. Wiedijk. Formal Proof Sketches. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs: Third International Workshop, TYPES 2003, Torino, Italy, April 30 – May 4, 2003, Revised Selected Papers, volume 3085 of LNCS, pages 378–393,

2004. <http://www.cs.ru.nl/~freek/pubs/sketches2.ps.gz>.

28. F. Wiedijk and J. Zwanenburg. First Order Logic with Domain Conditions. In David Basin and Burkhart Wolff, editors, Theorem Proving in Higher Order Logics, Proceedings of TPHOLs 2003, volume 2758 of LNCS, pages 221–237. Springer, 2003. <http:

//www.cs.ru.nl/~freek/pubs/partial.ps.gz>.

Key Publications of the Research Team: [2] [3] [4] [5] [13]

10) Requested Budget (in Dutch).

OiO  aanstelling  1 fte × 157.683 = 157.683
benchfee  1 fte × 4.538 =  4.538
additioneel reisbudget  —
apparatuur (incl. BTW)  8.250
overig  —
investeringen  —
totaal  170.471

The pages from Abramowitz & Stegun containing Section 4.1

12  F. Wiedijk

The F.E.A.R. project  13

(Page 86, as Formula 4.1.40 refers to Figure 4.7)