From 2ad3d9332aa5b5eb4a7a34c6937ce3fbe1efc247 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 24 Jun 2016 18:47:23 -0400
Subject: [PATCH] books/bookvolbib Axiom Citations in the Literature
Goal: Axiom Literate Programming
Collect algebra references in the bibliography
\index{Rothstein, Michael}
\index{Caviness, Bob F.}
\begin{chunk}{axiom.bib}
@article{Ro76a,
author = "Rothstein, Michael and Caviness, Bob F.",
title = "A structure theorem for exponential and primitive functions:
a preliminary report",
journal = "ACM Sigsam Bulletin",
volume = "10",
number = "4",
year = "1976",
paper = "Ro76a.pdf",
abstract =
"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{chunk}
\index{Singer, Michael F.}
\index{Saunders, B. David}
\index{Caviness, Bob F.}
\begin{chunk}{axiom.bib}
@article{Sing85,
author = "Singer, Michael F. and Saunders, B. David and Caviness, Bob F.",
title = "An extension of Liouville's theorem on integration in finite terms",
journal = "SIAM J. of Comp.",
volume = "14",
pages = "965-990",
year = "1985",
url = "http://www4.ncsu.edu/~singer/papers/singer_saunders_caviness.pdf",
paper = "Sing85.pdf",
abstract =
"In Part 1 of this paper, we give an extension of Liouville's Theorem
and give a number of examples which show that integration with special
functions involves some phenomena that do not occur in integration
with the elementary functions alone. Our main result generalizes
Liouville's Theorem by allowing, in addition to the elementary
functions, special functions such as the error function, Fresnel
integrals and the logarithmic integral (but not the dilogarithm or
exponential integral) to appear in the integral of an elementary
function. The basic conclusion is that these functions, if they
appear, appear linearly. We give an algorithm which decides if an
elementary function, built up using only exponential functions and
rational operations has an integral which can be expressed in terms of
elementary functions and error functions."
}
\end{chunk}
\index{Buchberger, Bruno}
\index{Caviness, Bob F.}
\begin{chunk}{axiom.bib}
@book{Buch85,
author = "Buchberger, Bruno and Caviness, Bob F. (eds)",
title = "Lecture Notes in Computer Science, Vol 204",
isbn = "0-387-15983-5 (vol 1), 0-387-15984-3 (vol 2)",
year = "1985",
month = "April",
publisher = "Springer-Verlag, Berlin, Germany",
keywords = "axiomref"
}
\end{chunk}
\index{Kokol-voljc, Vlasta}
\index{Kutzler, Bernhard}
\begin{chunk}{axiom.bib}
@misc{ACA00,
authors = "Kokol-voljc, Vlasta and Kutzler, Bernhard",
title = "Computer Algebra Meets Education",
keywords = "axiomref",
conference = "Sessions of ACA2000",
abstract =
"Education has become one of the fastest growing application areas for
computers in general and computer algebra in particular. Computer
algebra tools such as TI-92/89, Derive, Mathematica, Maple, Axiom,
Reduce, Macsyma, or Mupad make powerful teaching tools in mathematics,
physics, chemistry, biology, economy.
The goal of this session is to exchange ideas and experiences, to hear
about classroom experiments, and to discuss all issues related to the
use of computer algebra tools in the classroom (such as assessment,
change of curricula, new support material, ...)"
}
\end{chunk}
\index{van Leeuwen, Andr\'e M.A.}
\begin{chunk}{axiom.bib}
@article{Leeu94,
author = "van Leeuwen, Andre M.A.",
title = "LiE, A software package for Lie group computations",
journal = "Euromath Bulletin",
volume = "1",
number = "2",
year = "1994",
keywords = "axiomref",
paper = "Leeu94.pdf",
abstract =
"A description is given of LiE, a specialized computer algebra package
for computations concerning Lie groups and algebras, and their
representations. The functionality of the package is demonstrated by
sample computations, and the structure of the program and the
algorithms implemented in it are discussed."
}
\end{chunk}
\index{Hoarau, Emma}
\index{David, Claire}
\begin{chunk}{axiom.bib}
@article{Hoar08,
author = "Hoarau, Emma and David, Claire",
title = "Lie group computation of finite difference schemes",
year = "2008",
journal = "math.NA",
url = "http://arxiv.org/pdf/math/0611895.pdf",
paper = "Hoar08.pdf",
keywords = "axiomref",
abstract =
"A Mathematica based program has been elaborated in order to determine
the symmetry group of a finite difference equation. The package
provides functions which enabel use to solve the determining equations
of the related Lie group."
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Ency16,
author = "Unknown",
title = "Encyclopedia of Mathematics",
url =
"https://www.encyclopediaofmath.org/index.php/Computer\_algebra\_package",
keywords = "axiomref"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Swmath,
author = "Unknown",
title = "Axiom",
url = "https://www.swmath.org/software/63",
keywords = "axiomref",
abstract =
"Axiom is a general purpose Computer Algebra System (CAS). It is
useful for research and developement of mathematical algorithms.
It defines a strongly typed, mathematically correct type hierarchy.
It has a programming language and a built-in compiler."
}
\end{chunk}
\index{Heras, Jonathan}
\index{Martin-Mateos, Franciso Jesus}
\index{Pascual, Vico}
@article{Hera15,
author = "Heras, Jonathan and Martin-Mateos, Franciso Jesus and
Pascual, Vico",
title = "Modelling algebraic structures and morphisms in ACL2",
journal = "Appl. Algebra Eng. Commun. Comput.",
volume = "26",
number = "3",
pages = "277-303",
year = "2015",
keywords = "axiomref",
abstract =
"In this paper, we present how algebraic structures and morphisms can
be modelled in the ACL2 theorem prover. Namely, we illustrate a
methodology for implementing a set of tools that facilitates the
formalisations related to algebraic structures -- as a result, an
algebraic hierarchy ranging from setoids to vector spaces has been
developed. The resultant tools can be used to simplify the development
of generic theories about algebraic structures. In particular, the
benefits of using the tools presented in this paper, compared to a
from-scratch approach, are especially relevant when working with
complex mathematical structures; for example, the structures employed
in Algebraic Topology. This work shows that ACL2 can be a suitable
tool for formalising algebraic concepts coming, for instance, from
computer algebra systems."
}
\end{chunk}
\index{Heras, Jonathan}
\index{Martin-Mateos, Franciso Jesus}
\index{Pascual, Vico}
\begin{chunk}{axiom.bib}
@misc{Hera16,
author = "Heras, Jonathan and Martin-Mateos, Franciso Jesus and
Pascual, Vico",
title = "A Hierarchy of Mathematical Structures in ACL2",
keywords = "axiomref",
paper = "Hera16.pdf",
url = "http://staff.computing.dundee.ac.uk/jheras/papers/ahomsia.pdf",
abstract =
"In this paper, we present a methodology which allows one to deal with
{\sl mathematical structures} in the ACL2 theorem prover. Namely, we
cope with the representation of mathematical structures, the
certification that an object fulfills the axioms characterizing an
algebraic structure and the generation of generic theories about
concrete structures. As a by-product, an {\sl ACL2 algebraic
hierarchy} has been obtained. Our framework has been tested with the
definition of {\sl homology groups}, an example coming from
Homological Algebra which involves several notions related to
Universal Algebra. The method presented here, when compared to a
from-scratch approach, is preferred when working with complex
mathematical structures; for instance, the ones coming from Algebraic
Topology. The final aim of this work is the verification of Computer
Algebra systems, a field where our hierarchy fits better than the ones
developed in other systems."
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{ORMS,
author = "Unknown",
title = "Oberwolfach References on Mathematical Software",
url = "http://orms.mfo.de/project?id=234",
keywords = "axiomref"
}
\end{chunk}
\index{Ballarin, Clemens}
\begin{chunk}{axiom.bib}
@article{Ball14,
author = "Ballarin, Clemens",
title = "Locales: a module system for mathematical theories",
journal = "J. Autom. Reasoning",
volume = "52",
number = "2",
pages = "123-153",
year = "2014",
keywords = "axiomref",
url = "http://www21.in.tum.de/~ballarin/publications/jar2013.pdf",
paper = "Ball14.pdf",
abstract =
"Locales are a module system for managing theory hierarchies in a
theorem prover through theory interpretation. They are available for
the theorem prover Isabelle. In this paper, their semantics is defined
in terms of local theories and morphisms. Locales aim at providing
flexible means of extension and reuse. Theory modules (which are
called locales) may be extended by definitions and
theorems. Interpretation of Isabelle's global theories and proof
contexts is possible via morphisms. Even the locale hierarchy may be
changed if declared relations between locales do not adequately
reflect logical relations, which are implied by the locales'
specifications. By discussing their design and relating it to more
commonly known structuring mechanisms of programming languages and
provers, locales are made accessible to a wider audience beyond the
users of Isabelle. The discussed mechanisms include ML-style functors,
type classes and mixins (the latter are found in modern
object-oriented languages)."
}
\end{chunk}
\index{van der Hoeven, Joris}
\begin{chunk}{axiom.bib}
@article{Hoev12,
author = "van der Hoeven, Joris",
title = "Overview of the Mathemagix type system",
journal = "ASCM 2102",
year = "2012",
keywords = "axiomref",
url = "http://www.texmacs.org/joris/mmxtyping/mmxtyping.pdf",
paper = "Hoev12.pdf",
abstract =
"The goal of the {\tt MATHEMAGIX} project is to develop a new and free
software for computer algebra and computer analysis, base on a
strongly typed and compiled language. In this paper, we focus on the
nderlying type system of this language, which allows for heavy
overloading, including parameterized overloading with parameters in so
called ``categories''. The exposition is informal and aims at giving
the reader an overview of the main concepts, ideas and differences
with existing languages. In a forthcoming paer, we intend to describe
the formal semantics of the type system in more detail."
}
\end{chunk}
---
books/bookvolbib.pamphlet | 269 +++++++++++++++++++++++++++++++---
changelog | 2 +
patch | 321 ++++++++++++++++++++++++++++++++++------
src/axiom-website/patches.html | 2 +
4 files changed, 528 insertions(+), 66 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 49e3c37..031cac2 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -6836,13 +6836,18 @@ PhD thesis, University of Wisconsin-Madison (1976)
\index{Rothstein, Michael}
\index{Caviness, Bob F.}
-\begin{chunk}{ignore}
-\bibitem[Rothstein 76a]{Ro76a} Rothstein, Michael; Caviness, B.F.
- title = "A structure theorem for exponential and primitive functions: a preliminary report",
-ACM Sigsam Bulletin Vol 10 Issue 4 (1976)
+\begin{chunk}{axiom.bib}
+@article{Ro76a,
+ author = "Rothstein, Michael and Caviness, Bob F.",
+ title = "A structure theorem for exponential and primitive functions:
+ a preliminary report",
+ journal = "ACM Sigsam Bulletin",
+ volume = "10",
+ number = "4",
+ year = "1976",
paper = "Ro76a.pdf",
- abstract = "
- In this paper a generalization of the Risch Structure Theorem is reported.
+ abstract =
+ "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$
@@ -6851,6 +6856,7 @@ ACM Sigsam Bulletin Vol 10 Issue 4 (1976)
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{chunk}
@@ -6907,14 +6913,18 @@ Proc. Amer. Math. Soc. Vol 23 pp689-691 (1969)
\index{Singer, Michael F.}
\index{Saunders, B. David}
\index{Caviness, Bob F.}
-\begin{chunk}{ignore}
-\bibitem[Singer 85]{Sing85} Singer, M.F.; Saunders, B.D.; Caviness, B.F.
+\begin{chunk}{axiom.bib}
+@article{Sing85,
+ author = "Singer, Michael F. and Saunders, B. David and Caviness, Bob F.",
title = "An extension of Liouville's theorem on integration in finite terms",
-SIAM J. of Comp. Vol 14 pp965-990 (1985)
+ journal = "SIAM J. of Comp.",
+ volume = "14",
+ pages = "965-990",
+ year = "1985",
url = "http://www4.ncsu.edu/~singer/papers/singer_saunders_caviness.pdf",
paper = "Sing85.pdf",
- abstract = "
- In Part 1 of this paper, we give an extension of Liouville's Theorem
+ abstract =
+ "In Part 1 of this paper, we give an extension of Liouville's Theorem
and give a number of examples which show that integration with special
functions involves some phenomena that do not occur in integration
with the elementary functions alone. Our main result generalizes
@@ -6927,6 +6937,7 @@ SIAM J. of Comp. Vol 14 pp965-990 (1985)
elementary function, built up using only exponential functions and
rational operations has an integral which can be expressed in terms of
elementary functions and error functions."
+}
\end{chunk}
@@ -10168,6 +10179,29 @@ rational right-hand sides etc."
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Kokol-voljc, Vlasta}
+\index{Kutzler, Bernhard}
+\begin{chunk}{axiom.bib}
+@misc{ACA00,
+ authors = "Kokol-voljc, Vlasta and Kutzler, Bernhard",
+ title = "Computer Algebra Meets Education",
+ keywords = "axiomref",
+ conference = "Sessions of ACA2000",
+ abstract =
+ "Education has become one of the fastest growing application areas for
+ computers in general and computer algebra in particular. Computer
+ algebra tools such as TI-92/89, Derive, Mathematica, Maple, Axiom,
+ Reduce, Macsyma, or Mupad make powerful teaching tools in mathematics,
+ physics, chemistry, biology, economy.
+
+ The goal of this session is to exchange ideas and experiences, to hear
+ about classroom experiments, and to discuss all issues related to the
+ use of computer algebra tools in the classroom (such as assessment,
+ change of curricula, new support material, ...)"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{ACM89,
author = "ACM",
@@ -10354,6 +10388,40 @@ American Mathematical Society (1994)
\end{chunk}
+\index{Ballarin, Clemens}
+\begin{chunk}{axiom.bib}
+@article{Ball14,
+ author = "Ballarin, Clemens",
+ title = "Locales: a module system for mathematical theories",
+ journal = "J. Autom. Reasoning",
+ volume = "52",
+ number = "2",
+ pages = "123-153",
+ year = "2014",
+ keywords = "axiomref",
+ url = "http://www21.in.tum.de/~ballarin/publications/jar2013.pdf",
+ paper = "Ball14.pdf",
+ abstract =
+ "Locales are a module system for managing theory hierarchies in a
+ theorem prover through theory interpretation. They are available for
+ the theorem prover Isabelle. In this paper, their semantics is defined
+ in terms of local theories and morphisms. Locales aim at providing
+ flexible means of extension and reuse. Theory modules (which are
+ called locales) may be extended by definitions and
+ theorems. Interpretation of Isabelle's global theories and proof
+ contexts is possible via morphisms. Even the locale hierarchy may be
+ changed if declared relations between locales do not adequately
+ reflect logical relations, which are implied by the locales'
+ specifications. By discussing their design and relating it to more
+ commonly known structuring mechanisms of programming languages and
+ provers, locales are made accessible to a wider audience beyond the
+ users of Isabelle. The discussed mechanisms include ML-style functors,
+ type classes and mixins (the latter are found in modern
+ object-oriented languages)."
+}
+
+\end{chunk}
+
\index{Beebe, Nelson H. F.}
\begin{chunk}{axiom.bib}
@misc{Beeb14,
@@ -10917,16 +10985,16 @@ Elektronik, 43(15) CODEN EKRKAR ISSN 0013-5658
\index{Buchberger, Bruno}
\index{Caviness, Bob F.}
-\begin{chunk}{ignore}
-\bibitem[Buchberger 85]{BC85} Buchberger, Bruno and Caviness, Bob F. (eds)
-EUROCAL '85: European Conference on Computer Algebra, Linz, Austria,
-LLCN QA155.7.E4 E86
- isbn = "0-387-15983-5, 0-387-15984-3",
+\begin{chunk}{axiom.bib}
+@book{Buch85,
+ author = "Buchberger, Bruno and Caviness, Bob F. (eds)",
+ title = "Lecture Notes in Computer Science, Vol 204",
+ isbn = "0-387-15983-5 (vol 1), 0-387-15984-3 (vol 2)",
year = "1985",
month = "April",
publisher = "Springer-Verlag, Berlin, Germany",
- keywords = "axiomref",
- misc = "Lecture Notes in Computer Science, Vol 204",
+ keywords = "axiomref"
+}
\end{chunk}
@@ -11891,6 +11959,17 @@ Madrid Spain, NAG conference (private copy of paper)
\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{chunk}{axiom.bib}
+@misc{Ency16,
+ author = "Unknown",
+ title = "Encyclopedia of Mathematics",
+ url =
+ "https://www.encyclopediaofmath.org/index.php/Computer\_algebra\_package",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Er\"ocal, Burcin}
\index{Stein, William}
\begin{chunk}{ignore}
@@ -12524,6 +12603,69 @@ Vol. 8 No. 3 pp195-210 (2001)
\end{chunk}
+\index{Heras, Jonathan}
+\index{Martin-Mateos, Franciso Jesus}
+\index{Pascual, Vico}
+\begin{chunk}{axiom.bib}
+@misc{Hera16,
+ author = "Heras, Jonathan and Martin-Mateos, Franciso Jesus and
+ Pascual, Vico",
+ title = "A Hierarchy of Mathematical Structures in ACL2",
+ keywords = "axiomref",
+ paper = "Hera16.pdf",
+ url = "http://staff.computing.dundee.ac.uk/jheras/papers/ahomsia.pdf",
+ abstract =
+ "In this paper, we present a methodology which allows one to deal with
+ {\sl mathematical structures} in the ACL2 theorem prover. Namely, we
+ cope with the representation of mathematical structures, the
+ certification that an object fulfills the axioms characterizing an
+ algebraic structure and the generation of generic theories about
+ concrete structures. As a by-product, an {\sl ACL2 algebraic
+ hierarchy} has been obtained. Our framework has been tested with the
+ definition of {\sl homology groups}, an example coming from
+ Homological Algebra which involves several notions related to
+ Universal Algebra. The method presented here, when compared to a
+ from-scratch approach, is preferred when working with complex
+ mathematical structures; for instance, the ones coming from Algebraic
+ Topology. The final aim of this work is the verification of Computer
+ Algebra systems, a field where our hierarchy fits better than the ones
+ developed in other systems."
+}
+
+\end{chunk}
+
+\index{Heras, Jonathan}
+\index{Martin-Mateos, Franciso Jesus}
+\index{Pascual, Vico}
+\begin{chunk}{axiom.bib}
+@article{Hera15,
+ author = "Heras, Jonathan and Martin-Mateos, Franciso Jesus and
+ Pascual, Vico",
+ title = "Modelling algebraic structures and morphisms in ACL2",
+ journal = "Appl. Algebra Eng. Commun. Comput.",
+ volume = "26",
+ number = "3",
+ pages = "277-303",
+ year = "2015",
+ keywords = "axiomref",
+ abstract =
+ "In this paper, we present how algebraic structures and morphisms can
+ be modelled in the ACL2 theorem prover. Namely, we illustrate a
+ methodology for implementing a set of tools that facilitates the
+ formalisations related to algebraic structures -- as a result, an
+ algebraic hierarchy ranging from setoids to vector spaces has been
+ developed. The resultant tools can be used to simplify the development
+ of generic theories about algebraic structures. In particular, the
+ benefits of using the tools presented in this paper, compared to a
+ from-scratch approach, are especially relevant when working with
+ complex mathematical structures; for example, the structures employed
+ in Algebraic Topology. This work shows that ACL2 can be a suitable
+ tool for formalising algebraic concepts coming, for instance, from
+ computer algebra systems."
+}
+
+\end{chunk}
+
\index{Hereman, Willy}
\begin{chunk}{axiom.bib}
@misc{Here96,
@@ -12539,6 +12681,26 @@ Vol. 8 No. 3 pp195-210 (2001)
\end{chunk}
+\index{Hoarau, Emma}
+\index{David, Claire}
+\begin{chunk}{axiom.bib}
+@article{Hoar08,
+ author = "Hoarau, Emma and David, Claire",
+ title = "Lie group computation of finite difference schemes",
+ year = "2008",
+ journal = "math.NA",
+ url = "http://arxiv.org/pdf/math/0611895.pdf",
+ paper = "Hoar08.pdf",
+ keywords = "axiomref",
+ abstract =
+ "A Mathematica based program has been elaborated in order to determine
+ the symmetry group of a finite difference equation. The package
+ provides functions which enabel use to solve the determining equations
+ of the related Lie group."
+}
+
+\end{chunk}
+
\index{Hodorog, Madalina}
\begin{chunk}{axiom.bib}
@phdthesis{Hodo11,
@@ -13210,6 +13372,27 @@ June 29, 1996
\end{chunk}
+\index{van Leeuwen, Andr\'e M.A.}
+\begin{chunk}{axiom.bib}
+@article{Leeu94,
+ author = "van Leeuwen, Andre M.A.",
+ title = "LiE, A software package for Lie group computations",
+ journal = "Euromath Bulletin",
+ volume = "1",
+ number = "2",
+ year = "1994",
+ keywords = "axiomref",
+ paper = "Leeu94.pdf",
+ abstract =
+ "A description is given of LiE, a specialized computer algebra package
+ for computations concerning Lie groups and algebras, and their
+ representations. The functionality of the package is demonstrated by
+ sample computations, and the structure of the program and the
+ algorithms implemented in it are discussed."
+}
+
+\end{chunk}
+
\index{Levelt, A. H. M.}
\begin{chunk}{ignore}
\bibitem[Levelt 95]{Lev95} Levelt, A. H. M. (ed)
@@ -13608,6 +13791,16 @@ IBM T.J. Watson Research RC4998
\subsection{O} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{chunk}{axiom.bib}
+@misc{ORMS,
+ author = "Unknown",
+ title = "Oberwolfach References on Mathematical Software",
+ url = "http://orms.mfo.de/project?id=234",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Ollivier, F.}
\begin{chunk}{ignore}
\bibitem[Ollivier 89]{Oll89} Ollivier, F.
@@ -14237,6 +14430,21 @@ IBM Manual, March 1988
\end{chunk}
\begin{chunk}{axiom.bib}
+@misc{Swmath,
+ author = "Unknown",
+ title = "Axiom",
+ url = "https://www.swmath.org/software/63",
+ keywords = "axiomref",
+ abstract =
+ "Axiom is a general purpose Computer Algebra System (CAS). It is
+ useful for research and developement of mathematical algorithms.
+ It defines a strongly typed, mathematically correct type hierarchy.
+ It has a programming language and a built-in compiler."
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
@misc{Sympy,
keywords = "axiomref",
url = "https://github.com/sympy/sympy/wiki/SymPy-vs.-Axiom"
@@ -14299,6 +14507,30 @@ Universit\'e de Limoges 1998
\subsection{V} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{van der Hoeven, Joris}
+\begin{chunk}{axiom.bib}
+@article{Hoev12,
+ author = "van der Hoeven, Joris",
+ title = "Overview of the Mathemagix type system",
+ journal = "ASCM 2102",
+ year = "2012",
+ keywords = "axiomref",
+ url = "http://www.texmacs.org/joris/mmxtyping/mmxtyping.pdf",
+ paper = "Hoev12.pdf",
+ abstract =
+ "The goal of the {\tt MATHEMAGIX} project is to develop a new and free
+ software for computer algebra and computer analysis, base on a
+ strongly typed and compiled language. In this paper, we focus on the
+ nderlying type system of this language, which allows for heavy
+ overloading, including parameterized overloading with parameters in so
+ called ``categories''. The exposition is informal and aims at giving
+ the reader an overview of the main concepts, ideas and differences
+ with existing languages. In a forthcoming paer, we intend to describe
+ the formal semantics of the type system in more detail."
+}
+
+\end{chunk}
+
+\index{van der Hoeven, Joris}
\begin{chunk}{ignore}
\bibitem[van der Hoeven 14]{JvdH14} van der Hoeven, Joris
title = "Computer algebra systems and TeXmacs",
@@ -14914,6 +15146,7 @@ Jones and Bartlett, 1992, ISBN 0-86720-293-9
keywords = "axiomref",
\end{chunk}
+
\section{Axiom Citations of External Sources}
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/changelog b/changelog
index bdae6d0..dd436be 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20160624 tpd src/axiom-website/patches.html 20160624.07.tpd.patch
+20160624 tpd books/bookvolbib Axiom Citations in the Literature
20160624 tpd src/axiom-website/patches.html 20160624.06.tpd.patch
20160624 tpd books/bookvol10.4 Arna95, Dave92, Jaes93 IntegerPrimesPackage
20160624 tpd books/bookvolbib Arna95, Dave92, Jaes93 IntegerPrimesPackage
diff --git a/patch b/patch
index fae43af..ba4dec1 100644
--- a/patch
+++ b/patch
@@ -1,72 +1,297 @@
-books/bookvolbib Arna95, Dave92, Jaes93 package IntegerPrimesPackage
+books/bookvolbib Axiom Citations in the Literature
Goal: Axiom Literate Programming
Collect algebra references in the bibliography
-\index{Arnault, Francois}
+\index{Rothstein, Michael}
+\index{Caviness, Bob F.}
\begin{chunk}{axiom.bib}
-@Article{Arna95,
- author = "Arnault, Francois",
- title = "Constructing Carmichael numbers which are strong pseudoprimes to
- several bases",
- year = "1995",
- journal = "Journal of Symbolic Computation",
- volume = "20",
+@article{Ro76a,
+ author = "Rothstein, Michael and Caviness, Bob F.",
+ title = "A structure theorem for exponential and primitive functions:
+ a preliminary report",
+ journal = "ACM Sigsam Bulletin",
+ volume = "10",
+ number = "4",
+ year = "1976",
+ paper = "Ro76a.pdf",
+ abstract =
+ "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{chunk}
+
+\index{Singer, Michael F.}
+\index{Saunders, B. David}
+\index{Caviness, Bob F.}
+\begin{chunk}{axiom.bib}
+@article{Sing85,
+ author = "Singer, Michael F. and Saunders, B. David and Caviness, Bob F.",
+ title = "An extension of Liouville's theorem on integration in finite terms",
+ journal = "SIAM J. of Comp.",
+ volume = "14",
+ pages = "965-990",
+ year = "1985",
+ url = "http://www4.ncsu.edu/~singer/papers/singer_saunders_caviness.pdf",
+ paper = "Sing85.pdf",
+ abstract =
+ "In Part 1 of this paper, we give an extension of Liouville's Theorem
+ and give a number of examples which show that integration with special
+ functions involves some phenomena that do not occur in integration
+ with the elementary functions alone. Our main result generalizes
+ Liouville's Theorem by allowing, in addition to the elementary
+ functions, special functions such as the error function, Fresnel
+ integrals and the logarithmic integral (but not the dilogarithm or
+ exponential integral) to appear in the integral of an elementary
+ function. The basic conclusion is that these functions, if they
+ appear, appear linearly. We give an algorithm which decides if an
+ elementary function, built up using only exponential functions and
+ rational operations has an integral which can be expressed in terms of
+ elementary functions and error functions."
+}
+
+\end{chunk}
+
+\index{Buchberger, Bruno}
+\index{Caviness, Bob F.}
+\begin{chunk}{axiom.bib}
+@book{Buch85,
+ author = "Buchberger, Bruno and Caviness, Bob F. (eds)",
+ title = "Lecture Notes in Computer Science, Vol 204",
+ isbn = "0-387-15983-5 (vol 1), 0-387-15984-3 (vol 2)",
+ year = "1985",
+ month = "April",
+ publisher = "Springer-Verlag, Berlin, Germany",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Kokol-voljc, Vlasta}
+\index{Kutzler, Bernhard}
+\begin{chunk}{axiom.bib}
+@misc{ACA00,
+ authors = "Kokol-voljc, Vlasta and Kutzler, Bernhard",
+ title = "Computer Algebra Meets Education",
+ keywords = "axiomref",
+ conference = "Sessions of ACA2000",
+ abstract =
+ "Education has become one of the fastest growing application areas for
+ computers in general and computer algebra in particular. Computer
+ algebra tools such as TI-92/89, Derive, Mathematica, Maple, Axiom,
+ Reduce, Macsyma, or Mupad make powerful teaching tools in mathematics,
+ physics, chemistry, biology, economy.
+
+ The goal of this session is to exchange ideas and experiences, to hear
+ about classroom experiments, and to discuss all issues related to the
+ use of computer algebra tools in the classroom (such as assessment,
+ change of curricula, new support material, ...)"
+}
+
+\end{chunk}
+
+\index{van Leeuwen, Andr\'e M.A.}
+\begin{chunk}{axiom.bib}
+@article{Leeu94,
+ author = "van Leeuwen, Andre M.A.",
+ title = "LiE, A software package for Lie group computations",
+ journal = "Euromath Bulletin",
+ volume = "1",
number = "2",
- pages = "151-161",
- paper = "Arna95.pdf",
+ year = "1994",
+ keywords = "axiomref",
+ paper = "Leeu94.pdf",
+ abstract =
+ "A description is given of LiE, a specialized computer algebra package
+ for computations concerning Lie groups and algebras, and their
+ representations. The functionality of the package is demonstrated by
+ sample computations, and the structure of the program and the
+ algorithms implemented in it are discussed."
+}
+
+\end{chunk}
+
+\index{Hoarau, Emma}
+\index{David, Claire}
+\begin{chunk}{axiom.bib}
+@article{Hoar08,
+ author = "Hoarau, Emma and David, Claire",
+ title = "Lie group computation of finite difference schemes",
+ year = "2008",
+ journal = "math.NA",
+ url = "http://arxiv.org/pdf/math/0611895.pdf",
+ paper = "Hoar08.pdf",
+ keywords = "axiomref",
+ abstract =
+ "A Mathematica based program has been elaborated in order to determine
+ the symmetry group of a finite difference equation. The package
+ provides functions which enabel use to solve the determining equations
+ of the related Lie group."
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@misc{Ency16,
+ author = "Unknown",
+ title = "Encyclopedia of Mathematics",
url =
- "http://ac.els-cdn.com/S0747717185710425/1-s2.0-S0747717185710425-main.pdf",
+ "https://www.encyclopediaofmath.org/index.php/Computer\_algebra\_package",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@misc{Swmath,
+ author = "Unknown",
+ title = "Axiom",
+ url = "https://www.swmath.org/software/63",
keywords = "axiomref",
- comment = "\newline\refto{package PRIMES IntegerPrimesPackage}",
- abstract =
- "We describe here a method of constructing Carmichael numbers which
- are strong pseudoprimes to some set of prime bases. We apply it to
- find composite numbers which are found to be prime by the Rabin-Miller
- test of packages as Axiom or Maple. We also use a variation of this
- method to construct strong Lucas pseudoprimes with respect to several
- pairs of parameters."
+ abstract =
+ "Axiom is a general purpose Computer Algebra System (CAS). It is
+ useful for research and developement of mathematical algorithms.
+ It defines a strongly typed, mathematically correct type hierarchy.
+ It has a programming language and a built-in compiler."
}
-\index{Davenport, James H.}
+\end{chunk}
+
+\index{Heras, Jonathan}
+\index{Martin-Mateos, Franciso Jesus}
+\index{Pascual, Vico}
+@article{Hera15,
+ author = "Heras, Jonathan and Martin-Mateos, Franciso Jesus and
+ Pascual, Vico",
+ title = "Modelling algebraic structures and morphisms in ACL2",
+ journal = "Appl. Algebra Eng. Commun. Comput.",
+ volume = "26",
+ number = "3",
+ pages = "277-303",
+ year = "2015",
+ keywords = "axiomref",
+ abstract =
+ "In this paper, we present how algebraic structures and morphisms can
+ be modelled in the ACL2 theorem prover. Namely, we illustrate a
+ methodology for implementing a set of tools that facilitates the
+ formalisations related to algebraic structures -- as a result, an
+ algebraic hierarchy ranging from setoids to vector spaces has been
+ developed. The resultant tools can be used to simplify the development
+ of generic theories about algebraic structures. In particular, the
+ benefits of using the tools presented in this paper, compared to a
+ from-scratch approach, are especially relevant when working with
+ complex mathematical structures; for example, the structures employed
+ in Algebraic Topology. This work shows that ACL2 can be a suitable
+ tool for formalising algebraic concepts coming, for instance, from
+ computer algebra systems."
+}
+
+\end{chunk}
+
+\index{Heras, Jonathan}
+\index{Martin-Mateos, Franciso Jesus}
+\index{Pascual, Vico}
\begin{chunk}{axiom.bib}
-@article{Dave92,
- author = "Davenport, James H.",
- title = "Primality Testing Revisited",
- url = "http://staff.bath.ac.uk/masjhd/ISSACs/ISSAC1992.pdf",
- paper = "Dave92.pdf",
- report = "Technical Report TR2/93 Numerical Algorithms Group, Inc",
+@misc{Hera16,
+ author = "Heras, Jonathan and Martin-Mateos, Franciso Jesus and
+ Pascual, Vico",
+ title = "A Hierarchy of Mathematical Structures in ACL2",
keywords = "axiomref",
- comment = "\newline\refto{package PRIMES IntegerPrimesPackage}",
+ paper = "Hera16.pdf",
+ url = "http://staff.computing.dundee.ac.uk/jheras/papers/ahomsia.pdf",
abstract =
- "Rabin's algorithm is commonly used in computer algebra systems and
- elsewhere for primality testing. This paper presents an experience
- with this in the Axiom computer algebra system. As a result of this
- experience, we suggest certain strengthenings of the algorithm."
+ "In this paper, we present a methodology which allows one to deal with
+ {\sl mathematical structures} in the ACL2 theorem prover. Namely, we
+ cope with the representation of mathematical structures, the
+ certification that an object fulfills the axioms characterizing an
+ algebraic structure and the generation of generic theories about
+ concrete structures. As a by-product, an {\sl ACL2 algebraic
+ hierarchy} has been obtained. Our framework has been tested with the
+ definition of {\sl homology groups}, an example coming from
+ Homological Algebra which involves several notions related to
+ Universal Algebra. The method presented here, when compared to a
+ from-scratch approach, is preferred when working with complex
+ mathematical structures; for instance, the ones coming from Algebraic
+ Topology. The final aim of this work is the verification of Computer
+ Algebra systems, a field where our hierarchy fits better than the ones
+ developed in other systems."
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@misc{ORMS,
+ author = "Unknown",
+ title = "Oberwolfach References on Mathematical Software",
+ url = "http://orms.mfo.de/project?id=234",
+ keywords = "axiomref"
}
\end{chunk}
-\index{Jaeschke, Gerhard}
+\index{Ballarin, Clemens}
\begin{chunk}{axiom.bib}
-@article{Jaes93,
- author = "Jaeschke, Gerhard",
- title = "On String Pseudoprimes to Several Bases",
- journal = "Mathematics of Computation",
- volume = "61",
- number = "204",
- year = "1993",
- pages = "915-926",
- paper = "Jaes93.pdf",
+@article{Ball14,
+ author = "Ballarin, Clemens",
+ title = "Locales: a module system for mathematical theories",
+ journal = "J. Autom. Reasoning",
+ volume = "52",
+ number = "2",
+ pages = "123-153",
+ year = "2014",
keywords = "axiomref",
- comment = "\newline\refto{package PRIMES IntegerPrimesPackage}",
+ url = "http://www21.in.tum.de/~ballarin/publications/jar2013.pdf",
+ paper = "Ball14.pdf",
abstract =
- "With $\psi_k$ denoting the smallest strong pseudoprime to all of the
- first $k$ primes taken as bases we determine the exact values for
- $\psi_5$, $\psi_6$, $\psi_7$, $\psi_8$, and give upper bounds for
- $\psi_9$, $\psi_{10}$, $\psi_{11}$. We discuss the methods and
- underlying facts for obtaining these results"
+ "Locales are a module system for managing theory hierarchies in a
+ theorem prover through theory interpretation. They are available for
+ the theorem prover Isabelle. In this paper, their semantics is defined
+ in terms of local theories and morphisms. Locales aim at providing
+ flexible means of extension and reuse. Theory modules (which are
+ called locales) may be extended by definitions and
+ theorems. Interpretation of Isabelle's global theories and proof
+ contexts is possible via morphisms. Even the locale hierarchy may be
+ changed if declared relations between locales do not adequately
+ reflect logical relations, which are implied by the locales'
+ specifications. By discussing their design and relating it to more
+ commonly known structuring mechanisms of programming languages and
+ provers, locales are made accessible to a wider audience beyond the
+ users of Isabelle. The discussed mechanisms include ML-style functors,
+ type classes and mixins (the latter are found in modern
+ object-oriented languages)."
+}
+
+\end{chunk}
+
+\index{van der Hoeven, Joris}
+\begin{chunk}{axiom.bib}
+@article{Hoev12,
+ author = "van der Hoeven, Joris",
+ title = "Overview of the Mathemagix type system",
+ journal = "ASCM 2102",
+ year = "2012",
+ keywords = "axiomref",
+ url = "http://www.texmacs.org/joris/mmxtyping/mmxtyping.pdf",
+ paper = "Hoev12.pdf",
+ abstract =
+ "The goal of the {\tt MATHEMAGIX} project is to develop a new and free
+ software for computer algebra and computer analysis, base on a
+ strongly typed and compiled language. In this paper, we focus on the
+ nderlying type system of this language, which allows for heavy
+ overloading, including parameterized overloading with parameters in so
+ called ``categories''. The exposition is informal and aims at giving
+ the reader an overview of the main concepts, ideas and differences
+ with existing languages. In a forthcoming paer, we intend to describe
+ the formal semantics of the type system in more detail."
}
\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index b886109..edac3eb 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5374,6 +5374,8 @@ books/bookvolbib Lamb92 category FMCAT FreeModuleCat

books/bookvolbib Add Axiom Citations in the Literature

20160624.06.tpd.patch
books/bookvolbib Arna95, Dave92, Jaes93 IntegerPrimesPackage

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

--
1.7.5.4