From 9a171b2418813d4d17cd9740d913966d7405ad97 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 27 Jun 2016 14:38:11 -0400
Subject: [PATCH] books/bookvolbib Axiom Citations in the Literature
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Goal: Axiom Literate Programming
\index{Kumar, P.}
\index{Pellegrino, S.}
\begin{chunk}{axiom.bib}
@article{Kuma00,
author = "Kumar, P. and Pellegrino, S.",
title = "Computation of kinematic paths and bifurcation points",
journal = "Int. J. Solids Struct.",
volume = "37",
number = "46-47",
pages = "7003-7027",
year = "2000",
keywords = "axiomref",
abstract =
"This article deals with the kinematic simulation of movable
structures that go through special configurations of kinematic
bifurcation, as they move. A series of algorithms are developed for
structures that can be modelled using pin-jointed bars and that admit
a single-parameter motion. These algorithms are able to detect and
locate any bifurcation points that exist along the path of the
structure and, at each bifurcation point, can determine all possible
motions of the structure. The theory behind the algorithms is
explained, and the analysis of a simple example is discussed in
detail. Then, a simplified version of the particular problem that had
motivated this work, the simulation of the folding and deployment of a
thin membrane structure forming a solar sail, is analysed. For the
particular cases that are considered, it is found that the entire
process is inextensional, but a detailed study of the simulation
results shows that in more general cases, it is likely that stretching
or wrinkling will occur."
}
\end{chunk}
\index{Safouhi, Hassan}
\begin{chunk}{axiom.bib}
@article{Safo00,
author = "Safouhi, Hassan",
title = {The $HD$ and $H\overline{D}$ methods for accelerating the
convergence of three-center nuclear attraction and four-center
two-electron Coulomb integrals over $B$ functions and their
convergence properties.},
journal = "J. Comput. Phys.",
volume = "165",
number = "2",
pages = "473-495",
year = "2000",
keywords = "axiomref",
abstract =
"Three-center nuclear attraction and four-center two-electron
Coulomb integrals over Slater-type orbitals are required for $ab$
initio and density functional theory molecular structure
calculations. They occur in many millions of terms, even for small
molecules and require rapid and accurate evaluation. The $B$
functions are used as a basis set of atomic orbitals. These
functions are well adapted to the Fourier transform method that
allowed analytical expressions for the integrals of interest to be
developed. Rapid and accurate evaluation of these analytical
expressions is now made possible by applying the $HD$ and
$H\overline{D}$ methods for accelerating the convergence of the
semi-infinite oscillatory integrals. The convergence properties of
the new methods are analyzed. The numerical results section shows
the high predetermined accuracy and the substantial gain in the
calculation times obtained using the new methods."
}
\end{chunk}
\index{Adams, A.A.}
\index{Gottliebsen, H.}
\index{Linton, S.A.}
\index{Martin, U.}
\begin{chunk}{axiom.bib}
@InProceedings{Adam99a,
author = "Adams, A.A. and Gottliebsen, H. and Linton, S.A. and Martin, U.",
title = "VSDITLU: A verifiable symbolic definite integral table look-up",
booktitle = "Automated Deduction",
series = "CADE 16",
year = "1999",
location = "Trento, Italy",
pages = "112-126",
keywords = "axiomref",
paper = "Adam99a.pdf",
url = "http://www.a-cubed.info/Publications/CADE99.pdf",
abstract =
"We present a verifiable symbolic definite integral table lookup: 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 facts about the reals in the theorem
prover PVS to aid in the transformation of the table entry into an
answer. Our system is able to obtain correct answers in cases where
standard techniques implemented in computer algebra systems fail. 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 do not. We extend upon Fateman’s
web-based table by including parametric limits of integration and
queries with side conditions."
}
\end{chunk}
\index{Aitken, William E.}
\index{Constable, Robert L.}
\index{Underwood, Judith L.}
\begin{chunk}{axiom.bib}
@article{Aitk99,
author = "Aitken, William E. and Constable, Robert L. and
Underwood, Judith L.",
title = "Metalogical frameworks. II: Developing a reflected decision
procedure",
journal = "J. Autom. Reasoning",
volume = "22",
number = "2",
pages = "171-221",
year = "1999",
keywords = "axiomref",
paper = "Aitk99.pdf",
url = "http://www.nuprl.org/documents/Constable/MetalogicalFrameworksII.pdf",
abstract =
"Proving theorems is a creative act demanding new combinations of ideas
and on occasion new methods of argument. For this reason, theorem
proving systems need to be extensible. The provers should also remain
correct under extension, so there must be a secure mechanism for doing
this. The tactic-style provers pioneered by Edinburgh LCF provide a
very effective way to achieve secure extensions, but in such systems,
all new methods must be reduced to tactics. This is a drawback because
there are other useful proof generating tools such as decision
procedures; these include, for example, algorithms which reduce a
deduction problem, such as arithmetic provability, to a computation on
graphs.
The Nuprl system pioneered the combination of fixed decision
procedures with tactics, but the issue of securely adding new ones was
not solved. In this paper, we show how to safely include user-defined
decision procedures in theorem provers. The idea is to prove
properties of the procedure inside the prover’s logic and then invoke
a reflection rule to connect the procedure to the system. We also show
that using a rich underlying logic permits an abstract account of the
approach so that the results carry over to different implementations
and other logics."
}
\end{chunk}
\index{Boulm\'e, S.}
\index{Hardin, T.}
\index{Hirschkoff, D.}
\index{Rioboo, Renaud}
\index{M\'enissier-Morain, V.}
\begin{chunk}{axiom.bib}
@InProceedings{Boul99,
author = "Boulme, S. and Hardin, T. and Hirschkoff, D. and Rioboo, Renaud",
title = "On the way to certify Computer Algebra Systems",
booktitle = "Systems for integrated computation and deduction",
series = "Calculemus 99",
year = "1999",
publisher = "Elsevier",
location = "Trento, Italy",
pages = "11-12",
keywords = "axiomref",
paper = "Boul99.pdf",
abstract = "
The FOC project aims at supporting, within a coherent software system,
the entire process of mathematical computation, starting with proved
theories, ending with certified implementations of algorithms. In this
paper, we explain our design requirements for the implementation,
using polynomials as a running example. Indeed, proving correctness of
implementations depends heavily on the way this design allows
mathematical properties to be truly handled at the programming level.
The FOC project, started at the fall of 1997, is aimed to build a
programming environment for the development of certified symbolic
computation. The working languages are Coq and Ocaml. In this paper,
we present first the motivations of the project. We then explain why
and how our concern for proving properties of programs has led us to
certain implementation choices in Ocaml. This way, the sources express
exactly the mathematical dependencies between different structures.
This may ease the achievement of proofs."
}
\end{chunk}
---
books/bookvol10.2.pamphlet | 64 ++++++++--
books/bookvol10.4.pamphlet | 18 ++-
books/bookvolbib.pamphlet | 271 ++++++++++++++++++++++++++++++++++++----
changelog | 4 +
patch | 188 ++++++++++++++++++++++++++--
src/axiom-website/patches.html | 2 +
6 files changed, 500 insertions(+), 47 deletions(-)
diff --git a/books/bookvol10.2.pamphlet b/books/bookvol10.2.pamphlet
index ee85fdd..7b1feb1 100644
--- a/books/bookvol10.2.pamphlet
+++ b/books/bookvol10.2.pamphlet
@@ -32818,7 +32818,9 @@ V:OrderedSet, P:RecursivePolynomialCategory(R,E,V)):
?~=? : (%,%) -> Boolean
\end{verbatim}
-See: Aubry et al. \cite{Aubr99}
+See: SALSA\cite{SALSA}, Kalkbrener\cite{Kalk91,Kalk98},
+Aubry\cite{Aubr96,Aubr99,Aubr99a}, Lazard\cite{Laza91},
+Moreno Maza\cite{Maza95,Maza97,Maza98,Maza00}
\label{category TSETCAT TriangularSetCategory}
\begin{chunk}{category TSETCAT TriangularSetCategory}
)abbrev category TSETCAT TriangularSetCategory
@@ -32826,7 +32828,19 @@ See: Aubry et al. \cite{Aubr99}
++ Date Created: 04/26/1994
++ Date Last Updated: 12/15/1998
++ References :
+++ SALSA Solvers for Algebraic Systems and Applications
+++ Kalk91 Three contributions to elimination theory
+++ Kalk98 Algorithmic properties of polynomial rings
+++ Aubr96 Triangular Sets for Solving Polynomial Systems:
++ Aubr99 On the Theories of Triangular Sets
+++ Aubr99a Triangular Sets for Solving Polynomial Systems:
+++ Laza91 A new method for solving algebraic systems of positive dimension
+++ Maza95 Polynomial Gcd Computations over Towers of Algebraic Extensions
+++ Maza97 Calculs de pgcd au-dessus des tours d'extensions simples et
+++ resolution des systemes d'equations algebriques
+++ Maza98 A new algorithm for computing triangular decomposition of
+++ algebraic varieties
+++ Maza00 On Triangular Decompositions of Algebraic Varieties
++ Description:
++ The category of triangular sets of multivariate polynomials
++ with coefficients in an integral domain.
@@ -39321,8 +39335,9 @@ P:RecursivePolynomialCategory(R,E,V)):
?=? : (%,%) -> Boolean
\end{verbatim}
-See: SALSA\cite{SALSA}, Kalkbrener\cite{Kalk91}\cite{Kalk98},
-Aubry\cite{Aubr99}, Moreno Maza\cite{Maza98}
+See: SALSA\cite{SALSA}, Kalkbrener\cite{Kalk91,Kalk98},
+Aubry\cite{Aubr96,Aubr99,Aubr99a}, Lazard\cite{Laza91},
+Moreno Maza\cite{Maza95,Maza97,Maza98,Maza00}
\label{category RSETCAT RegularTriangularSetCategory}
\begin{chunk}{category RSETCAT RegularTriangularSetCategory}
)abbrev category RSETCAT RegularTriangularSetCategory
@@ -39333,9 +39348,16 @@ Aubry\cite{Aubr99}, Moreno Maza\cite{Maza98}
++ SALSA Solvers for Algebraic Systems and Applications
++ Kalk91 Three contributions to elimination theory
++ Kalk98 Algorithmic properties of polynomial rings
+++ Aubr96 Triangular Sets for Solving Polynomial Systems:
++ Aubr99 On the Theories of Triangular Sets
+++ Aubr99a Triangular Sets for Solving Polynomial Systems:
+++ Laza91 A new method for solving algebraic systems of positive dimension
+++ Maza95 Polynomial Gcd Computations over Towers of Algebraic Extensions
+++ Maza97 Calculs de pgcd au-dessus des tours d'extensions simples et
+++ resolution des systemes d'equations algebriques
++ Maza98 A new algorithm for computing triangular decomposition of
-++ algebraic varieties
+++ algebraic varieties
+++ Maza00 On Triangular Decompositions of Algebraic Varieties
++ Description:
++ The category of regular triangular sets, introduced under
++ the name regular chains in [1] (and other papers).
@@ -41629,8 +41651,9 @@ P:RecursivePolynomialCategory(R,E,V)):
?~=? : (%,%) -> Boolean
\end{verbatim}
-See: Lazard\cite{Laza91}, Aubry\cite{Aubr99},
-Morena Maza\cite{Maza95}\cite{Maza97}
+See: SALSA\cite{SALSA}, Kalkbrener\cite{Kalk91,Kalk98},
+Aubry\cite{Aubr96,Aubr99,Aubr99a}, Lazard\cite{Laza91},
+Moreno Maza\cite{Maza95,Maza97,Maza98,Maza00}
\label{category NTSCAT NormalizedTriangularSetCategory}
\begin{chunk}{category NTSCAT NormalizedTriangularSetCategory}
)abbrev category NTSCAT NormalizedTriangularSetCategory
@@ -41638,11 +41661,19 @@ Morena Maza\cite{Maza95}\cite{Maza97}
++ Date Created: 10/07/1998
++ Date Last Updated: 12/12/1998
++ References :
-++ Laza91 A new method for solving algebraic systems of positive dimension
+++ SALSA Solvers for Algebraic Systems and Applications
+++ Kalk91 Three contributions to elimination theory
+++ Kalk98 Algorithmic properties of polynomial rings
+++ Aubr96 Triangular Sets for Solving Polynomial Systems:
++ Aubr99 On the Theories of Triangular Sets
+++ Aubr99a Triangular Sets for Solving Polynomial Systems:
+++ Laza91 A new method for solving algebraic systems of positive dimension
++ Maza95 Polynomial Gcd Computations over Towers of Algebraic Extensions
++ Maza97 Calculs de pgcd au-dessus des tours d'extensions simples et
-++ resolution des systemes d'equations algebriques
+++ resolution des systemes d'equations algebriques
+++ Maza98 A new algorithm for computing triangular decomposition of
+++ algebraic varieties
+++ Maza00 On Triangular Decompositions of Algebraic Varieties
++ Description:
++ The category of normalized triangular sets. A triangular
++ set ts is said normalized if for every algebraic
@@ -43094,7 +43125,9 @@ P:RecursivePolynomialCategory(R,E,V)):
?~=? : (%,%) -> Boolean
\end{verbatim}
-See: Lazard\cite{Laza91}, Kalkbrener\cite{Kalk98}, Moreno Maza\cite{Maza98}
+See: SALSA\cite{SALSA}, Kalkbrener\cite{Kalk91,Kalk98},
+Aubry\cite{Aubr96,Aubr99,Aubr99a}, Lazard\cite{Laza91},
+Moreno Maza\cite{Maza95,Maza97,Maza98,Maza00}
\label{category SFRTCAT SquareFreeRegularTriangularSetCategory}
\begin{chunk}{category SFRTCAT SquareFreeRegularTriangularSetCategory}
)abbrev category SFRTCAT SquareFreeRegularTriangularSetCategory
@@ -43102,10 +43135,19 @@ See: Lazard\cite{Laza91}, Kalkbrener\cite{Kalk98}, Moreno Maza\cite{Maza98}
++ Date Created: 09/03/1996
++ Date Last Updated: 09/10/1998
++ References :
-++ Laza91 A new method for solving algebraic systems of positive dimension
+++ SALSA Solvers for Algebraic Systems and Applications
+++ Kalk91 Three contributions to elimination theory
++ Kalk98 Algorithmic properties of polynomial rings
+++ Aubr96 Triangular Sets for Solving Polynomial Systems:
+++ Aubr99 On the Theories of Triangular Sets
+++ Aubr99a Triangular Sets for Solving Polynomial Systems:
+++ Laza91 A new method for solving algebraic systems of positive dimension
+++ Maza95 Polynomial Gcd Computations over Towers of Algebraic Extensions
+++ Maza97 Calculs de pgcd au-dessus des tours d'extensions simples et
+++ resolution des systemes d'equations algebriques
++ Maza98 A new algorithm for computing triangular decomposition of
-++ algebraic varieties
+++ algebraic varieties
+++ Maza00 On Triangular Decompositions of Algebraic Varieties
++ Description:
++ The category of square-free regular triangular sets.
++ A regular triangular set \spad{ts} is square-free if
diff --git a/books/bookvol10.4.pamphlet b/books/bookvol10.4.pamphlet
index bdc964e..de19f99 100644
--- a/books/bookvol10.4.pamphlet
+++ b/books/bookvol10.4.pamphlet
@@ -226540,7 +226540,9 @@ modulo regular chains.
\end{quote}
-See: Moreno Maza\cite{Maza98}\cite{Maza00}, Aubry\cite{Aubr96}
+See: SALSA\cite{SALSA}, Kalkbrener\cite{Kalk91,Kalk98},
+Aubry\cite{Aubr96,Aubr99,Aubr99a}, Lazard\cite{Laza91},
+Moreno Maza\cite{Maza95,Maza97,Maza98,Maza00}
\label{package RSDCMPK RegularSetDecompositionPackage}
\begin{chunk}{package RSDCMPK RegularSetDecompositionPackage}
)abbrev package RSDCMPK RegularSetDecompositionPackage
@@ -226548,11 +226550,19 @@ See: Moreno Maza\cite{Maza98}\cite{Maza00}, Aubry\cite{Aubr96}
++ Date Created: 09/16/1998
++ Date Last Updated: 12/16/1998
++ References :
+++ SALSA Solvers for Algebraic Systems and Applications
+++ Kalk91 Three contributions to elimination theory
+++ Kalk98 Algorithmic properties of polynomial rings
+++ Aubr96 Triangular Sets for Solving Polynomial Systems:
+++ Aubr99 On the Theories of Triangular Sets
+++ Aubr99a Triangular Sets for Solving Polynomial Systems:
+++ Laza91 A new method for solving algebraic systems of positive dimension
+++ Maza95 Polynomial Gcd Computations over Towers of Algebraic Extensions
+++ Maza97 Calculs de pgcd au-dessus des tours d'extensions simples et
+++ resolution des systemes d'equations algebriques
++ Maza98 A new algorithm for computing triangular decomposition of
-++ algebraic varieties
+++ algebraic varieties
++ Maza00 On Triangular Decompositions of Algebraic Varieties
-++ Aubr96 Triangular Sets for Solving Polynomial Systems:
-++ a Comparison of Four Methods
++ Description:
++ A package providing a new algorithm for solving polynomial systems
++ by means of regular chains. Two ways of solving are proposed:
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index f44bc7a..dd9752f 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -4478,12 +4478,19 @@ Martin, U.
\index{Ballarin, Clemens}
\index{Paulson, Lawrence C.}
-\begin{chunk}{ignore}
-\bibitem[Ballarin 99]{Ball99} Ballarin, Clemens; Paulson, Lawrence C.
+\begin{chunk}{axiom.bib}
+@article{Ball99,
+ author = "Ballarin, Clemens and Paulson, Lawrence C.",
title = "A Pragmatic Approach to Extending Provers by Computer Algebra --
with Applications to Coding Theory",
+ journal = "Fundam. Inform.",
+ volume = "39",
+ number = "1-2",
+ pages = "1-20",
+ year = "1999",
url = "http://www.cl.cam.ac.uk/~lp15/papers/Isabelle/coding.pdf",
paper = "Ball99.pdf",
+ keywords = "axiomref",
abstract = "
The use of computer algebra is usually considered beneficial for
mechanised reasoning in mathematical domains. We present a case study,
@@ -4503,6 +4510,7 @@ Martin, U.
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{chunk}
@@ -4555,15 +4563,20 @@ Martin, U.
\index{Hirschkoff, D.}
\index{Rioboo, Renaud}
\index{M\'enissier-Morain, V.}
-\begin{chunk}{ignore}
-\bibitem[Boulme 01]{BHHMR01}
-Boulm\'e, S.; Hardin, T.; Hirschkoff, D.; M\'enissier-Morain, V.; Rioboo, R.
+\begin{chunk}{axiom.bib}
+@InProceedings{Boul99,
+ author = "Boulme, S. and Hardin, T. and Hirschkoff, D. and Rioboo, Renaud",
title = "On the way to certify Computer Algebra Systems",
- year = "2001",
-Calculemus-2001
- paper = "BHHMR01.pdf",
- abstract = "
- The FOC project aims at supporting, within a coherent software system,
+ booktitle = "Systems for integrated computation and deduction",
+ series = "Calculemus 99",
+ year = "1999",
+ publisher = "Elsevier",
+ location = "Trento, Italy",
+ pages = "11-12",
+ keywords = "axiomref",
+ paper = "Boul99.pdf",
+ abstract =
+ "The FOC project aims at supporting, within a coherent software system,
the entire process of mathematical computation, starting with proved
theories, ending with certified implementations of algorithms. In this
paper, we explain our design requirements for the implementation,
@@ -4579,6 +4592,7 @@ Calculemus-2001
certain implementation choices in Ocaml. This way, the sources express
exactly the mathematical dependencies between different structures.
This may ease the achievement of proofs."
+}
\end{chunk}
@@ -10550,6 +10564,40 @@ J. Symbolic Computation 5, 237-259 (1988)
\end{chunk}
+\index{Adams, A.A.}
+\index{Gottliebsen, H.}
+\index{Linton, S.A.}
+\index{Martin, U.}
+\begin{chunk}{axiom.bib}
+@InProceedings{Adam99a,
+ author = "Adams, A.A. and Gottliebsen, H. and Linton, S.A. and Martin, U.",
+ title = "VSDITLU: A verifiable symbolic definite integral table look-up",
+ booktitle = "Automated Deduction",
+ series = "CADE 16",
+ year = "1999",
+ location = "Trento, Italy",
+ pages = "112-126",
+ keywords = "axiomref",
+ paper = "Adam99a.pdf",
+ url = "http://www.a-cubed.info/Publications/CADE99.pdf",
+ abstract =
+ "We present a verifiable symbolic definite integral table lookup: 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 facts about the reals in the theorem
+ prover PVS to aid in the transformation of the table entry into an
+ answer. Our system is able to obtain correct answers in cases where
+ standard techniques implemented in computer algebra systems fail. 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 do not. We extend upon Fateman’s
+ web-based table by including parametric limits of integration and
+ queries with side conditions."
+}
+
+\end{chunk}
+
\index{Akbar Hussain, D.M.}
\index{Haq, Shaiq A.}
\index{Khan, Zafar Ullah}
@@ -10583,6 +10631,49 @@ J. Symbolic Computation 5, 237-259 (1988)
\end{chunk}
+\index{Aitken, William E.}
+\index{Constable, Robert L.}
+\index{Underwood, Judith L.}
+\begin{chunk}{axiom.bib}
+@article{Aitk99,
+ author = "Aitken, William E. and Constable, Robert L. and
+ Underwood, Judith L.",
+ title = "Metalogical frameworks. II: Developing a reflected decision
+ procedure",
+ journal = "J. Autom. Reasoning",
+ volume = "22",
+ number = "2",
+ pages = "171-221",
+ year = "1999",
+ keywords = "axiomref",
+ paper = "Aitk99.pdf",
+ url = "http://www.nuprl.org/documents/Constable/MetalogicalFrameworksII.pdf",
+ abstract =
+ "Proving theorems is a creative act demanding new combinations of ideas
+ and on occasion new methods of argument. For this reason, theorem
+ proving systems need to be extensible. The provers should also remain
+ correct under extension, so there must be a secure mechanism for doing
+ this. The tactic-style provers pioneered by Edinburgh LCF provide a
+ very effective way to achieve secure extensions, but in such systems,
+ all new methods must be reduced to tactics. This is a drawback because
+ there are other useful proof generating tools such as decision
+ procedures; these include, for example, algorithms which reduce a
+ deduction problem, such as arithmetic provability, to a computation on
+ graphs.
+
+ The Nuprl system pioneered the combination of fixed decision
+ procedures with tactics, but the issue of securely adding new ones was
+ not solved. In this paper, we show how to safely include user-defined
+ decision procedures in theorem provers. The idea is to prove
+ properties of the procedure inside the prover’s logic and then invoke
+ a reflection rule to connect the procedure to the system. We also show
+ that using a rich underlying logic permits an abstract account of the
+ approach so that the results carry over to different implementations
+ and other logics."
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{America,
keywords = "axiomref",
@@ -14463,6 +14554,39 @@ ISSN 0304-3975
\end{chunk}
+\index{Kumar, P.}
+\index{Pellegrino, S.}
+\begin{chunk}{axiom.bib}
+@article{Kuma00,
+ author = "Kumar, P. and Pellegrino, S.",
+ title = "Computation of kinematic paths and bifurcation points",
+ journal = "Int. J. Solids Struct.",
+ volume = "37",
+ number = "46-47",
+ pages = "7003-7027",
+ year = "2000",
+ keywords = "axiomref",
+ abstract =
+ "This article deals with the kinematic simulation of movable
+ structures that go through special configurations of kinematic
+ bifurcation, as they move. A series of algorithms are developed for
+ structures that can be modelled using pin-jointed bars and that admit
+ a single-parameter motion. These algorithms are able to detect and
+ locate any bifurcation points that exist along the path of the
+ structure and, at each bifurcation point, can determine all possible
+ motions of the structure. The theory behind the algorithms is
+ explained, and the analysis of a simple example is discussed in
+ detail. Then, a simplified version of the particular problem that had
+ motivated this work, the simulation of the folding and deployment of a
+ thin membrane structure forming a solar sail, is analysed. For the
+ particular cases that are considered, it is found that the entire
+ process is inextensional, but a detailed study of the simulation
+ results shows that in more general cases, it is likely that stretching
+ or wrinkling will occur."
+}
+
+\end{chunk}
+
\index{Kusche, K.}
\index{Kutzler, B.}
\index{Mayr, H.}
@@ -15137,7 +15261,11 @@ ISSN 0730-8639
paper = "Maza00.pdf",
url = "http://www.csd.uwo.ca/~moreno//Publications",
keywords = "axiomref",
- comment = "\newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
abstract =
"Different kinds of triangular decompositions of algebraic varieties
are presented. The main result is an efficient method for obtaining
@@ -15924,6 +16052,40 @@ Mathematik und Physik, 75 (suppl. 2):S435-S438, 1995 ISSN 0044-2267
\index{Safouhi, Hassan}
\begin{chunk}{axiom.bib}
+@article{Safo00,
+ author = "Safouhi, Hassan",
+ title = {The $HD$ and $H\overline{D}$ methods for accelerating the
+ convergence of three-center nuclear attraction and four-center
+ two-electron Coulomb integrals over $B$ functions and their
+ convergence properties.},
+ journal = "J. Comput. Phys.",
+ volume = "165",
+ number = "2",
+ pages = "473-495",
+ year = "2000",
+ keywords = "axiomref",
+ abstract =
+ "Three-center nuclear attraction and four-center two-electron
+ Coulomb integrals over Slater-type orbitals are required for $ab$
+ initio and density functional theory molecular structure
+ calculations. They occur in many millions of terms, even for small
+ molecules and require rapid and accurate evaluation. The $B$
+ functions are used as a basis set of atomic orbitals. These
+ functions are well adapted to the Fourier transform method that
+ allowed analytical expressions for the integrals of interest to be
+ developed. Rapid and accurate evaluation of these analytical
+ expressions is now made possible by applying the $HD$ and
+ $H\overline{D}$ methods for accelerating the convergence of the
+ semi-infinite oscillatory integrals. The convergence properties of
+ the new methods are analyzed. The numerical results section shows
+ the high predetermined accuracy and the substantial gain in the
+ calculation times obtained using the new methods."
+}
+
+\end{chunk}
+
+\index{Safouhi, Hassan}
+\begin{chunk}{axiom.bib}
@article{Safo01,
author = "Safouhi, Hassan",
title = "Numerical evaluation of three-center two-electron Coulomb and
@@ -15951,7 +16113,11 @@ Mathematik und Physik, 75 (suppl. 2):S435-S438, 1995 ISSN 0044-2267
title = "Solvers for Algebraic Systems and Applications",
url =
"http://www.ens-lyon.fr/LIP/Arenaire/SYMB/teams/salsa/proposal-salsa.pdf",
- comment = "\newline\refto{category RSETCAT RegularTriangularSetCategory}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
paper = "SALSA.pdf"
}
@@ -17315,7 +17481,9 @@ National Physical Laboratory. (1982)
papers = "Aubr99.pdf",
comment = "\newline\refto{category TSETCAT TriangularSetCategory}
\newline\refto{category RSETCAT RegularTriangularSetCategory}
- \newline\refto{category NTSCAT NormalizedTriangularSetCategory}",
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
abstract =
"Different notions of triangular sets are presented. The relationship
between these notions are studied. The main result is that four
@@ -17334,7 +17502,42 @@ National Physical Laboratory. (1982)
a Comparison of Four Methods",
url = "http://www.lip6.fr/lip6/reports/1997/lip6.1997.009.ps.gz",
paper = "Aubr96.pdf",
- comment = "\newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
+ keywords = "axiomref",
+ abstract =
+ "Four methods for solving polynomial systems by means of triangular
+ sets are presented and implemented in a unified way. These methods are
+ those of Wu, Lazard, Kalkbrener, and Wang. They are compared on
+ various examples with emphasis on efficiency, conciseness and
+ legibility of the outputs."
+}
+
+\end{chunk}
+
+\index{Aubry, Phillippe}
+\index{Maza, Marc Moreno}
+\begin{chunk}{axiom.bib}
+@article{Aubr99a,
+ author = "Aubry, Phillippe and Maza, Marc Moreno",
+ title = "Triangular Sets for Solving Polynomial Systems:
+ a Comparison of Four Methods",
+ journal = "J. Symb. Comput.",
+ volume = "28",
+ number = "1-2",
+ pages = "125-154",
+ year = "1999",
+ url =
+ "http://www.csd.uwo.ca/~moreno/Publications/Aubry-MorenoMaza-1999-JSC.pdf",
+ paper = "Aubr99a.pdf",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
keywords = "axiomref",
abstract =
"Four methods for solving polynomial systems by means of triangular
@@ -19257,7 +19460,11 @@ Comput. J. 9 281--285. (1966)
title = "Three contributions to elimination theory",
school = "University of Linz, Austria",
year = "1991",
- comment = "\newline\refto{category RSETCAT RegularTriangularSetCategory}"
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}"
}
\end{chunk}
@@ -19268,8 +19475,11 @@ Comput. J. 9 281--285. (1966)
author = "Kalkbrener, M.",
title = "Algorithmic properties of polynomial rings",
journal = "Journal of Symbolic Computation",
- comment = "\newline\refto{category RSETCAT RegularTriangularSetCategory}
- \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
year = "1998",
paper = "Kalk98.pdf",
abstract =
@@ -19471,8 +19681,11 @@ Prentice-Hall. (1974)
year = "1991",
pages = "147-160",
paper = "Laza91.pdf",
- comment = "\newline\refto{category NTSCAT NormalizedTriangularSetCategory}
- \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
abstract =
"A new algorithm is presented for solving algebraic systems of
equations, which is designed from the structure which is wanted for
@@ -19751,7 +19964,11 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
year = "1995",
journal = "Proceedings of AAECC11",
keywords = "axiomref",
- comment = "\newline\refto{category NTSCAT NormalizedTriangularSetCategory}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
abstract =
"Some methods for polynomial system solving require efficient
techniques for computing univariate polynomial gcd over algebraic
@@ -19777,7 +19994,11 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
year = "1997",
paper = "Maza97.pdf",
keyword = "axiomref",
- comment = "\newline\refto{category NTSCAT NormalizedTriangularSetCategory}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
url =
"http://www.csd.uwo.ca/~moreno//Publications/MorenoMaza-Thesis-1997.ps.gz",
abstract =
@@ -19807,9 +20028,11 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
title = "A new algorithm for computing triangular decomposition of
algebraic varieties",
institution = "Numerical Algorithms Group (NAG)",
- comment = "\newline\refto{category RSETCAT RegularTriangularSetCategory}
- \newline\refto{package RSDCMPK RegularSetDecompositionPackage}
- \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}",
+ comment = "\newline\refto{category TSETCAT TriangularSetCategory}
+ \newline\refto{category RSETCAT RegularTriangularSetCategory}
+ \newline\refto{category NTSCAT NormalizedTriangularSetCategory}
+ \newline\refto{category SFRTCAT SquareFreeRegularTriangularSetCategory}
+ \newline\refto{package RSDCMPK RegularSetDecompositionPackage}",
year = "1998"
}
diff --git a/changelog b/changelog
index a3cd4c0..d835d31 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,7 @@
+20160627 tpd src/axiom-website/patches.html 20160626.02.tpd.patch
+20160627 tpd books/bookvol10.4 additional citations
+20160627 tpd books/bookvol10.2 additional citations
+20160627 tpd books/bookvolbib Axiom Citations in the Literature
20160627 tpd src/axiom-website/patches.html 20160627.01.tpd.patch
20160627 tpd buglist: add todo 339: missing side conditions
20160626 tpd src/axiom-website/patches.html 20160626.10.tpd.patch
diff --git a/patch b/patch
index ecc6842..7c3f9f6 100644
--- a/patch
+++ b/patch
@@ -1,14 +1,186 @@
-buglist: add todo 339: missing side conditions
+books/bookvolbib Axiom Citations in the Literature
-Goal: Correct Axiom Mathematics
+Goal: Axiom Literate Programming
-=========================================================================
-todo 339: missing side conditions
+\index{Kumar, P.}
+\index{Pellegrino, S.}
+\begin{chunk}{axiom.bib}
+@article{Kuma00,
+ author = "Kumar, P. and Pellegrino, S.",
+ title = "Computation of kinematic paths and bifurcation points",
+ journal = "Int. J. Solids Struct.",
+ volume = "37",
+ number = "46-47",
+ pages = "7003-7027",
+ year = "2000",
+ keywords = "axiomref",
+ abstract =
+ "This article deals with the kinematic simulation of movable
+ structures that go through special configurations of kinematic
+ bifurcation, as they move. A series of algorithms are developed for
+ structures that can be modelled using pin-jointed bars and that admit
+ a single-parameter motion. These algorithms are able to detect and
+ locate any bifurcation points that exist along the path of the
+ structure and, at each bifurcation point, can determine all possible
+ motions of the structure. The theory behind the algorithms is
+ explained, and the analysis of a simple example is discussed in
+ detail. Then, a simplified version of the particular problem that had
+ motivated this work, the simulation of the folding and deployment of a
+ thin membrane structure forming a solar sail, is analysed. For the
+ particular cases that are considered, it is found that the entire
+ process is inextensional, but a detailed study of the simulation
+ results shows that in more general cases, it is likely that stretching
+ or wrinkling will occur."
+}
-integrate((x-b)^(-1),x)
+\end{chunk}
- (1) log(x - b)
- Type: Union(Expression(Integer),...)
+\index{Safouhi, Hassan}
+\begin{chunk}{axiom.bib}
+@article{Safo00,
+ author = "Safouhi, Hassan",
+ title = {The $HD$ and $H\overline{D}$ methods for accelerating the
+ convergence of three-center nuclear attraction and four-center
+ two-electron Coulomb integrals over $B$ functions and their
+ convergence properties.},
+ journal = "J. Comput. Phys.",
+ volume = "165",
+ number = "2",
+ pages = "473-495",
+ year = "2000",
+ keywords = "axiomref",
+ abstract =
+ "Three-center nuclear attraction and four-center two-electron
+ Coulomb integrals over Slater-type orbitals are required for $ab$
+ initio and density functional theory molecular structure
+ calculations. They occur in many millions of terms, even for small
+ molecules and require rapid and accurate evaluation. The $B$
+ functions are used as a basis set of atomic orbitals. These
+ functions are well adapted to the Fourier transform method that
+ allowed analytical expressions for the integrals of interest to be
+ developed. Rapid and accurate evaluation of these analytical
+ expressions is now made possible by applying the $HD$ and
+ $H\overline{D}$ methods for accelerating the convergence of the
+ semi-infinite oscillatory integrals. The convergence properties of
+ the new methods are analyzed. The numerical results section shows
+ the high predetermined accuracy and the substantial gain in the
+ calculation times obtained using the new methods."
+}
-should show the side-condition x > b or should be log(abs(x-b))
+\end{chunk}
+
+\index{Adams, A.A.}
+\index{Gottliebsen, H.}
+\index{Linton, S.A.}
+\index{Martin, U.}
+\begin{chunk}{axiom.bib}
+@InProceedings{Adam99a,
+ author = "Adams, A.A. and Gottliebsen, H. and Linton, S.A. and Martin, U.",
+ title = "VSDITLU: A verifiable symbolic definite integral table look-up",
+ booktitle = "Automated Deduction",
+ series = "CADE 16",
+ year = "1999",
+ location = "Trento, Italy",
+ pages = "112-126",
+ keywords = "axiomref",
+ paper = "Adam99a.pdf",
+ url = "http://www.a-cubed.info/Publications/CADE99.pdf",
+ abstract =
+ "We present a verifiable symbolic definite integral table lookup: 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 facts about the reals in the theorem
+ prover PVS to aid in the transformation of the table entry into an
+ answer. Our system is able to obtain correct answers in cases where
+ standard techniques implemented in computer algebra systems fail. 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 do not. We extend upon Fateman’s
+ web-based table by including parametric limits of integration and
+ queries with side conditions."
+}
+
+\end{chunk}
+
+\index{Aitken, William E.}
+\index{Constable, Robert L.}
+\index{Underwood, Judith L.}
+\begin{chunk}{axiom.bib}
+@article{Aitk99,
+ author = "Aitken, William E. and Constable, Robert L. and
+ Underwood, Judith L.",
+ title = "Metalogical frameworks. II: Developing a reflected decision
+ procedure",
+ journal = "J. Autom. Reasoning",
+ volume = "22",
+ number = "2",
+ pages = "171-221",
+ year = "1999",
+ keywords = "axiomref",
+ paper = "Aitk99.pdf",
+ url = "http://www.nuprl.org/documents/Constable/MetalogicalFrameworksII.pdf",
+ abstract =
+ "Proving theorems is a creative act demanding new combinations of ideas
+ and on occasion new methods of argument. For this reason, theorem
+ proving systems need to be extensible. The provers should also remain
+ correct under extension, so there must be a secure mechanism for doing
+ this. The tactic-style provers pioneered by Edinburgh LCF provide a
+ very effective way to achieve secure extensions, but in such systems,
+ all new methods must be reduced to tactics. This is a drawback because
+ there are other useful proof generating tools such as decision
+ procedures; these include, for example, algorithms which reduce a
+ deduction problem, such as arithmetic provability, to a computation on
+ graphs.
+
+ The Nuprl system pioneered the combination of fixed decision
+ procedures with tactics, but the issue of securely adding new ones was
+ not solved. In this paper, we show how to safely include user-defined
+ decision procedures in theorem provers. The idea is to prove
+ properties of the procedure inside the prover’s logic and then invoke
+ a reflection rule to connect the procedure to the system. We also show
+ that using a rich underlying logic permits an abstract account of the
+ approach so that the results carry over to different implementations
+ and other logics."
+}
+
+\end{chunk}
+
+\index{Boulm\'e, S.}
+\index{Hardin, T.}
+\index{Hirschkoff, D.}
+\index{Rioboo, Renaud}
+\index{M\'enissier-Morain, V.}
+\begin{chunk}{axiom.bib}
+@InProceedings{Boul99,
+ author = "Boulme, S. and Hardin, T. and Hirschkoff, D. and Rioboo, Renaud",
+ title = "On the way to certify Computer Algebra Systems",
+ booktitle = "Systems for integrated computation and deduction",
+ series = "Calculemus 99",
+ year = "1999",
+ publisher = "Elsevier",
+ location = "Trento, Italy",
+ pages = "11-12",
+ keywords = "axiomref",
+ paper = "Boul99.pdf",
+ abstract = "
+ The FOC project aims at supporting, within a coherent software system,
+ the entire process of mathematical computation, starting with proved
+ theories, ending with certified implementations of algorithms. In this
+ paper, we explain our design requirements for the implementation,
+ using polynomials as a running example. Indeed, proving correctness of
+ implementations depends heavily on the way this design allows
+ mathematical properties to be truly handled at the programming level.
+
+ The FOC project, started at the fall of 1997, is aimed to build a
+ programming environment for the development of certified symbolic
+ computation. The working languages are Coq and Ocaml. In this paper,
+ we present first the motivations of the project. We then explain why
+ and how our concern for proving properties of programs has led us to
+ certain implementation choices in Ocaml. This way, the sources express
+ exactly the mathematical dependencies between different structures.
+ This may ease the achievement of proofs."
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 1c4123f..9c4efa0 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5414,6 +5414,8 @@ books/bookvolbib Axiom Citations in the Literature

books/bookvolbib Axiom Citations in the Literature

20160627.01.tpd.patch
buglist: add todo 339: missing side conditions

+20160627.02.tpd.patch
+books/bookvolbib Axiom Citations in the Literature

--
1.7.5.4