diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 2472ed4..4dbb5c8 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -216,6 +216,19 @@ in Watt [Wat91], pp241-246 ISBN 0-89791-437-6 LCCN QA76.95.I59 1991
In S.Watt, editor, {\sl Proceedings of ISSAC'91},
pages 241-246, ACM Press, 1991.
+\bibitem[Bronstein 91c]{Bro91c} Bronstein, Manual\\
+``Computer Algebra and Indefinite Integrals''\\
+%\verb|axiom-developer.org/axiom-website/papers/Bro91c.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We give an overview, from an analytical point of view, of decision
+procedures for determining whether an elementary function has an
+elementary function has an elementary antiderivative. We give examples
+of algebraic functions which are integrable and non-integrable in
+closed form, and mention the current implementation of various computer
+algebra systems.
+\end{adjustwidth}
+
\bibitem[Bronstein 92]{Bro92} Bronstein, M.\\
``Linear Ordinary Differential Equations: breaking through the order 2 barrier''\\
\verb|www-sop.inria.fr/cafe/Manuel.Bronstein/publications/issac92.ps.gz|
@@ -794,6 +807,31 @@ Naciri, Hanane\\
``Multi-values Computer Algebra''\\
ISSN 0249-6399 Institut National De Recherche en Informatique et en
Automatique Sept. 2000 No. 4001
+\verb|hal.inria.fr/inria-00072643/PDF/RR-4401.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/FDN00b.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+One of the main strengths of computer algebra is being able to solve a family
+of problems with one computation. In order to express not only one problem
+but a family of problems, one introduces some symbols which are in fact the
+parameters common to all the problems of the family.
+
+The user must be able to understand in which way these parameters
+affect the result when he looks at the answer. Otherwise it may lead
+to completely wrong calculations, which when used for numerical
+applications bring nonsensical answers. This is the case in most
+current Computer Algebra Systems we know because the form of the
+answer is never explicitly conditioned by the values of the
+parameters. The user is not even informed that the given answer may be
+wrong in some cases then computer algebra systems can not be entirely
+trustworthy. We have introduced multi-valued expressions called {\sl
+conditional} expressions, in which each potential value is associated
+with a condition on some parameters. This is used, in particular, to
+capture the situation in integration, where the form of the answer can
+depend on whether certain quantities are positive, negative or
+zero. We show that it is also necessary when solving modular linear
+equations or deducing congruence conditions from complex expressions.
+\end{adjustwidth}
\bibitem[Fitch 84]{Fit84} Fitch, J. P. (ed)\\
EUROSAM '84: International Symposium on Symbolic and
@@ -901,7 +939,23 @@ In Fitch [Fit93], pp193-202. ISBN 0-387-57272-4 (New York),
\bibitem[Gottliebsen 05]{GKM05} Gottliebsen, Hanne; Kelsey, Tom;
Martin, Ursula\\
``Hidden verification for computational mathematics''\\
-Journal of Symbolic Computation, Vol39, Num 5, 2005
+Journal of Symbolic Computation, Vol39, Num 5, pp539-567 (2005)\\
+\verb|www.sciencedirect.com/science/article/pii/S0747717105000295|
+%\verb|axiom-developer.org/axiom-website/papers/GKM05.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We present hidden verification as a means to make the power of
+computational logic available to users of computer algebra systems
+while shielding them from its complexity. We have implemented in PVS a
+library of facts about elementary and transcendental function, and
+automatic procedures to attempt proofs of continuity, convergence and
+differentiability for functions in this class. These are called
+directly from Maple by a simple pipe-lined interface. Hence we are
+able to support the analysis of differential equations in Maple by
+direct calls to PVS for: result refinement and verification, discharge
+of verification conditions, harnesses to ensure more reliable
+differential equation solvers, and verifiable look-up tables.
+\end{adjustwidth}
\bibitem[Grabe 98]{Gra98} Gr\"abe, Hans-Gert\\
``About the Polynomial System Solve Facility of Axiom, Macyma, Maple
@@ -1009,6 +1063,11 @@ implemented in a symbolic manipulation system.
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibitem[Boyle 88]{Boyl88} Boyle, Ann\\
+``Future Directions for Research in Symbolic Computation''\\
+\verb|www.eecis.udel.edu/~caviness/wsreport.pdf|
+%\verb|axiom-developer.org/axiom-website/Boyl88.pdf|
+
\bibitem[Hassner 87]{HBW87} Hassner, Martin; Burge, William H.;
Watt, Stephen M.\\
``Construction of Algebraic Error Control Codes (ECC) on the Elliptic
@@ -2794,6 +2853,11 @@ Numerical Algorithms Group, Inc., Downer's
Grove, IL, USA and Oxford, UK, 1992\\
\verb|www.nag.co.uk/doc/TechRep/axiomtr.html|
+\bibitem[Granville 1911]{Gran1911} Granville, William Anthony\\
+``Elements of the Differential and Integral Calculus''\\
+\verb|djm.cc/library/Elements_Differential_Integral_Calculus_Granville_edited_2.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Gran1911.pdf|
+
\bibitem[Gruntz 93]{Gru93} Gruntz, Dominik\\
``Limit computation in computer algebra''\\
\verb|algo.inria.fr/seminars/sem92-93/gruntz.pdf|
@@ -3207,7 +3271,12 @@ ACM Trans. Math. Softw. 5 118--125. (1979)
\subsection{O} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\bibitem[NIST10]{NIST10} Olver, Frank W.; Lozier, Daniel W.;
+\bibitem[Ollagnier 94]{Olla94} Ollagnier, Jean Moulin\\
+``Algorithms and methods in differential algebra''\\
+\verb|www.lix.polytechnique.fr/~moulin/papiers/atelier.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Olla94.pdf|
+
+\bibitem[Olver 10]{NIST10} Olver, Frank W.; Lozier, Daniel W.;
Boisvert, Ronald F.; Clark, Charles W. (ed)\\
``NIST Handbook of Mathematical Functions''\\
(2010) Cambridge University Press ISBN 978-0-521-19225-5
@@ -3411,6 +3480,24 @@ Rocky Mountain J. Math. 14 223--237. (1984)
``Free Lie Algebras''\\
Oxford University Press, June 1993 ISBN 0198536798
+\bibitem[Rich xx]{Rixx} Rich, A.D.; Jeffrey, D.J.\\
+``Crafting a Repository of Knowledge Based on Transformation''\\
+\verb|www.apmaths.uwo.ca/~djeffrey/Offprints/IntegrationRules.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Rixx.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We describe the development of a repository of mathematical knowledge
+based on transformation rules. The specific mathematical problem is
+indefinite integration. It is important that the repository be not
+confused with a look-up table. The database of transformation rules is
+at present encoded in Mathematica, but this is only one convenient
+form of the repository, and it could be readily translated into other
+formats. The principles upon which the set of rules is compiled is
+described. One important principle is minimality. The benefits of the
+approach are illustrated with examples, and with the results of
+comparisons with other approaches.
+\end{adjustwidth}
+
\bibitem[Rich 10]{Ri10} Rich, Albert D.\\
``Rule-based Mathematics''\\
\verb|www.apmaths.uwo.ca/~arich|
@@ -3811,8 +3898,28 @@ to the techniques of artificial intelligence and theorem proving than
the original problem of complex-variable analysis.
\end{adjustwidth}
+\bibitem[Ng 68]{Ng68} Ng, Edward W.; Geller, Murray\\
+``A Table of Integrals of the Error functions''\\
+\verb|nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn1p1_A1b.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Ng68.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This is a compendium of indefinite and definite integrals of products
+of the Error functions with elementary and transcendental functions.
+\end{adjustwidth}
+
\subsubsection{Exponential Integral $E_1(x)$} %%%%%%%%%%%%%%%%%%%%%%%%%
+\bibitem[Geller 69]{Gell69} Geller, Murray; Ng, Edward W.\\
+``A Table of Integrals of the Exponential Integral''\\
+\verb|nvlpubs.nist.gov/nistpubs/jres/73B/jresv73Bn3p191_A1b.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Gell69.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+This is a compendium of indefinite and definite integrals of products
+of the Exponential Integral with elementary or transcendental functions.
+\end{adjustwidth}
+
\bibitem[Segletes 98]{Se98} Segletes, S.B.\\
``A compact analytical fit to the exponential integral $E_1(x)$\\
Technical Report ARL-TR-1758, U.S. Army Ballistic Research Laboratory,\\
@@ -4049,6 +4156,74 @@ for rigorous results.
\subsection{Proving Axiom Correct} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibitem[Adams 99]{Adam99} Adams, A.A.; Gottlieben, H.; Linton, S.A.;
+Martin, U.\\
+``Automated theorem proving in support of computer algebra:''\\
+`` symbolic definite integration as a case study''\\
+%\verb|axiom-developer.org/axiom-website/papers/Adam99.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We assess the current state of research in the application of computer
+aided formal reasoning to computer algebra, and argue that embedded
+verification support allows users to enjoy its benefits without
+wrestling with technicalities. We illustrate this claim by considering
+symbolic definite integration, and present a verifiable symbolic
+definite integral table look up: a system which matches a query
+comprising a definite integral with parameters and side conditions,
+against an entry in a verifiable table and uses a call to a library of
+lemmas about the reals in the theorem prover PVS to aid in the
+transformation of the table entry into an answer. We present the full
+model of such a system as well as a description of our prototype
+implementation showing the efficacy of such a system: for example, the
+prototype is able to obtain correct answers in cases where computer
+algebra systems [CAS] do not. We extend upon Fateman's web-based table
+by including parametric limits of integration and queries with side
+conditions.
+\end{adjustwidth}
+
+\bibitem[Adams 01]{Adam01} Adams, Andrew; Dunstan, Martin; Gottliebsen, Hanne;
+Kelsey, Tom; Martin, Ursula; Owre, Sam\\
+``Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS''\\
+\verb|www.csl.sri.com/~owre/papers/tphols01/tphols01.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Adam01.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We describe an interface between version 6 of the Maple computer
+algebra system with the PVS automated theorem prover. The interface is
+designed to allow Maple users access to the robust and checkable proof
+environment of PVS. We also extend this environment by the provision
+of a library of proof strategies for use in real analysis. We
+demonstrate examples using the interface and the real analysis
+library. These examples provide proofs which are both illustrative and
+applicable to genuine symbolic computation problems.
+\end{adjustwidth}
+
+\bibitem[Ballarin 99]{Ball99} Ballarin, Clemens; Paulson, Lawrence C.\\
+``A Pragmatic Approach to Extending Provers by Computer Algebra -- with Applications to Coding Theory''\\
+\verb|www.cl.cam.ac.uk/~lp15/papers/Isabelle/coding.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Ball99.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+The use of computer algebra is usually considered beneficial for
+mechanised reasoning in mathematical domains. We present a case study,
+in the application domain of coding theory, that supports this claim:
+the mechanised proofs depend on non-trivial algorithms from computer
+algebra and increase the reasoning power of the theorem prover.
+
+The unsoundness of computer algebra systems is a major problem in
+interfacing them to theorem provers. Our approach to obtaining a sound
+overall system is not blanket distrust but based on the distinction
+between algorithms we call sound and {\sl ad hoc} respectively. This
+distinction is blurred in most computer algebra systems. Our
+experimental interface therefore uses a computer algebra library. It
+is based on formal specifications for the algorithms, and links the
+computer algebra library Sumit to the prover Isabelle.
+
+We give details of the interface, the use of the computer algebra
+system on the tactic-level of Isabelle and its integration into proof
+procedures.
+\end{adjustwidth}
+
\bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre\\
``Interactive Theorem Proving and Program Development''\\
Springer ISBN 3-540-20854-2
@@ -4676,6 +4851,7 @@ only linear computations.
``On Solutions of Linear Ordinary Differential Equations in their
Coefficient Field''\\
\verb|www-sop.inria.fr/cafe/Manuel.Bronstein/publications/mb_papers.html|
+%\verb|axiom-developer.org/axiom-website/papers/Bro90.pdf|
\begin{adjustwidth}{2.5em}{0pt}
We describe a rational algorithm for finding the denominator of any
@@ -4808,6 +4984,24 @@ to show that all the solutions of a factor of such a system can be
completed to solutions of the original system.
\end{adjustwidth}
+\bibitem[Singer 9]{Sing91.pdf} singer, Michael F.\\
+``Liouvillian Solutions of Linear Differential Equations with Liouvillian Coefficients''\\
+J. Symbolic Computation V11 No 3 pp251-273 (1991)\\
+\verb|www.sciencedirect.com/science/article/pii/S074771710880048X|
+%\verb|axiom-developer.org/axiom-website/papers/Sing91.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Let $L(y)=b$ be a linear differential equation with coefficients in a
+differential field $K$. We discuss the problem of deciding if such an
+equation has a non-zero solution in $K$ and give a decision procedure
+in case $K$ is an elementary extension of the field of rational
+functions or is an algebraic extension of a transcendental liouvillian
+extension of the field of rational functions We show how one can use
+this result to give a procedure to find a basis for the space of
+solutions, liouvillian over $K$, of $L(y)=0$ where $K$ is such a field
+and $L(y)$ has coefficients in $K$.
+\end{adjustwidth}
+
\bibitem[Von Mohrenschildt 94]{Mohr94} Von Mohrenschildt, Martin\\
``Symbolic Solutions of Discontinuous Differential Equations''\\
\verb|e-collection.library.ethz.ch/eserv/eth:39463/eth-39463-01.pdf|
@@ -4875,6 +5069,11 @@ implementations of simplification routines.
\subsection{Integration} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibitem[Adamchik xx]{Adamxx} Adamchik, Victor\\
+``Definite Integration''\\
+\verb|www.cs.cmu.edu/~adamchik/articles/integr/mj.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Adamxx.pdf|
+
\bibitem[Adamchik 97]{Adam97} Adamchik, Victor\\
``A Class of Logarithmic Integrals''\\
\verb|www.cs.cmu.edu/~adamchik/articles/issac/issac97.pdf|
@@ -4887,6 +5086,26 @@ derivatives of the Hurwitz Zeta function. Some special cases for which
such derivatives can be expressed in closed form are also considered.
\end{adjustwidth}
+\bibitem[Avgoustis 77]{Avgo77} Avgoustis, Ioannis Dimitrios\\
+``Definite Integration using the Generalized Hypergeometric Functions''\\
+\verb|dspace.mit.edu/handle/1721.1/16269|
+%\verb|axiom-developer.org/axiom-websitep/papers/Avgo77.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+A design for the definite integration of approximately fifty Special
+Functions is described. The Generalized Hypergeometric Functions are
+utilized as a basis for the representation of the members of the above
+set of Special Functions. Only a relatively small number of formulas
+that generally involve Generalized Hypergeometric Functions are
+utilized for the integration stage. A last and crucial stage is
+required for the integration process: the reduction of the Generalized
+Hypergeometric Function to Elementary and/or Special Functions.
+
+The result of an early implementation which involves Laplace
+transforms are given and some actual examples with their corresponding
+timing are provided.
+\end{adjustwidth}
+
\bibitem[Baddoura 89]{Bad89} Baddoura, Jamil\\
``A Dilogarithmic Extension of Liouville's Theorem on Integration in Finite Terms''\\
\verb|www.dtic.mil/dtic/tr/fulltext/u2/a206681.pdf|
@@ -4917,6 +5136,22 @@ functions by taking transcendental exponentials, dilogarithms, and
logarithms.
\end{adjustwidth}
+\bibitem[Baddoura 10]{Bad10} Baddoura, Jamil\\
+``A Note on Symbolic Integration with Polylogarithms''\\
+J. Math Vol 8 pp229-241 (2011)
+%\verb|axiom-developer.org/axiom-website/papers/Bad10.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We generalize partially Liouville's theorem on integration in finite
+terms to allow polylogarithms of any order to occur in the integral in
+addition to elementary functions. The result is a partial
+generalization of a theorem proved by the author for the
+dilogarithm. It is also a partial proof of a conjecture postulated by
+the author in 1994. The basic conclusion is that an associated
+function to the nth polylogarithm appears linearly with logarithms
+appearing possibly in a polynomial way with non-constant coefficients.
+\end{adjustwidth}
+
\bibitem[Bajpai 70]{Bajp70} Bajpai, S.D.\\
``A contour integral involving legendre polynomial and Meijer's G-function''\\
\verb|link.springer.com/article/10.1007/BF03049565|
@@ -4946,6 +5181,20 @@ the integrand, and to check a necessary condition for elementary
integrability.
\end{adjustwidth}
+\bibitem[Bronstein 90]{Bro90b} Bronstein, Manuel\\
+``A Unification of Liouvillian Extensions''\\
+%\verb|axiom-developer.org/axiom-website/papers/Bro90b.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+We generalize Liouville's theory of elementary functions to a larger
+class of differential extensions. Elementary, Liouvillian and
+trigonometric extensions are all special cases of our extensions. In
+the transcendental case, we show how the rational techniques of
+integration theory can be applied to our extensions, and we give a
+unified presentation which does not require separate cases for
+different monomials.
+\end{adjustwidth}
+
\bibitem[Bronstein 97]{Bro97} Bronstein, M.\\
``Symbolic Integration I--Transcendental Functions.''\\
Springer, Heidelberg, 1997 ISBN 3-540-21493-3\\
@@ -5085,6 +5334,18 @@ the variable of integration.
``On the Parallel Risch Algorithm (III): Use of Tangents''\\
SIGSAM V16 no. 3 pp3-6 August 1982
+\bibitem[Davenport 03]{Dav03} Davenport, James H.\\
+``The Difficulties of Definite Integration''\\
+\verb|www.researchgate.net/publication/|\\
+\verb|247837653_The_Diculties_of_Definite_Integration/file/72e7e52a9b1f06e196.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Dav03.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Indefinite integration is the inverse operation to differentiation,
+and, before we can understand what we mean by indefinite integration,
+we need to understand what we mean by differentiation.
+\end{adjustwidth}
+
\bibitem[Fateman 02]{Fat02} Fateman, Richard\\
``Symbolic Integration''\\
\verb|inst.eecs.berkeley.edu/~cs282/sp02/lects/14.pdf|
@@ -5265,6 +5526,20 @@ College Mathematics Journal Vol 25 No 4 (1994) pp295-308\\
\verb|www.rangevoting.org/MarchisottoZint.pdf|
%\verb|axiom-developer.org/axiom-website/papers/Marc94.pdf|
+\bibitem[Marik 91]{Mari91} Marik, Jan\\
+``A note on integration of rational functions''\\
+\verb|dml.cz/bitstream/handle/10338.dmlcz/126024/MathBohem_116-1991-4_9.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Mari91.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Let $P$ and $Q$ be polynomials in one variable with complex coefficients
+and let $n$ be a natural number. Suppose that $Q$ is not constant and
+has only simple roots. Then there is a rational function $\varphi$
+with $\varphi^\prime=P/Q^{n+1}$ if and only if the Wronskian of the
+functions $Q^\prime$, $(Q^2)^\prime,\ldots\,(Q^n)^\prime$,$P$ is
+divisible by $Q$.
+\end{adjustwidth}
+
\bibitem[Moses 76]{Mos76} Moses, Joel\\
``An introduction to the Risch Integration Algorithm''\\
ACM Proc. 1976 annual conference pp425-428
@@ -5303,6 +5578,62 @@ finding the definite integral are also described.
d'expressions''\\
Comm. Math. Helv., Vol 18 pp 283-308, (1946)
+\bibitem[Raab 12]{Raab12} Raab, Clemens G.\\
+``Definite Integration in Differential Fields''\\
+\verb|www.risc.jku.at/publications/download/risc_4583/PhD_CGR.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Raab12.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+The general goal of this thesis is to investigate and develop computer
+algebra tools for the simplification resp. evaluation of definite
+integrals. One way of finding the value of a def- inite integral is
+via the evaluation of an antiderivative of the integrand. In the
+nineteenth century Joseph Liouville was among the first who analyzed
+the structure of elementary antiderivatives of elementary functions
+systematically. In the early twentieth century the algebraic structure
+of differential fields was introduced for modeling the differential
+properties of functions. Using this framework Robert H. Risch
+published a complete algorithm for transcendental elementary
+integrands in 1969. Since then this result has been extended to
+certain other classes of integrands as well by Michael F. Singer,
+Manuel Bronstein, and several others. On the other hand, if no
+antiderivative of suitable form is available, then linear relations
+that are satisfied by the parameter integral of interest may be found
+based on the principle of parametric integration (often called
+differentiating under the integral sign or creative telescoping).
+
+The main result of this thesis extends the results mentioned above to
+a complete algo- rithm for parametric elementary integration for a
+certain class of integrands covering a majority of the special
+functions appearing in practice such as orthogonal polynomials,
+polylogarithms, Bessel functions, etc. A general framework is provided
+to model those functions in terms of suitable differential fields. If
+the integrand is Liouvillian, then the present algorithm considerably
+improves the efficiency of the corresponding algorithm given by Singer
+et al. in 1985. Additionally, a generalization of Czichowski’s
+algorithm for computing the logarithmic part of the integral is
+presented. Moreover, also partial generalizations to include other
+types of integrands are treated.
+
+As subproblems of the integration algorithm one also has to find
+solutions of linear or- dinary differential equations of a certain
+type. Some contributions are also made to solve those problems in our
+setting, where the results directly dealing with systems of
+differential equations have been joint work with Moulay A. Barkatou.
+
+For the case of Liouvillian integrands we implemented the algorithm in
+form of our Mathematica package Integrator. Parts of the
+implementation also deal with more general functions. Our procedures
+can be applied to a significant amount of the entries in integral
+tables, both indefinite and definite integrals. In addition, our
+procedures have been successfully applied to interesting examples of
+integrals that do not appear in these tables or for which current
+standard computer algebra systems like Mathematica or Maple do not
+succeed. We also give examples of how parameter integrals coming from
+the work of other researchers can be solved with the software, e.g.,
+an integral arising in analyzing the entropy of certain processes.
+\end{adjustwidth}
+
\bibitem[Raab 13]{Raab13} Raab, Clemens G.\\
``Generalization of Risch's Algorithm to Special Functions''\\
\verb|arxiv.org/pdf/1305.1481.pdf|
@@ -5349,6 +5680,24 @@ example, this means that
can be computed without including log(x) in the differential field.
\end{adjustwidth}
+\bibitem[Rich 09]{Rich09} Rich, A.D.; Jeffrey, D.J.\\
+``A Knowledge Repository for Indefinite Integration Based on Transformation Rules''\\
+\verb|www.apmaths.uwo.ca/~arich/A%2520Rule-based%2520Knowedge%2520Repository.pdf|
+%\verb|axiom-developer.org/axiom-website/papers/Rich09.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+Taking the specific problem domain of indefinite integration, we
+describe the on-going development of a repository of mathematical
+knowledge based on transformation rules. It is important that the
+repository be not confused with a look-up table. The database of
+transformation rules is at present encoded in Mathematica, but this is
+only one convenient form of the repository, and it could be readily
+translated into other formats. The principles upon which the set of
+rules is compiled is described. One important principle is
+minimality. The benefits of the approach are illustrated with
+examples, and with the results of comparisons with other approaches.
+\end{adjustwidth}
+
\bibitem[Risch 68]{Ris68} Risch, Robert\\
``On the integration of elementary functions
which are built up using algebraic operations''\\
@@ -5420,10 +5769,63 @@ simplicity and generalization.
{\sl American Mathematical Monthly}, 79:963-972, 1972
%\verb|axiom-developer.org/axiom-website/papers/Ro72.pdf|
-\bibitem[Rothstein 76]{Ro76} Rosenlicht, Maxwell\\
+\bibitem[Rothstein 76]{Ro76} Rothstein, Michael\\
``Aspects of symbolic integration and simplifcation of exponential
and primitive functions''\\
PhD thesis, University of Wisconsin-Madison (1976)
+\verb|www.cs.kent.edu/~rothstei/dis.pdf|
+#\verb|axiom-developer.org/axiom-website/papers/Ro76.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+In this thesis we cover some aspects of the theory necessary to obtain
+a canonical form for functions obtained by integration and
+exponentiation from the set of rational functions.
+
+These aspects include a new algorithm for symbolic integration of
+functions involving logarithms and exponentials which avoids
+factorization of polynomials in those cases where algebraic extension
+of the constant field is not required, avoids partial fraction
+decompositions, and only solves linear systems with a small number of
+unknowns.
+
+We have also found a theorem which states, roughly speaking, that if
+integrals which can be represented as logarithms are represented as
+such, the only algebraic dependence that a new exponential or
+logarithm can satify is given by the law of exponents or the law of
+logarithms.
+\end{adjustwidth}
+
+\bibitem[Rothstein 76a]{Ro76a} Rothstein, Michael; Caviness, B.F.\\
+``A structure theorem for exponential and primitive functions: a preliminary report''\\
+ACM Sigsam Bulletin Vol 10 Issue 4 (1976)
+%\verb|axiom-developer.org/axiom-website/papers/Ro76a.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+In this paper a generalization of the Risch Structure Theorem is reported.
+The generalization applies to fields $F(t_1,\ldots,t_n)$ where $F$
+is a differential field (in our applications $F$ will be a finitely
+generated extension of $Q$, the field of rational numbers) and each $t_i$
+is either algebraic over $F_{i-1}=F(t_1,\ldots,t_{i-1}), is an exponential
+of an element in $F_{i-1}$, or is an integral of an element in $F_{i-1}$.
+If $t_i$ is an integral and can be expressed using logarithms, it must be
+so expressed for the generalized structure theorem to apply.
+\end{adjustwidth}
+
+\bibitem[Rothstein 76b]{Ro76b} Rothstein, Michael; Caviness, B.F.\\
+``A structure theorem for exponential and primitive functions''\\
+SIAM J. Computing Vol 8 No 3 (1979)
+%\verb|axiom-developer.org/axiom-website/papers/Ro76b.pdf|
+
+\begin{adjustwidth}{2.5em}{0pt}
+In this paper a new theorem is proved that generalizes a result of
+Risch. The new theorem gives all the possible algebraic relationships
+among functions that can be built up from the rational functions by
+algebraic operations, by taking exponentials, and by integration. The
+functions so generated are called exponential and primitive functions.
+From the theorem an algorithm for determining algebraic dependence
+among a given set of exponential and primitive functions is derived.
+The algorithm is then applied to a problem in computer algebra.
+\end{adjustwidth}
\bibitem[Rothstein 77]{Ro77} Rothstein, Michael\\
``A new algorithm for the integration of
diff --git a/changelog b/changelog
index cc966a4..17ac1bb 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140808 tpd src/axiom-website/patches.html 20140808.01.tpd.patch
+20140808 tpd books/bookvolbib add bibliographic references
20140807 tpd src/axiom-website/patches.html 20140807.01.tpd.patch
20140807 tpd books/bookvolbib add bibliographic references
20140806 tpd src/axiom-website/patches.html 20140806.01.tpd.patch
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 612cc52..ea43c65 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4606,6 +4606,8 @@ Makefile, src/Makefile remove src/scripts directory
merge and remove include, lib, and clef into books
20140807.01.tpd.patch
books/bookvolbib add bibliographic references
+20140808.01.tpd.patch
+books/bookvolbib add bibliographic references