From db5eeb22a82a312958585419f33b00f81b094921 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 5 Sep 2017 20:40:01 -0400
Subject: [PATCH] books/bookvol3 Additional explanations and references
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Goal: Proving Axiom Correct
\index{Bertoli, P.}
\index{Calmet, J.}
\index{Guinchiglia, F.}
\index{Homann, K.}
\begin{chunk}{axiom.bib}
@article{Bert98,
author = "Bertoli, P. and Calmet, J. and Guinchiglia, F. and Homann, K.",
title = "Specification and Integration of Theorem Provers and Computer
Algebra Systems",
journal = "Lecture Notes in Computer Science",
volume = "1476",
year = "1998",
pages = "94-106",
abstract =
"Computer algebra systems (CASs) and automated theorem provers (ATPs)
exhibit complementary abilities. CASs focus on efficiently solving
domain-specific problems. ATPs are designed to allow for the
formalization and solution of wide classes of problems within some
logical framework. Integrating CASs and ATPs allows for the solution
of problems of a higher complexity than those confronted by each class
alone. However, most experiments conducted so far followed an ad-hoc
approach, resulting in tailored solutions to specific problems. A
structured and principled approach is necessary to allow for the sound
integration of systems in a modular way. The Open Mechanized Reasoning
Systems (OMRS) framework was introduced for the specification and
implementation of mechanized reasoning systems, e.g. ATPs. The
approach was recasted to the domain of computer algebra systems. In
this paper, we introduce a generalization of OMRS, named OMSCS (Open
Mechanized Symbolic Computation Systems). We show how OMSCS can be
used to soundly express CASs, ATPs, and their integration, by
formalizing a combination between the Isabelle prover and the Maple
algebra system. We show how the integrated system solves a problem
which could not be tackled by each single system alone.",
paper = "Bert98.pdf"
}
\end{chunk}
\index{Dolzmann, Andreas},
\index{Sturm, Thomas}
\begin{chunk}{axiom.bib}
@article{Dolz97b,
author = "Dolzmann, Andreas and Sturm, Thomas",
title = "REDLOG: Computer Algebra meets Computer Logic",
journal = "ACM SIGSAM Bulletin",
volume = "31",
number = "2",
year = "1997",
pages = "2-9",
abstract =
"REDLOG is a package that extends the computer algebra system REDUCE
to a computer logic system, i.e., a system that provides algorithms
for the symbolic manipulation of first-order formulas over some
temporarily fixed language and theory. In contrast to theorem provers,
the methods applied know about the underlying algebraic theory and
make use of it. We illustrate some applications of REDLOG, describe
its functionality as it appears to the user, and explain the design
issues and implementation techniques. REDLOG is available on the WWW.",
paper = "Dolz97b.pdf"
}
\end{chunk}
\index{Calmet, Jacques}
\index{Homann, Karsten}
\begin{chunk}{axiom.bib}
@book{Calm96,
author = "Calmet, Jacques and Homann, Karsten",
title = "Classification of Communication and Cooperation Mechanisms for
Logical and Symbolic Computation Systems",
booktitle = "Frontiers of Combining Systems",
publisher = "Kluwer Academic",
year = "1996",
pages = "221-234",
abstract =
"The combination of logical and symbolic computation systems has
recently emerged from prototype extensions of stand-alone systems to
the study of environments allowing interaction among several
systems. Communication and cooperation mechanisms of systems
performing any kind of mathematical service enable one to study and
solve new classes of problems and to perform efficient computation by
distributed specialized packages. The classification of communication
and cooperation methods for logical and symbolic computation systems
given in this paper provides and surveys different methodologies for
combining mathematical services and their characteristics,
capabilities, requirements, and differences. The methods are
illustrated by recent well-known examples. We separate the
classification into communication and cooperation methods. The former
includes all aspects of the physical connection, the flow of
mathematical information, the communication language(s) and its
encoding, encryption, and knowledge sharing. The latter concerns the
semantic aspects of architectures for cooperative problem solving.",
paper = "Calm96.pdf"
}
\end{chunk}
\index{Dowek, Gilles}
\begin{chunk}{axiom.bib}
@article{Dowe00,
author = "Dowek, Gilles",
title = "Axioms vs Rewrite Rules: From Completeness to Cut Elimination",
journal = "Lecture Notes in Computer Science",
volume = "1794",
pages = "62-72",
year = "2000",
abstract =
"Combining a standard proof search method, such as resolution or
tableaux, and rewriting is a powerful way to cut off search space in
automated theorem proving, but proving the completeness of such
combined methods may be challenging. It may require in particular to
prove cut elimination for an extended notion of proof that combines
deductions and computations. This suggests new interactions between
automated theorem proving and proof theory.",
paper = "Dowe00.pdf"
}
\end{chunk}
\index{Sorge, Volker}
\begin{chunk}{axiom.bib}
@article{Sorg00,
author = "Sorge, Volker",
title = "Non-trivial Symbolic Computations in Proof Planning",
journal = "LNCS",
volume = "1794",
pages = "121-135",
year = "2000",
abstract =
"We discuss a pragmatic approach to integrate computer algebra into
proof planning. It is based on the idea to separate computation and
verification and can thereby exploit the fact that many elaborate
symbolic computations are trivially checked. In proof planning the
separation is realized by using a powerful computer algebra system
during the planning process to do non-trivial symbolic
computations. Results of these computations are checked during the
refinement of a proof plan to a calculus level proof using a small,
self-implemented system that gives us protocol information on its
calculation. This protocol can be easily expanded into a checkable
low-level calculus proof ensuring the correctness of the
computation. We demonstrate our approach with the concrete
implementation in the $\Omega$MEGA system.",
paper = "Sorg00.pdf"
}
\end{chunk}
\index{Melham, Thomas F.}
\begin{chunk}{axiom.bib}
@article{Melh02,
author = "Melham, Thomas F.",
title = "PROSPER An Investigation into Software Architecture for Embedded
Proof Engines",
journal = "LNCS",
volume = "2309",
pages = "193-206",
year = "2002",
abstract =
"Prosper is a recently-completed ESPRIT Framework IV research project
that investigated software architectures for component-based, embedded
formal verification tools. The aim of the project was to make
mechanized formal analysis more accessible in practice by providing a
framework for integrating formal proof tools inside other software
applications. This paper is an extended abstract of an invited
presentation on Prosper given at FroCoS 2002. It describes the vision
of the Prosper project and provides a summary of the technical
approach taken and some of the lessons learned.",
paper = "Melh02.pdf"
}
\end{chunk}
\index{Adams, Andrew A.}
\index{Gottlieben, Hanne}
\index{Linton, Steve A.}
\index{Martin, Ursula}
\begin{chunk}{axiom.bib}
@inproceedings{Adam99,
author = "Adams, Andrew A. and Gottlieben, Hanne and Linton, Steve A. and
Martin, Ursula",
title = "Automated theorem proving in support of computer algebra:
symbolic definite integration as a case study",
booktitle = "ISSAC '99",
pages = "253-260",
year = "1999",
abstract = "
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.",
paper = "Adam99.pdf"
\end{chunk}
\index{Buchberger, B.}
\index{Jebelean, Tudor}
\index{Kriftner, Franz}
\index{Vasaru, Daniela}
\begin{chunk}{axiom.bib}
@inproceedings{Buch77,
author = "Buchberger, B. and Jebelean, Tudor and Kriftner, Franz and
Vasaru, Daniela",
title = "A Survey on the Theorema Project",
booktitle = "ISSAC '97",
year = "1997",
abstract =
"The Theorema project aims at extending current computer algebra
systems by facilities for supporting mathematical proving. The present
early-prototype version of the Theorema software system is implemented
in Mathematica 3.0. The system consists of a general higher-order
predicate logic prover and a collection of special provers that call
each other depending on the particular proof situations. The
individual provers imitate the proof style of human mathematicians and
aim at producing human-readable proofs in natural language presented
in nested cells that facilitate studying the computer-generated proofs
at various levels of detail. The special provers are intimately
connected with the functors that build up the various mathematical
domains.",
paper = "Buch77.pdf"
}
\end{chunk}
\index{Clarke, Edmund}
\index{Zhao, Xudong}
\begin{chunk}{axiom.bib}
@techreport{Clar94,
author = "Clarke, Edmund and Zhao, Xudong",
title = "Combining Symbolic Computation and Theorem Proving: Some
Problems of Ramanujan",
year = "1994",
type = "technical report",
institution = "Carnegie Mellon University",
number = "CMU-CS-94-103",
abstract =
"One way of building more powerful theorem provers is to use
techniques from symbolic computation. The challenge problems in this
paper are taken from Chapter 2 of Ramanujan''s Notebooks. They were
selected because they are non-trivial and require the use of symbolic
computation techniques. We have developed a theorem prover based on
the symbolic computation system Mathematica, that can prove all the
challenge problems completely automatically. The axioms and inference
rules for constructing the proofs are also briefly discussed.",
paper = "Clar94.pdf",
keywords = "CAS-Proof"
}
\end{chunk}
\index{de Bruijn, N.G.}
\begin{chunk}{axiom.bib}
@article{Brui94,
author = "de Bruijn, N.G.",
title = "A Survey on the project Automath",
journal = "Studies in Logic and the Foundations of Mathematics",
volume = "133",
year = "1994",
pages = "141-161",
abstract =
"Thus far, much about Automath has been written in separate
reports. Most of this work has been made available upon request, but
only a small part was published in journals, conference proceedings,
etc. Unfortunately, a general survey in the form of a book is still
lacking. A short survey was given in [de Bruijn 73c], but the present
one will be much more extensive. Naturally, this survey will report
about work that has been done, is going on, or is planned for the
future. But it will also be used to explain how various parts of the
project are related. Moreover we shall try to clarify a few points
which many outsiders consider as uncommon or even wierd. In particular
we spend quite some attention to our concept of types and the matter
of ``propositions as types'' (Section 14). Finally the survey will be
used to ventilate opinions and views in mathematics which are not
easily set down in more technical reports.",
paper = "Brui94.pdf"
}
\end{chunk}
\index{Dutertre, Bruno}
\begin{chunk}{axiom.bib}
@article{Dute96,
author = "Dutertre, Bruno",
title = "Elements of Mathematical Analysis in PVS",
journal = "LNCS",
volume = "1125",
pages = "141-156",
year = "1996",
abstract =
"This paper presents the formalization of some elements of
mathematical analysis using the PVS verification system. Our main
motivation was to extend the existing PVS libraries and provide means
of modelling and reasoning about hybrid systems. The paper focuses on
several important aspects of PVS including recent extensions of the
type system and discusses their merits and effectiveness. We conclude
by a brief comparison with similar developments using other theorem
provers.",
paper = "Dute96.pdf"
}
\end{chunk}
\index{Homann, Karsten}
\index{Calmet, Jacques}
\begin{chunk}{axiom.bib}
@article{Homa94,
author = "Homann, Karsten and Calmet, Jacques",
title = "Combining Theorem Proving and Symbolic Mathematical Computing",
journal = "LNCS",
volume = "958",
pages = "18-29",
year = "1994",
abstract =
"An intelligent mathematical environment must enable symbolic
mathematical computation and sophisticated reasoning techniques on the
underlying mathematical laws. This paper disscusses different possible
levels of interaction between a symbolic calculator based on algebraic
algorithms and a theorem prover. A high level of interaction requires
a common knowledge representation of the mathematical knowledge of the
two systems. We describe a model for such a knowledge base mainly
consisting of type and algorithm schemata, algebraic algorithms and
theorems.",
paper = "Homa94.pdf",
keywords = "CAS-Proof"
}
\end{chunk}
\index{Kredel, Heinz}
\begin{chunk}{axiom.bib}
@article{Kred90,
author = "Kredel, Heinz",
title = "MAS Modula-2 Algebra System",
journal = "LNCS",
volume = "429",
pages = "270-271",
year = "1990",
keywords = "axiomref"
}
\end{chunk}
\index{Fortenbacher, Albrecht}
\begin{chunk}{axiom.bib}
@article{Fort87,
author = "Fortenbacher, Albrecht",
title = "An Algebraic Approach to Unification Under Associativity and
Commutativity",
journal = "J. Symbolic Computation",
volume = "3",
pages = "217-229",
year = "1987",
abstract =
"From the work of Siekmann & Livesey, and Stickel it is known how to
unify two terms in an associative and commutative theory: transfer the
terms into Abelian strings, look for mappings which solve the problem
in the Abelian monoid, and decide whether a mapping can be regarded as
a unifier. Very often most of the mappings are thus eliminated, and
so it is crucial for efficiency either to not create these unnecessary
solutions or to remove them as soon as possible. The following work
formalises the transformations between the free algebra and this
monoid. This leads to an algorithm which uses maximal information for
its search for solutions in the monoid. It is both very efficient and
easily verifiable. Some applications of this algorithm are shown in
the appendix.",
paper = "Fort87.pdf"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@book{ADAx83,
author = "U.S. Government",
title = "The Programming Language Ada Reference Manual",
publisher = "U.S. Government",
year = "1983",
comment = "STD-1815A-1983"
}
\end{chunk}
\index{Ausiello, Giovanni Francesco Mascari}
\begin{chunk}{axiom.bib}
@article{Ausi79,
author = "Ausiello, Giovanni Francesco Mascari",
title = "On the Design of Algebraic Data Structures with the
Approach of Abstract Data Types",
journal = "LNCS",
volume = "72",
year = "1979",
pages = "514-530",
abstract =
"The problem of giving a formal definition of the representation of
algebraic data structures is considered and developped in the frame
work of the abstract data types approach. Such concepts as canonical
form and simplification are formalized and related to properties of
the abstract specification and of the associated term rewriting
system.",
paper = "Ausi79.pdf"
}
\end{chunk}
\index{Burstall, R.M.}
\index{Goguen, J.A.}
\begin{chunk}{axiom.bib}
@inproceedings{Burs77,
author = "Burstall, R.M. and Goguen, J.A.",
title = "Putting THeories together to make Specifications",
booktitle = "IJCAI 77 Volume 2",
pages = "1045-1058",
year = "1977",
paper = "Burs77.pdf"
}
\end{chunk}
\index{Cohn, Paul Moritz}
\begin{chunk}{axiom.bib}
@book{Cohn65,
author = "Cohn, Paul Moritz",
title = "Universal Algebra",
publisher = "Harper and Row",
year = "1965"
}
\end{chunk}
\index{Davenport, J.H.}
\index{Jenks, R.D.}
\begin{chunk}{axiom.bib}
@misc{Dave80b,
author = "Davenport, J.H. and Jenks, R.D.",
title = "SCRATCHPAD/370: Modes and Domains",
year = "1980",
comment = "private communication"
}
\end{chunk}
\index{Demers, A.}
\index{Donahue, J.}
\begin{chunk}{axiom.bib}
@techreport{Deme79,
author = "Demers, A. and Donahue, J.",
title = "Revised Report on RUSSELL",
year = "1979",
type = "technical report",
institution = "Cornell",
number = "TR 79-389"
}
\end{chunk}
\index{Griss, Martin L.}
\begin{chunk}{axiom.bib}
@inproceedings{Gris76,
author = "Griss, Martin L.",
title = "The Definition and Use of Data Structures in REDUCE",
booktitle = "SYMSAC '76",
pages = "53-59",
year = "1976",
abstract =
"This paper gives a brief description and motivation of the mode
analyzing and data-structuring extensions to the algebraic language
REDUCE. These include generic functions, user defined recursive data
structures, mode transfer functions and user modifiable automatic
coercion. A number of examples are given to illustrate the style and
features of the language, and how it will aid in the construction of
more efficient and reliable programs."
}
\end{chunk}
\index{Loos, Ruediger G. K.}
\begin{chunk}{axiom.bib}
@article{Loos74,
author = "Loos, Ruediger G. K.",
title = "Toward a Formal Implementation of Computer Algebra",
journal = "SIGSAM",
volume = "8",
number = "3",
pages = "9-16",
year = "1974",
abstract =
"We consider in this paper the task of synthesizing an algebraic
system. Today the task is significantly simpler than in the pioneer
days of symbol manipulation, mainly because of the work done by the
pioneers in our area, but also because of the progress in other areas
of Computer Science. There is now a considerable collection of
algebraic algorithms at hand and a much better understanding of data
structures and programming constructs than only a few years ago.",
paper = "Loos74.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Levenworth, B.}
\begin{chunk}{axiom.bib}
@misc{Leve80,
author = "Levenworth, B.",
title = "ADAPT Reference Manual",
comment = "IBM Research",
year = "1980"
}
\end{chunk}
\index{Wegbreit, Ben}
\begin{chunk}{axiom.bib}
@article{Wegb74,
author = "Wegbreit, Ben",
title = "The Treatment of Data Types in EL1",
journal = "Communications of the ACM",
volume = "17",
number = "5",
year = "1974",
pages = "251-264",
abstract =
"In constructing a general purpose programming language, a key issue
is providing a sufficient set of data types and associated operations
in a manner that permits both natural problem-oriented notation and
efficient implementation. The EL1 language contains a number of
features specifically designed to simultaneously satisfy both
requirements. The resulting treatment of data types includes provision
for programmer-defined data types and generaic routines, programmer
control over type conversion, and very flexible data type behavior, in
a context that allows efficient compiled code and compact data
representation.",
paper = "Wegb74.pdf"
}
\end{chunk}
\index{Wulf, William A.}
\index{London, Ralph L.}
\index{Shaw, Mary}
\begin{chunk}{axiom.bib}
@article{Wulf76,
author = "Wulf, William A. and London, Ralph L. and Shaw, Mary",
title = "An Introduction to the Construction and Verification of
Alphard Programs",
journal = "IEEE Tr. Software Engineering",
volume = "SE-2",
number = "4",
year = "1976",
pages = "253-265",
abstract =
"The programming language Alphard is designed to provide support for
both the methodologies of ``well-structured'' programming and the
techniques of formal program verification. Language constructs allow
a programmer to isolate an abstraction, specifying its behavior
publicly while localizing. knowledge about its implementation. The
verification of such an abstraction consists of showing that its
implementation behaves in accordance with its public specifications;
the abstraction can then be used with confidence in constructing
other programs, and the verification of that use employs only the
public specifications. This paper introduces Alphard by developing
and verifying a data structure definition and a program that uses it.
It shows how each language construct contributes to the development of
the abstraction and discusses the way the language design and the
verification methodology wete tailored to each other. It serves not
only as an introduction to Alphard, but also as an example of the
symbiosis between verification and methodology in language design.
The strategy of program structuring, illustrated for Alphard, is
also applicable to most of the "data abstraction" mechanisms now
appearing.",
paper = "Wulf76.pdf"
}
\end{chunk}
\index{Astesiano, Egidio}
\index{Bidoit, Michel}
\index{Kirchner, Helene}
\index{Krieg-Bruckner, Bernd}
\index{Mosses, Peter D.}
\index{Sannella, Donald}
\index{Tarlecki, Andrzej}
\begin{chunk}{axiom.bib}
@article{Aste02,
author = "Astesiano, Egidio and Bidoit, Michel and Kirchner, Helene and
Krieg-Bruckner, Bernd and Mosses, Peter D. and Sannella, Donald
and Tarlecki, Andrzej",
title = "CASL: the Common Algebraic Specification Language",
journal = "Theoretical Computer Science",
volume = "286",
number = "2",
pages = "153-196",
year = "2002",
abstract =
"The Common Algebraic Specification Language (CASL) is an expressive
language for the formal specification of functional requirements and
modular design of software. It has been designed by COFI, the
international Common Framework Initiative for algebraic specification
and development. It is based on a critical selection of features that
have already been explored in various contexts, including subsorts,
partial functions, first-order logic, and structured and architectural
specifications. CASL should facilitate interoperability of many
existing algebraic prototyping and verification tools.
This paper gives an overview of the CASL design. The major issues that
had to be resolved in the design process are indicated, and all the
main concepts and constructs of CASL are briefly explained and
illustrated — the reader is referred to the CASL Language Summary for
further details. Some familiarity with the fundamental concepts of
algebraic specification would be advantageous.",
paper = "Aste02.pdf"
}
\end{chunk}
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@article{Dave90a,
author = "Davenport, James H.",
title = "Current Problems in Computer Algebra Systems Design",
journal = "LNCS",
volume = "429",
year = "1990",
pages = "1-9",
abstract =
"Computer Algebra systems have been with us for over twenty years, but
there is still no consensus on what an ``ideal'' system would look
like. There are all sorts of tradeoffs between portability,
functionality, and efficiency. This paper discusses some of those issues.",
keywords = "axiomref"
}
\end{chunk}
\index{Galligo, A.}
\index{Grimm, J.}
\index{Pottier, L.}
\begin{chunk}{axiom.bib}
@article{Gall90,
author = "Galligo, A. and Grimm, J. and Pottier, L.",
title = "The Design of SISYPHE: A System for doing Symbolic and
Algebraic Computations",
journal = "LNCS",
volume = "429"
pages = "30-39",
year = "1990"
keywords = "axiomref"
}
\end{chunk}
---
books/axiom.bib | 701 +++++++++++++++++++++++++++++++---
books/bookvol3.pamphlet | 563 +++++++++++++++++++++++++++
books/bookvolbib.pamphlet | 842 ++++++++++++++++++++++++++++++++++++++---
changelog | 4 +
patch | 665 +++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
6 files changed, 2679 insertions(+), 98 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index debf098..a184cd6 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -1666,7 +1666,8 @@ paper = "Brea89.pdf"
components may be combined to solve scientific problems that can not
be solved within a single CAS, or may be organised into a system for
distributed parallel computations.",
- paper = "Lint10.pdf"
+ paper = "Lint10.pdf",
+ keywords = "CAS-Proof"
}
@article{Loos72,
@@ -1721,7 +1722,7 @@ paper = "Brea89.pdf"
algebraic algorithms at hand and a much better understanding of data
structures and programming constructs than only a few years ago.",
paper = "Loos74.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@book{Loos92,
@@ -5790,7 +5791,8 @@ paper = "Brea89.pdf"
numbers in the Maple computer algebra system. Exact reals are
represented by potentially infinite lists of binary digits, and
interpreted as sums of negative powers of the golden ratio.",
- paper = "Kels00.pdf"
+ paper = "Kels00.pdf",
+ keywords = "CAS-Proof"
}
@article{Knus98,
@@ -6643,6 +6645,35 @@ paper = "Brea89.pdf"
paper = "Acze13.pdf"
}
+@inproceedings{Adam99,
+ author = "Adams, Andrew A. and Gottlieben, Hanne and Linton, Steve A. and
+ Martin, Ursula",
+ title = "Automated theorem proving in support of computer algebra:
+ symbolic definite integration as a case study",
+ booktitle = "ISSAC '99",
+ pages = "253-260",
+ year = "1999",
+ abstract = "
+ 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.",
+ paper = "Adam99.pdf",
+ keywords = "axiomref, CAS-Proof"
+}
+
@InProceedings{Adam01,
author = "Adams, Andrew A. and Dunstan, Martin and Gottlieben, Hanne and
Kelsey, Tom and Martin, Ursula and Owre, Sam",
@@ -6663,7 +6694,7 @@ paper = "Brea89.pdf"
library. These examples provide proofs which are both illustrative and
applicable to genuine symbolic computation problems.",
paper = "Adam01.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Ager88,
@@ -6736,7 +6767,8 @@ paper = "Brea89.pdf"
title = "LEAN proof of GCD",
link =
"\url{http://github.com/leanprover/lean2/blob/master/library/data/nat/gcd.lean}",
- year = "2014"
+ year = "2014",
+ keywords = "CAS-Proof"
}
@misc{Avig16,
@@ -6778,7 +6810,8 @@ paper = "Brea89.pdf"
we specify syntax translations for the concrete syntax of Maple
which enables the communication between both systems illustrated by
some examples that can be solved by theorems and algorithms",
- paper = "Ball95.pdf"
+ paper = "Ball95.pdf",
+ keywords = "CAS-Proof"
}
@@ -6802,7 +6835,8 @@ paper = "Brea89.pdf"
experimental interface therefore uses a computer algebra library. It
is based on theorem templates, which provide formal specifications for
the algorithms.",
- paper = "Ball98.pdf"
+ paper = "Ball98.pdf",
+ keywords = "CAS-Proof"
}
@article{Ball99,
@@ -6835,7 +6869,7 @@ paper = "Brea89.pdf"
system on the tactic-level of Isabelle and its integration into proof
procedures.",
paper = "Ball99.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@article{Bare01,
@@ -6875,7 +6909,8 @@ paper = "Brea89.pdf"
Some examples of communication forms are given that show how the
participants benefit",
- paper = "Bare01.pdf"
+ paper = "Bare01.pdf",
+ keywords = "CAS-Proof"
}
@article{Baue16,
@@ -7131,7 +7166,7 @@ paper = "Brea89.pdf"
exactly the mathematical dependencies between different structures.
This may ease the achievement of proofs.",
paper = "Boul99.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@techreport{Boul94,
@@ -7413,7 +7448,8 @@ paper = "Brea89.pdf"
title = "Analytica -- A Theorem Prover in Mathematica",
year = "1991",
link = "\url{http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Analytica%20A%20Theorem%20Prover%20in%20Mathematica.pdf}",
- paper = "Clar91.pdf"
+ paper = "Clar91.pdf",
+ keywords = "CAS-Proof"
}
@article{Como88,
@@ -7545,7 +7581,7 @@ paper = "Brea89.pdf"
our claim that the Nuprl proof development system is especially well
suited to support this kind of mathematics.",
paper = "Cons98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@InProceedings{Dani06,
@@ -7604,7 +7640,8 @@ paper = "Brea89.pdf"
year = "2017",
comment = "BPR presentation, Cambridge, England",
video = "Dave17a.mp4",
- paper = "Dave17a.pdf"
+ paper = "Dave17a.pdf",
+ keywords = "CAS-Proof"
}
@book{Dijk76,
@@ -7727,7 +7764,7 @@ paper = "Brea89.pdf"
a modest cost. Our approach is based on retargeting the code generator
of the OpenAxiom compiler to the Poly/ML abstract machine.",
paper = "Dosr11.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@InProceedings{Duns98,
@@ -7746,7 +7783,7 @@ paper = "Brea89.pdf"
methodology for Aldor program analysis and verification. There are
examples of abstract specifications of Axiom primitives.",
paper = "Duns98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@phdthesis{Duns99a,
@@ -7786,7 +7823,7 @@ paper = "Brea89.pdf"
case study of abstract specifications of AXIOM primitives, and provide
an interface between these abstractions and Aldor code.",
paper = "Duns99.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Fate02a,
@@ -7814,7 +7851,7 @@ paper = "Brea89.pdf"
execution of the algorithms, equivalent to testing over infinite test
sets, aids in debugging, while strengthening beliefs that the correctness
of results is an algebraic truth rather than an accident.",
- paper = "Fate02a.pdf"
+ paper = "Fate02a.pdf, CAS-Proof"
}
@inproceedings{Fate03a,
@@ -7845,7 +7882,8 @@ paper = "Brea89.pdf"
sketch a proof of a numerical program to compute sine, and display a
related approach to a version of a Bessel function algorithm for J0(x)
based on a recurrence.",
- paper = "Fate03a.pdf"
+ paper = "Fate03a.pdf",
+ keywords = "CAS-Proof"
}
@article{Frad08,
@@ -7960,7 +7998,7 @@ paper = "Brea89.pdf"
practice. Apart rom the inheritance and reuse of properties, the
algebraic hierarchy has proven very useful for reusing notations.",
paper = "Geuv02.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Gime16,
@@ -8030,7 +8068,7 @@ paper = "Brea89.pdf"
of verification conditions, harnesses to ensure more reliable
differential equation solvers, and verifiable look-up tables.",
paper = "Gott05.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Grab17,
@@ -8126,7 +8164,7 @@ paper = "Brea89.pdf"
reals which combines the rigour of a theorem prover with the power of
a computer algebra system.",
paper = "Harr94.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Heer02,
@@ -8252,7 +8290,7 @@ paper = "Brea89.pdf"
algebra system and the relevance of this work for abstract functional
programming.",
paper = "Jack94.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@phdthesis{Jack95,
@@ -8305,7 +8343,7 @@ paper = "Brea89.pdf"
discusses the appropriateness of this foundation, and the extent to
which the work relied on it.",
paper = "Jack95.pdf",
- keyword = "axiomref"
+ keyword = "axiomref, CAS-Proof"
}
@misc{Juds16,
@@ -8340,7 +8378,7 @@ paper = "Brea89.pdf"
prototype, but can be straightforwardly scaled up to a practical
computer algebra system.",
paper = "Kali07.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Kauf98,
@@ -8407,7 +8445,7 @@ paper = "Brea89.pdf"
well-suited for producing a high-level verbalised explication as well
as for a low-level (machine checkable) calculus-level proof.",
paper = "Kerb96.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@article{Kome11,
@@ -8430,7 +8468,8 @@ paper = "Brea89.pdf"
protocol known as SC- SCP. We describe general aspects of viewing
OpenMath terms produced by a CAS in the calculus of Coq, as well as
viewing pure Coq terms in a simpler type system that is behind OpenMath.",
- paper = "Kome11.pdf"
+ paper = "Kome11.pdf",
+ keywords = "CAS-Proof"
}
@phdthesis{Kreb15,
@@ -8876,7 +8915,8 @@ paper = "Brea89.pdf"
given by the approach. The {\tt Agda} functional language is used as an
instrument. This paper is a continuation for the introductory paper
published in this journal in 2014. (In Russian)",
- paper = "Mesh15.pdf"
+ paper = "Mesh15.pdf",
+ keywords = "CAS-Proof"
}
@book{Mesh16,
@@ -9319,7 +9359,7 @@ paper = "Brea89.pdf"
The paper shows an interesting way to decorate Axiom with pre- and
post-conditions.",
paper = "Poll98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Poll99,
@@ -9347,10 +9387,13 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
-@misc{Poll00,
+@article{Poll00,
author = "Poll, Erik and Thompson, Simon",
title = "Integrating Computer Algebra and Reasoning through the Type
System of Aldor",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1794",
+ pages = "136-150",
year = "2000",
abstract =
"A number of combinations of reasoning and computer algebra systems
@@ -9474,7 +9517,7 @@ paper = "Brea89.pdf"
given algorithm a set of theorems that imply the correctness of this
algorithm.",
paper = "Schw97.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Seli13,
@@ -10002,6 +10045,30 @@ paper = "Brea89.pdf"
paper = "Dave86.pdf"
}
+@article{Fort87,
+ author = "Fortenbacher, Albrecht",
+ title = "An Algebraic Approach to Unification Under Associativity and
+ Commutativity",
+ journal = "J. Symbolic Computation",
+ volume = "3",
+ pages = "217-229",
+ year = "1987",
+ abstract =
+ "From the work of Siekmann and Livesey, and Stickel it is known how to
+ unify two terms in an associative and commutative theory: transfer the
+ terms into Abelian strings, look for mappings which solve the problem
+ in the Abelian monoid, and decide whether a mapping can be regarded as
+ a unifier. Very often most of the mappings are thus eliminated, and
+ so it is crucial for efficiency either to not create these unnecessary
+ solutions or to remove them as soon as possible. The following work
+ formalises the transformations between the free algebra and this
+ monoid. This leads to an algorithm which uses maximal information for
+ its search for solutions in the monoid. It is both very efficient and
+ easily verifiable. Some applications of this algorithm are shown in
+ the appendix.",
+ paper = "Fort87.pdf"
+}
+
@inproceedings{Cavi76,
author = "Caviness, Bob F. and Fateman, Richard J.",
title = "Simplification of Radical Expressions",
@@ -16027,7 +16094,8 @@ paper = "Brea89.pdf"
computations can be done to variable (presumably high) precision. We
introduce notations p-representable and p-negligible where p denotes
precision, and show how this helps in our applications.",
- paper = "Fate03.pdf"
+ paper = "Fate03.pdf",
+ keywords = "CAS-Proof"
}
@misc{Fate15,
@@ -19711,6 +19779,21 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Dave90a,
+ author = "Davenport, James H.",
+ title = "Current Problems in Computer Algebra Systems Design",
+ journal = "LNCS",
+ volume = "429",
+ year = "1990",
+ pages = "1-9",
+ abstract =
+ "Computer Algebra systems have been with us for over twenty years, but
+ there is still no consensus on what an ``ideal'' system would look
+ like. There are all sorts of tradeoffs between portability,
+ functionality, and efficiency. This paper discusses some of those issues.",
+ keywords = "axiomref"
+}
+
@techreport{Dave92e,
author = "Davenport, James H.",
title = "The AXIOM System",
@@ -19784,6 +19867,7 @@ paper = "Brea89.pdf"
(e.g. PLUS could be declared for Integer arguments, or Rational, or
Real, or even Polynomial arguments) and the system will apply the
correct function for the types of the arguments.",
+ paper = "Dave81a.pdf",
keywords = "axiomref"
}
@@ -19920,7 +20004,7 @@ paper = "Brea89.pdf"
mathematical equality and with data structure equality, and to
explain how necessary it is to keep a clear distintion between the two.",
paper = "Dave02.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Dave07,
@@ -20029,7 +20113,7 @@ paper = "Brea89.pdf"
conventional, non-constructive, theory. It is also somewhat different
from the theories of Seidenberg [1974] and his school, who are not
particularly concerned with practical questions of efficiency.",
- paper = "Dave90.pdf",
+ paper = "Dave90c.pdf",
keywords = "axiomref",
beebe = "Davenport:1992:SVAa"
}
@@ -21108,7 +21192,7 @@ paper = "Brea89.pdf"
are inspired by the IMPS Interactive Mathematical Proof System and the
Axiom computer algebra system.",
paper = "Farm03.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@inproceedings{Fate79,
@@ -21669,6 +21753,17 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Gall90,
+ author = "Galligo, A. and Grimm, J. and Pottier, L.",
+ title = "The Design of SISYPHE: A System for doing Symbolic and
+ Algebraic Computations",
+ journal = "LNCS",
+ volume = "429",
+ pages = "30-39",
+ year = "1990",
+ keywords = "axiomref"
+}
+
@techreport{Gall92,
author = "Gallopoulos, Stratis and Houstis, Elias and Rice, John",
title = "Future Research Directions in Problem Solving Environments for
@@ -22446,7 +22541,7 @@ paper = "Brea89.pdf"
of computer algebra results proved formally in the HOL theorem prover
with the aid of Maple.",
paper = "Harr98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@misc{Harr12,
@@ -23300,6 +23395,7 @@ paper = "Brea89.pdf"
properties appears novel among programming languages (cf. image
functor of RUSSELL) and leads to a very powerful notion of abstract
algorithms missing from other work on data types known to the authors.",
+ paper = "Jenk81.pdf",
keywords = "axiomref"
}
@@ -23896,7 +23992,7 @@ paper = "Brea89.pdf"
and (iii) interface specifications which assist the verification of
pre- and post conditions of implemented code.",
paper = "Kels00a.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@article{Kend01,
@@ -23921,7 +24017,7 @@ paper = "Brea89.pdf"
on stochastic differentials, of the Mardia-Dryden distribution from
statistical shape theory.",
paper = "Kend01.pdf",
- keywords = "axiomref",
+ keywords = "axiomref, CAS-Proof",
beebe = "Kendall:2001:SIC"
}
@@ -23987,7 +24083,7 @@ paper = "Brea89.pdf"
calculus-level proof. We present an implementation of our ideas and
exemplify them using an automatically solved example.",
paper = "Kerb98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@article{Kocb96,
@@ -24148,6 +24244,16 @@ paper = "Brea89.pdf"
beebe = "Koseleff:1991:WGF"
}
+@article{Kred90,
+ author = "Kredel, Heinz",
+ title = "MAS Modula-2 Algebra System",
+ journal = "LNCS",
+ volume = "429",
+ pages = "270-271",
+ year = "1990",
+ keywords = "axiomref"
+}
+
@article{Kred08,
author = "Kredel, Heinz",
title = "On a Java computer algebra system,
@@ -26383,7 +26489,7 @@ paper = "Brea89.pdf"
concepts. The full calculus has been implemented and tested with our
LA compiler which generates executable files.",
paper = "Sant96.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
@book{Sant05,
@@ -28548,6 +28654,14 @@ paper = "Brea89.pdf"
paper = "Abra06.pdf"
}
+@book{ADAx83,
+ author = "U.S. Government",
+ title = "The Programming Language Ada Reference Manual",
+ publisher = "U.S. Government",
+ year = "1983",
+ comment = "STD-1815A-1983"
+}
+
@book{Altm05,
author = "Altmann, Simon L.",
title = "Rotations, Quaternions, and Double Groups",
@@ -28556,6 +28670,36 @@ paper = "Brea89.pdf"
isbn = "0-486-44518-6"
}
+@article{Aste02,
+ author = "Astesiano, Egidio and Bidoit, Michel and Kirchner, Helene and
+ Krieg-Bruckner, Bernd and Mosses, Peter D. and Sannella, Donald
+ and Tarlecki, Andrzej",
+ title = "CASL: the Common Algebraic Specification Language",
+ journal = "Theoretical Computer Science",
+ volume = "286",
+ number = "2",
+ pages = "153-196",
+ year = "2002",
+ abstract =
+ "The Common Algebraic Specification Language (CASL) is an expressive
+ language for the formal specification of functional requirements and
+ modular design of software. It has been designed by COFI, the
+ international Common Framework Initiative for algebraic specification
+ and development. It is based on a critical selection of features that
+ have already been explored in various contexts, including subsorts,
+ partial functions, first-order logic, and structured and architectural
+ specifications. CASL should facilitate interoperability of many
+ existing algebraic prototyping and verification tools.
+
+ This paper gives an overview of the CASL design. The major issues that
+ had to be resolved in the design process are indicated, and all the
+ main concepts and constructs of CASL are briefly explained and
+ illustrated — the reader is referred to the CASL Language Summary for
+ further details. Some familiarity with the fundamental concepts of
+ algebraic specification would be advantageous.",
+ paper = "Aste02.pdf"
+}
+
@article{Aubr99,
author = "Aubry, Phillippe and Lazard, Daniel and {Moreno Maza}, Marc",
title = "On the Theories of Triangular Sets",
@@ -28639,13 +28783,32 @@ paper = "Brea89.pdf"
paper = "Aubr99b.pdf"
}
+@article{Ausi79,
+ author = "Ausiello, Giovanni Francesco Mascari",
+ title = "On the Design of Algebraic Data Structures with the
+ Approach of Abstract Data Types",
+ journal = "LNCS",
+ volume = "72",
+ year = "1979",
+ pages = "514-530",
+ abstract =
+ "The problem of giving a formal definition of the representation of
+ algebraic data structures is considered and developped in the frame
+ work of the abstract data types approach. Such concepts as canonical
+ form and simplification are formalized and related to properties of
+ the abstract specification and of the associated term rewriting
+ system.",
+ paper = "Ausi79.pdf"
+}
+
@misc{Avig12,
author = "Avigad, Jeremy",
title = "Interactive Theorem Proving, Automated Reasoning, and
Mathematical Computation",
year = "2012",
comment = "slides",
- paper = "Avig12.pdf"
+ paper = "Avig12.pdf",
+ keywords ="CAS-Proof"
}
@misc{Avig14a,
@@ -28715,6 +28878,31 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Baue98,
+ author = "Bauer, Andrej and Clarke, Edmund and Zhao, Xudong",
+ title = "Analytica -- An Experiment in Combining Theorem Proving and
+ Symbolic Computation",
+ journal = "Journal of Automated Reasoning",
+ volume = "21",
+ number = "3",
+ pages = "295-325",
+ year = "1998",
+ abstract =
+ "Analytica is an automatic theorem prover for theorems in elementary
+ analysis. The prover is written in the Mathematica language and runs
+ in the Mathematica environment. The goal of the project is to use a
+ powerful symbolic computation system to prove theorems that are beyond
+ the scope of previous automatic theorem provers. The theorem prover is
+ also able to deduce the correctness of certain simplification steps
+ that would otherwise not be performed. We describe the structure of
+ Analytica and explain the main techniques that it uses to construct
+ proofs. Analytica has been able to prove several nontrivial
+ theorems. In this paper, we show how it can prove a series of lemmas
+ that lead to the Bernstein approximation theorem.",
+ paper = "Baue98.pdf",
+ keywords = "CAS-Proof"
+}
+
@book{Beez15,
author = "Judson, Tom and Beezer, Rob",
title = "Abstract Algebra: Theory and Applications",
@@ -28731,6 +28919,38 @@ paper = "Brea89.pdf"
year = "1991"
}
+@article{Bert98,
+ author = "Bertoli, P. and Calmet, J. and Guinchiglia, F. and Homann, K.",
+ title = "Specification and Integration of Theorem Provers and Computer
+ Algebra Systems",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1476",
+ year = "1998",
+ pages = "94-106",
+ abstract =
+ "Computer algebra systems (CASs) and automated theorem provers (ATPs)
+ exhibit complementary abilities. CASs focus on efficiently solving
+ domain-specific problems. ATPs are designed to allow for the
+ formalization and solution of wide classes of problems within some
+ logical framework. Integrating CASs and ATPs allows for the solution
+ of problems of a higher complexity than those confronted by each class
+ alone. However, most experiments conducted so far followed an ad-hoc
+ approach, resulting in tailored solutions to specific problems. A
+ structured and principled approach is necessary to allow for the sound
+ integration of systems in a modular way. The Open Mechanized Reasoning
+ Systems (OMRS) framework was introduced for the specification and
+ implementation of mechanized reasoning systems, e.g. ATPs. The
+ approach was recasted to the domain of computer algebra systems. In
+ this paper, we introduce a generalization of OMRS, named OMSCS (Open
+ Mechanized Symbolic Computation Systems). We show how OMSCS can be
+ used to soundly express CASs, ATPs, and their integration, by
+ formalizing a combination between the Isabelle prover and the Maple
+ algebra system. We show how the integrated system solves a problem
+ which could not be tackled by each single system alone.",
+ paper = "Bert98.pdf",
+ keywords = "CAS-Proof"
+}
+
@article{Bert95,
author = "Bertrand, Laurent",
title = "Computing a hyperelliptic integral using arithmetic in the
@@ -28887,10 +29107,86 @@ paper = "Brea89.pdf"
series = "ISSAC'98",
year = "1998",
address = "INRIA Sophia Antipolis",
- link = "\url{http://www-sop.inria.fr/cafe/Manuel.Bronstein/publications/issac98.pdf}",
+ link =
+"\url{http://www-sop.inria.fr/cafe/Manuel.Bronstein/publications/issac98.pdf}",
paper = "Bro98b.pdf"
}
+@article{Brui94,
+ author = "de Bruijn, N.G.",
+ title = "A Survey on the project Automath",
+ journal = "Studies in Logic and the Foundations of Mathematics",
+ volume = "133",
+ year = "1994",
+ pages = "141-161",
+ abstract =
+ "Thus far, much about Automath has been written in separate
+ reports. Most of this work has been made available upon request, but
+ only a small part was published in journals, conference proceedings,
+ etc. Unfortunately, a general survey in the form of a book is still
+ lacking. A short survey was given in [de Bruijn 73c], but the present
+ one will be much more extensive. Naturally, this survey will report
+ about work that has been done, is going on, or is planned for the
+ future. But it will also be used to explain how various parts of the
+ project are related. Moreover we shall try to clarify a few points
+ which many outsiders consider as uncommon or even wierd. In particular
+ we spend quite some attention to our concept of types and the matter
+ of ``propositions as types'' (Section 14). Finally the survey will be
+ used to ventilate opinions and views in mathematics which are not
+ easily set down in more technical reports.",
+ paper = "Brui94.pdf"
+}
+
+@inproceedings{Buch77,
+ author = "Buchberger, B. and Jebelean, Tudor and Kriftner, Franz and
+ Vasaru, Daniela",
+ title = "A Survey on the Theorema Project",
+ booktitle = "ISSAC '97",
+ year = "1997",
+ abstract =
+ "The Theorema project aims at extending current computer algebra
+ systems by facilities for supporting mathematical proving. The present
+ early-prototype version of the Theorema software system is implemented
+ in Mathematica 3.0. The system consists of a general higher-order
+ predicate logic prover and a collection of special provers that call
+ each other depending on the particular proof situations. The
+ individual provers imitate the proof style of human mathematicians and
+ aim at producing human-readable proofs in natural language presented
+ in nested cells that facilitate studying the computer-generated proofs
+ at various levels of detail. The special provers are intimately
+ connected with the functors that build up the various mathematical
+ domains.",
+ paper = "Buch77.pdf",
+ keywords = "CAS-Proof"
+}
+
+@book{Buch96,
+ author = "Buchberger, B.",
+ title = "Symbolic Computation: Computer Algebra and Logic",
+ booktitle = "Frontiers of Combining Systems",
+ publisher = "Kluwer Academic",
+ year = "1996",
+ pages = "192-220",
+ abstract =
+ "In this paper we present our personal view of what should be the next
+ step in the development of symbolic computation systems. The main
+ point is that future systems should integrate the power of algebra and
+ logic. We identify four gaps between the future ideal and the systems
+ available at present: the logic, the syntax, the mathematics, and the
+ prover gap, respectively. We discuss higher order logic without
+ extensionality and with set theory as a subtheory as a logic frame for
+ future systems and we propose to start from existing computer algebra
+ systems and proceed by adding new facilities for closing the syntax,
+ mathematics, and the prover gaps. Mathematica seems to be a
+ particularly suitable candidate for such an approach. As the main
+ technique for structuring mathematical knowledge, mathematical methods
+ (including algorithms), and also mathematical proofs, we underline the
+ practical importance of functors and show how they can be naturally
+ embedded into Mathematica.",
+ paper = "Buch96.pdf",
+ keywords = "CAS-Proof"
+}
+
@article{Burg74,
author = "William H. Burge",
title = "Stream Processing Functions",
@@ -28917,6 +29213,15 @@ paper = "Brea89.pdf"
separate parts, which can then be considered independently."
}
+@inproceedings{Burs77,
+ author = "Burstall, R.M. and Goguen, J.A.",
+ title = "Putting THeories together to make Specifications",
+ booktitle = "IJCAI 77 Volume 2",
+ pages = "1045-1058",
+ year = "1977",
+ paper = "Burs77.pdf"
+}
+
@inproceedings{Butl96,
author = "Butler, Greg",
title = "Software Architectures for Computer Algebra: A Case Study",
@@ -28941,6 +29246,36 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@book{Calm96,
+ author = "Calmet, Jacques and Homann, Karsten",
+ title = "Classification of Communication and Cooperation Mechanisms for
+ Logical and Symbolic Computation Systems",
+ booktitle = "Frontiers of Combining Systems",
+ publisher = "Kluwer Academic",
+ year = "1996",
+ pages = "221-234",
+ abstract =
+ "The combination of logical and symbolic computation systems has
+ recently emerged from prototype extensions of stand-alone systems to
+ the study of environments allowing interaction among several
+ systems. Communication and cooperation mechanisms of systems
+ performing any kind of mathematical service enable one to study and
+ solve new classes of problems and to perform efficient computation by
+ distributed specialized packages. The classification of communication
+ and cooperation methods for logical and symbolic computation systems
+ given in this paper provides and surveys different methodologies for
+ combining mathematical services and their characteristics,
+ capabilities, requirements, and differences. The methods are
+ illustrated by recent well-known examples. We separate the
+ classification into communication and cooperation methods. The former
+ includes all aspects of the physical connection, the flow of
+ mathematical information, the communication language(s) and its
+ encoding, encryption, and knowledge sharing. The latter concerns the
+ semantic aspects of architectures for cooperative problem solving.",
+ paper = "Calm96.pdf",
+ keywords = "CAS-Proof"
+}
+
@article{Cant87,
author = "Cantor, D.",
title = "Computing in the Jacobian of a HyperellipticCurve",
@@ -28960,8 +29295,36 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@techreport{Clar94,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Combining Symbolic Computation and Theorem Proving: Some
+ Problems of Ramanujan",
+ year = "1994",
+ type = "technical report",
+ institution = "Carnegie Mellon University",
+ number = "CMU-CS-94-103",
+ abstract =
+ "One way of building more powerful theorem provers is to use
+ techniques from symbolic computation. The challenge problems in this
+ paper are taken from Chapter 2 of Ramanujan''s Notebooks. They were
+ selected because they are non-trivial and require the use of symbolic
+ computation techniques. We have developed a theorem prover based on
+ the symbolic computation system Mathematica, that can prove all the
+ challenge problems completely automatically. The axioms and inference
+ rules for constructing the proofs are also briefly discussed.",
+ paper = "Clar94.pdf",
+ keywords = "CAS-Proof"
+}
+
+@book{Cohn65,
+ author = "Cohn, Paul Moritz",
+ title = "Universal Algebra",
+ publisher = "Harper and Row",
+ year = "1965"
+}
+
@book{Cohn91,
- author = "Chon, P.M.",
+ author = "Cohn, Paul Moritz",
title = "Algebra (2nd Ed.)",
publisher = "Wiley",
isbn = "978-0471101697",
@@ -28988,6 +29351,14 @@ paper = "Brea89.pdf"
paper = "Corl92.pdf"
}
+@misc{Dave80b,
+ author = "Davenport, J.H. and Jenks, R.D.",
+ title = "SCRATCHPAD/370: Modes and Domains",
+ year = "1980",
+ comment = "private communication",
+ keywords = "axiomref"
+}
+
@article{Dave81b,
author = "Davenport, James H.",
title = "Effective Mathematics: The Computer Algebra Viewpoint",
@@ -29010,6 +29381,36 @@ paper = "Brea89.pdf"
paper = "Dave81b.pdf"
}
+@techreport{Deme79,
+ author = "Demers, A. and Donahue, J.",
+ title = "Revised Report on RUSSELL",
+ year = "1979",
+ type = "technical report",
+ institution = "Cornell",
+ number = "TR 79-389"
+}
+
+@article{Dolz97b,
+ author = "Dolzmann, Andreas and Sturm, Thomas",
+ title = "REDLOG: Computer Algebra meets Computer Logic",
+ journal = "ACM SIGSAM Bulletin",
+ volume = "31",
+ number = "2",
+ year = "1997",
+ pages = "2-9",
+ abstract =
+ "REDLOG is a package that extends the computer algebra system REDUCE
+ to a computer logic system, i.e., a system that provides algorithms
+ for the symbolic manipulation of first-order formulas over some
+ temporarily fixed language and theory. In contrast to theorem provers,
+ the methods applied know about the underlying algebraic theory and
+ make use of it. We illustrate some applications of REDLOG, describe
+ its functionality as it appears to the user, and explain the design
+ issues and implementation techniques. REDLOG is available on the WWW.",
+ paper = "Dolz97b.pdf",
+ keywords = "CAS-Proof"
+}
+
@misc{blas01,
author = "Dongarra, Jack and et al.",
title = "Basic Linear Algebra Subprograms Technical (BLAST) Forum Standard",
@@ -29018,6 +29419,24 @@ paper = "Brea89.pdf"
paper = "blas01.pdf"
}
+@article{Dowe00,
+ author = "Dowek, Gilles",
+ title = "Axioms vs Rewrite Rules: From Completeness to Cut Elimination",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1794",
+ pages = "62-72",
+ year = "2000",
+ abstract =
+ "Combining a standard proof search method, such as resolution or
+ tableaux, and rewriting is a powerful way to cut off search space in
+ automated theorem proving, but proving the completeness of such
+ combined methods may be challenging. It may require in particular to
+ prove cut elimination for an extended notion of proof that combines
+ deductions and computations. This suggests new interactions between
+ automated theorem proving and proof theory.",
+ paper = "Dowe00.pdf"
+}
+
@misc{Duns01,
author = "Dunstan, M.N. and Gottliebsen, H. and Kelsey, T.W. and
Martin, U.",
@@ -29026,6 +29445,25 @@ paper = "Brea89.pdf"
year = "2001"
}
+@article{Dute96,
+ author = "Dutertre, Bruno",
+ title = "Elements of Mathematical Analysis in PVS",
+ journal = "LNCS",
+ volume = "1125",
+ pages = "141-156",
+ year = "1996",
+ abstract =
+ "This paper presents the formalization of some elements of
+ mathematical analysis using the PVS verification system. Our main
+ motivation was to extend the existing PVS libraries and provide means
+ of modelling and reasoning about hybrid systems. The paper focuses on
+ several important aspects of PVS including recent extensions of the
+ type system and discusses their merits and effectiveness. We conclude
+ by a brief comparison with similar developments using other theorem
+ provers.",
+ paper = "Dute96.pdf"
+}
+
@article{Duva96a,
author = {Duval, Dominique and Gonz\'alez-Vega, L.},
title = "Dynamic Evaluation and Real Closure",
@@ -29266,6 +29704,22 @@ paper = "Brea89.pdf"
year = "1991"
}
+@inproceedings{Gris76,
+ author = "Griss, Martin L.",
+ title = "The Definition and Use of Data Structures in REDUCE",
+ booktitle = "SYMSAC '76",
+ pages = "53-59",
+ year = "1976",
+ abstract =
+ "This paper gives a brief description and motivation of the mode
+ analyzing and data-structuring extensions to the algebraic language
+ REDUCE. These include generic functions, user defined recursive data
+ structures, mode transfer functions and user modifiable automatic
+ coercion. A number of examples are given to illustrate the style and
+ features of the language, and how it will aid in the construction of
+ more efficient and reliable programs."
+}
+
@article{Hach95,
author = "Hach\'e, G. and Le Brigand, D.",
title = "Effective construction of algebraic geometry codes",
@@ -29379,6 +29833,27 @@ paper = "Brea89.pdf"
paper = "Hebi10.pdf"
}
+@article{Homa94,
+ author = "Homann, Karsten and Calmet, Jacques",
+ title = "Combining Theorem Proving and Symbolic Mathematical Computing",
+ journal = "LNCS",
+ volume = "958",
+ pages = "18-29",
+ year = "1994",
+ abstract =
+ "An intelligent mathematical environment must enable symbolic
+ mathematical computation and sophisticated reasoning techniques on the
+ underlying mathematical laws. This paper disscusses different possible
+ levels of interaction between a symbolic calculator based on algebraic
+ algorithms and a theorem prover. A high level of interaction requires
+ a common knowledge representation of the mathematical knowledge of the
+ two systems. We describe a model for such a knowledge base mainly
+ consisting of type and algorithm schemata, algebraic algorithms and
+ theorems.",
+ paper = "Homa94.pdf",
+ keywords = "axiomref, CAS-Proof"
+}
+
@article{Homa05,
author = "Homann, Karsten and Calmet, Jacques",
title = "Structures for Symbolic Mathematical Reasoning and Computation",
@@ -29395,7 +29870,8 @@ paper = "Brea89.pdf"
reasoning and computation theories and structures provide a formal
framework for the specification of symbolic mathematical problem
solving by cooperation of algorithms and theorems.",
- paper = "Homa05.pdf"
+ paper = "Homa05.pdf",
+ keywords = "CAS-Proof"
}
@book{Hous81,
@@ -29690,7 +30166,8 @@ paper = "Brea89.pdf"
version = "2.2.2",
year = "2017",
link = "\url{}",
- paper = "Kono17.pdf"
+ paper = "Kono17.pdf",
+ keywords = "CAS-Proof"
}
@book{Lamp86,
@@ -29831,6 +30308,13 @@ paper = "Brea89.pdf"
paper = "Lehn10.pdf"
}
+@misc{Leve80,
+ author = "Levenworth, B.",
+ title = "ADAPT Reference Manual",
+ comment = "IBM Research",
+ year = "1980"
+}
+
@article{Lint02,
author = "Linton, S. and Sebastiani, R.",
title = "Editorial: The Integration of Automated Reasoning and Computer
@@ -29839,7 +30323,8 @@ paper = "Brea89.pdf"
volume = "34",
pages = "239-239",
year = "2002",
- paper = "Lint02.pdf"
+ paper = "Lint02.pdf",
+ keywords = "CAS-Proof"
}
@article{Lisk77,
@@ -30103,6 +30588,28 @@ paper = "Brea89.pdf"
year = "1998"
}
+@article{Melh02,
+ author = "Melham, Thomas F.",
+ title = "PROSPER An Investigation into Software Architecture for Embedded
+ Proof Engines",
+ journal = "LNCS",
+ volume = "2309",
+ pages = "193-206",
+ year = "2002",
+ abstract =
+ "Prosper is a recently-completed ESPRIT Framework IV research project
+ that investigated software architectures for component-based, embedded
+ formal verification tools. The aim of the project was to make
+ mechanized formal analysis more accessible in practice by providing a
+ framework for integrating formal proof tools inside other software
+ applications. This paper is an extended abstract of an invited
+ presentation on Prosper given at FroCoS 2002. It describes the vision
+ of the Prosper project and provides a summary of the technical
+ approach taken and some of the lessons learned.",
+ paper = "Melh02.pdf",
+ keywords = "CAS-Proof"
+}
+
@article{Mill68,
author = "Millen, J. K.",
title = "CHARYBDIS: A LISP program to display mathematical expressions
@@ -30504,6 +31011,31 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Sorg00,
+ author = "Sorge, Volker",
+ title = "Non-trivial Symbolic Computations in Proof Planning",
+ journal = "LNCS",
+ volume = "1794",
+ pages = "121-135",
+ year = "2000",
+ abstract =
+ "We discuss a pragmatic approach to integrate computer algebra into
+ proof planning. It is based on the idea to separate computation and
+ verification and can thereby exploit the fact that many elaborate
+ symbolic computations are trivially checked. In proof planning the
+ separation is realized by using a powerful computer algebra system
+ during the planning process to do non-trivial symbolic
+ computations. Results of these computations are checked during the
+ refinement of a proof plan to a calculus level proof using a small,
+ self-implemented system that gives us protocol information on its
+ calculation. This protocol can be easily expanded into a checkable
+ low-level calculus proof ensuring the correctness of the
+ computation. We demonstrate our approach with the concrete
+ implementation in the $\Omega$MEGA system.",
+ paper = "Sorg00.pdf",
+ keywords = "CAS-Proof"
+}
+
@book{Stee90,
author = "Steele, Guy L.",
title = "Common Lisp, The Language",
@@ -30541,6 +31073,31 @@ paper = "Brea89.pdf"
year = "1890"
}
+@article{That82,
+ author = "Thatcher, J.W. and Wagner, E.G. and Wright, J.B.",
+ title = "Data Type Specification: Parameterization and the Power of
+ Specification Techniques",
+ journal = "ACM TOPLAS",
+ volume = "4",
+ number = "4",
+ pages = "711-732",
+ year = "1982",
+ abstract =
+ "Our earlier work on abstract data types is extended by the answers to
+ a number of questions on the power and limitations of algebraic
+ specification techniques and by an algebraic treatment of
+ parameterized data types like {\bf sets-of()} and
+ {\bf stacks-of-()}. The ``hidden function'' problem (the need to include
+ operations in specifications which are wanted hidden from the user) is
+ investigated; the relative power of conditional specifications and
+ equational specifications is investigated; the relative power of
+ conditional specifications and equational specifications is
+ investigated; and it is shown that parameterized specifications must
+ contain ``side conditions'' (e.g. that {\bf finite-sets-of-d} requires
+ an equality predicate on {\bf d}).",
+ paper = "That82.pdf"
+}
+
@article{Thur94,
author = "Thurston, William P.",
title = "On Proof and Progress in Mathematics",
@@ -30626,6 +31183,28 @@ paper = "Brea89.pdf"
year = "2003"
}
+@article{Wegb74,
+ author = "Wegbreit, Ben",
+ title = "The Treatment of Data Types in EL1",
+ journal = "Communications of the ACM",
+ volume = "17",
+ number = "5",
+ year = "1974",
+ pages = "251-264",
+ abstract =
+ "In constructing a general purpose programming language, a key issue
+ is providing a sufficient set of data types and associated operations
+ in a manner that permits both natural problem-oriented notation and
+ efficient implementation. The EL1 language contains a number of
+ features specifically designed to simultaneously satisfy both
+ requirements. The resulting treatment of data types includes provision
+ for programmer-defined data types and generaic routines, programmer
+ control over type conversion, and very flexible data type behavior, in
+ a context that allows efficient compiled code and compact data
+ representation.",
+ paper = "Wegb74.pdf"
+}
+
@misc{Weil71,
author = "Weil, Andr\'{e}",
title = "Courbes alg\'{e}briques et vari\'{e}t\'{e}s Abeliennes",
@@ -30665,6 +31244,38 @@ paper = "Brea89.pdf"
link = "\url{https://en.wikipedia.org/wiki/Levenshtein\_distance}"
}
+@article{Wulf76,
+ author = "Wulf, William A. and London, Ralph L. and Shaw, Mary",
+ title = "An Introduction to the Construction and Verification of
+ Alphard Programs",
+ journal = "IEEE Tr. Software Engineering",
+ volume = "SE-2",
+ number = "4",
+ year = "1976",
+ pages = "253-265",
+ abstract =
+ "The programming language Alphard is designed to provide support for
+ both the methodologies of ``well-structured'' programming and the
+ techniques of formal program verification. Language constructs allow
+ a programmer to isolate an abstraction, specifying its behavior
+ publicly while localizing. knowledge about its implementation. The
+ verification of such an abstraction consists of showing that its
+ implementation behaves in accordance with its public specifications;
+ the abstraction can then be used with confidence in constructing
+ other programs, and the verification of that use employs only the
+ public specifications. This paper introduces Alphard by developing
+ and verifying a data structure definition and a program that uses it.
+ It shows how each language construct contributes to the development of
+ the abstraction and discusses the way the language design and the
+ verification methodology wete tailored to each other. It serves not
+ only as an introduction to Alphard, but also as an example of the
+ symbiosis between verification and methodology in language design.
+ The strategy of program structuring, illustrated for Alphard, is
+ also applicable to most of the ``data abstraction'' mechanisms now
+ appearing.",
+ paper = "Wulf76.pdf"
+}
+
@misc{Zdan14,
author = "Zdancewic, Steve and Martin, Milo M.K.",
title = "Vellvm: Verifying the LLVM",
diff --git a/books/bookvol3.pamphlet b/books/bookvol3.pamphlet
index 64fa500..ec71648 100644
--- a/books/bookvol3.pamphlet
+++ b/books/bookvol3.pamphlet
@@ -3,6 +3,569 @@
\input{bookheader.tex}
\mainmatter
\setcounter{chapter}{0} % Chapter 1
+\chapter[A Language for Computational Algebra]
+{A Language for Computational Algebra by Jenks and Trager}
+
+\section{Introduction}
+
+Jenks and Trager\cite{Jenk81} describe a language with parameterized
+types and generic operators particularly suited to computational algebra.
+A flexible framework is given for building algebraic structures and
+defining algorithms which work in as general a setting as possible.
+This section will be an overview of our main concepts: ``domains''
+and ``categories''.
+
+A language for computational algebra should be able to express algorithms
+for dealing with algebraic objects at their most natural level of abstraction.
+We can illustrate this concept with two simple algorithms. First, we wish
+to write a function {\sl max} which computes the maximum of two elements
+of any set on which an ordering predicate is defined. One approach to this
+problem is to explicitly pass the ordering predicate as an additional
+argument to max. Thus max might be defined by
+\begin{verbatim}
+ max(x,y,lessThan) == if lessThan(x,y) then y else x
+\end{verbatim}
+where lessThan is the ordering predicate. In more complicated algorithms,
+the number of additional arguments required gets out of hand. Our approach
+is instead to require the arguments $x$ and $y$ of max to be elements
+of some specific algebraic structure which has a ``less than'' operation
+'$<$' implemented by some function. We will call such algebraic structures
+{\bf domains}. Thus '$<$' is a ``generic'' operation which has different
+function definitions for different domains. Our definition of max, with
+suitable declarations, becomes:
+\begin{verbatim}
+ max(x,y) == if x < y then y else x
+\end{verbatim}
+
+The requirement that a generic operation have a particular name does not
+characterize its algebraic properties. In the above definition of max,
+it is implicitly assumed that '$<$' provides a total ordering on the
+elements of its domain. To this end, our domains will also have a set of
+{\sl attributes} which permit a description of the algebraic properties
+of its operations (e.g. so as to distinguish between totally-ordered and
+partially-ordered sets).
+
+As a second example, we examine the classical algorithm for computing the
+{\sl gcd}, the greatest common divisor, of two integers:
+\begin{verbatim}
+ gcd(x,y) == if x = 0 then y else gcd(y,remainder(x,y))
+\end{verbatim}
+
+Although this algorithm was originally intended to be used only on integers,
+a cursory examination shows that only a few properties of the integers are
+actually required. In fact, the same algorithm can be used on gaussian
+integers, polynomials over fields, or any other domain which has an
+appropriate remainder function. We wish to specify the minimum requirements
+of an algebraic structure for the gcd algorithm to be applicable. To do this,
+we introduce a grouping of domains called a {\bf category}, in this case,
+``the category of Euclidean domains''. Any domain of this category will be
+an integral domain with a generic function {\sl remainder} satisfying two
+requirements. The first is that
+\begin{verbatim}
+ remainder(x,y) = x - q*x*y
+\end{verbatim}
+for some $q$ in the domain as this implies
+\begin{verbatim}
+ gcd(x,y) - gcd(y,remainder(x,y))
+\end{verbatim}
+The remainder function must also have the property that the remainder
+sequence generated by any two elements of the domain always reaches 0 in a
+finite number of steps. These two requirements are sufficient to guarantee
+the correctness of our gcd algorithm.
+
+Categories provide a set of required generic operations together with a
+set of attributes describing the required algebraic properties of these
+operations. Domains provide specific functions which implement the
+operations and satisfy the attributes. Thus we may speak of ``the category
+of totally-ordered sets'' as the class of all domains which have the above
+'$<$' operation with specific algebraic properties, and ``the domain of
+the integers'' as an example of a member of that category since it has a
+function 'integer$<$' which provides that operation and satisfies those
+properties.
+
+Once an abstract algorithm has been written, its author specifies the
+category of domains to which it applies, either by explicitly listing
+the operations and attributes it requires or by referencing a predefined
+category. For example, having defined the category EuclideanDomain
+(``the category of Euclidean domains''), a complete definition of the gcd
+function could be written:
+\begin{verbatim}
+ gcd(x:R,y:R):R where R:EuclideanDomain ==
+ if x=0 then y else gcd(y,remainder(x,y))
+\end{verbatim}
+
+Expressions of the form ``A:B'' are called {\sl declarations}. The
+arguments $x$ and $y$ of gcd are {\sl declared} to be elements of some
+domain R which, in turn, is declared to be a member of EuclideanDomain.
+Declaring ``A:B'' means ``A is a member of B'' in the following sense.
+Declaring a domain to be a member of a category indicates that all the
+operations of the category are implemented in that domain as functions
+which satisfy the attributes of the category. Similarly declaring an
+object to be a member of a domain means that all the functions provided
+in that domain are applicable to the object.
+
+Domains and categories are both computed objects that can be assigned to
+a variable, passed as arguments, and returned from functions. A category
+may be produced by explicitly listing operations and attributes, or by
+invoking a function which returns a category. Categories may be augmented,
+diminished, or ``joined'' with other categories to produce a new category
+containing all of the operations and attributes of the individual categories.
+
+A domain is always created by a function which we call a {\bf functor}.
+Some simple domains are ``the integers'' and ``the booleans'' which are
+produced by functors of no arguments. Other domains such as ``the integers
+mod 7'' are produced by functors which take arguments (such as the modulus
+7). Most algebraic domains are built up from other domains which, along
+with other parameters, are passed as arguments to the functors that construct
+them. For example, the domain ``polynomials in X over the integers'' is
+created by a polynomial functor which takes a variable (e.g. ``X'') and an
+underlying domain (e.g. ``the integers'') as arguments. With the few
+exceptions noted in the next section,
+functors and categories are definable in the
+language and may be freely modified. A user is free to introduce new
+categories and define new functors in order to make more domains available
+for computation.
+
+Max and gcd were both defined in terms of generic operations from domains
+implicitly passed as arguments. As required by some algebraic algorithms,
+domains are dynamically created and assigned to local variables. Objects
+of these newly created local domains can be created, manipulated, and
+converted to objects of other domains.
+
+\begin{center}
+Figure 1: Algebraic Categories\\
+\begin{tabular}{|l|l|l|}
+\hline
+{\bf category} & {\bf extends} & {\bf operations}\\
+\hline
+Set & & $=$\\
+AbelianGroup & Set & $0,+,-$\\
+OrderedSet & Set & $<$\\
+QuotientObject(S:Set) & Set & reduce,lift\\
+SemiGroup & Set & $\times$\\
+Finite & Set & size,random\\
+Monoid & SemiGroup & 1\\
+Group & Monoid & inv\\
+Ring & (Monoid,AG) & characteristic, recip\\
+Module(R:Ring) & AbelianGroup & scalar$\times$\\
+Algebra(R:Ring) & (Ring,Module(R)) &\\
+DifferentialRing & Ring & deriv\\
+IntegralDomain & Ring & isAssociate./ /\\
+SkewField & Ring & /\\
+UniqueFactorizationDomain & IntegralDomain & gcd, factor, isPrime\\
+EuclideanDomain & UFD & size<, quo, rem\\
+Field & (ED, SkewField) &\\
+GaloisField & (Field, Finite) &\\
+VectorSpace(S:Field) & Module(S) &\\
+\hline
+\end{tabular}
+\end{center}
+
+Both categories and domains may be organized into hierarchies. Figure 1
+shows an algebraic hierarchy of categories, listing the operations (but
+not the attributes) introduced by the successive categories. Set is a
+category with a single operation '$=$'. SemiGroup extends Set by adding
+an operation '$\times$' etc. More complicated cases will be discussed
+in the next section. We will also allow one domain to extend another.
+
+For example, one can write a ``free-module functor'' to provide the
+module-theoretic aspects of a polynomial ring (additon and multiplication
+by scalars). One can then write various polynomial, algebraic-extension,
+and sparse-matrix functors as extensions of the free-module functor. The
+polynomial functor, for example, would augment the functions provided
+by the free-module functor, adding explicit definitions only for the other
+polynomal functions such as multiplication. Similarly, a ``localization
+functor'' can be written to provide computations where denominators may be
+from a different domain than that of the numerator, such as ``the odd
+integers'', ``powers of 2'', ``products of factored polynomials in X''.
+The localization functor is thus a function of two arguments, one for
+the numerator domain, the other for the denominator domain. A ``quotient
+field functor'' can then be written which extends the localization functor
+for the special case when the two argument domains are the same integral
+domain. From the quotient field functor, one can produce all of the rational
+function domains and ``the rational numbers'' as special cases.
+
+To summarize, our language design provides the useful notions of ``domains''
+and ``categories'' for the abstract description of algorithms for
+computational algebra. The facility for categories is unique to our
+language and its use seems to be invaluable for describing algorithms
+for computational algebra. Our domains are similar to ``modes'' in
+EL1\cite{Wegb74} and ``types'' in RUSSELL\cite{Deme79} and ADAPT\cite{Leve80}.
+As in EL1, but in contrast to Ada\cite{ADAx83}, domains are computed values.
+Our notions of categories and functors are based on concepts in universal
+algebra \cite{Cohn65} developed by the ADJ group \cite{That82} and Burstall
+and Goguen \cite{Burs77}. In addition, categories extend the idea of
+``type constraint'' in CLU \cite{Lisk79} and Alphard \cite{Wulf76} where
+functions can require that their arguments have certain operations available
+to them. For related work in computer algebra, see \cite{Ausi79},
+\cite{Gris76}, \cite{Jenk74}, and \cite{Loos74}.
+
+\section{Concepts}
+
+In this section, we give precise definitions and examples of the concepts
+of domain, category, and functor.
+
+{\bf Domain}. By a {\sl domain of computation}, or, simply, {\bf domain},
+we mean:
+\begin{enumerate}
+\item a set of generic {\bf operations}
+\item a {\bf representation}
+\item a set of {\bf functions} which implement the operations in terms
+of the representation
+\item a set of {\bf attributes}, which designate useful facts such as
+axioms and mathematical theorems which are true for the operations as
+implemented by the functions.
+\end{enumerate}
+
+The simplest examples of domains are those corresponding to the basic
+data-types offered by the underlying system, such as Integer (``the
+integers''), Boolean (``the booleans''), etc. Other examples of domains
+are RationalNumber (``the rational numbers''), Matrix(Integer)
+(``rectangular matrices with integer coefficients''), and
+Polynomial(X,RationalNumber) (``the polynomials in X with rational
+number coefficients'').
+
+The generic operations are given by {\bf signatures}, expressions consisting
+of an {\sl operation name}, a {\sl source}, and a {\sl target}. The domain
+Integer, for example, has the operation ``less than'' expressed by the
+signture:
+\[`<`: ({\rm Integer},{\rm Integer}) \rightarrow {\rm Boolean}\]
+with '$<$' as operation name, (Integer,Integer) as source, and Boolean
+as target. The source part of the signature is any sequence of domains,
+and the target part is any domain.
+
+The representation for a domain describes a data structure used to
+represent the objects of the domain.
+
+The functions component is a set of compiled functions providing a
+domain-specific implementation for each generic operation. For example,
+domain Integer has a function ``Integer$<$'' which implements ``less than''.
+If a domain has an operation signature
+\[{\rm op:}(D_1,\ldots,Dn) \rightarrow D_0\]
+then the associated function must take arguments from the representations
+of $D_1,\ldots,D_n$ respectively and return a result in the representation
+of $D_0$.
+
+The attribute component of a domain is described either by a name, e.g.
+``finite'', or by a form with operator names as parameters, e.g.
+``distributive('$\times$','$+$')''. The purpose of attributes is not to
+provide complete axiomatic descriptions of an operation, rather to assert
+facts which programs can query.
+
+{\bf Category} A ``category'' designates a class of domains with common
+operations and attributes but with different functions and representations.
+The categories of interest here will be those of algebraic structures such
+as Ring (``the class of all rings''), Field (``the class of all fields''),
+and Set (``the class of all sets'').
+
+By a {\bf category} we mean:
+\begin{enumerate}
+\item a set of generic {\bf operations}
+\item a set of {\bf attributes}, which designate facts which must be
+true for any implementation of the operations.
+\end{enumerate}
+
+As with domains, the generic operations of categories are given by
+signatures, consisting of an operation name, a source, and a target.
+In addition to the domains which may appear in the source and target, a
+special symbol \$ (or, later \%) is used to designate an arbitrary member
+domain of the category. The set of operations and attributes are those
+which member domains have in common. A simple example of a category is Set,
+a category which has one operation
+\[=: (\$,\$) \rightarrow Boolean\]
+and no attributes. Another is SemiGroup, which besides the '$=$'
+operation, has the operation
+\[\times: (\$,\$) \rightarrow \$\]
+and the attribute associative('$\times$').
+
+We say a domain D is ``a member of'' a category C, equivalently, D is of C,
+if D contains every operation and attribute of C with \$ replaced by D.
+For example, Integer is of Set because it contains an operation
+\[=: ({\rm Integer},{\rm Integer}) \rightarrow {\rm Boolean}\]
+We say that a category B extends a category A if all of the operations and
+attributes of A are contained in B. SemiGroup extends Set since all of the
+operations ('$=$') of Set are contained in SemiGroup.
+
+\begin{center}
+Figure 2. Examples of Category Definitions
+\end{center}
+
+\hrulefill
+
+Set: Category == {\bf category}\\
+\hbox{\hskip 0.5cm} [{\sl operations}] =:(\$,\$) $\rightarrow$ Boolean
+
+SemiGroup: Category == Set with\\
+\hbox{\hskip 0.5cm} [{\sl operations}] $\times$:(\$,\$) $\rightarrow$ \$\\
+\hbox{\hskip 0.5cm} [{\sl attributes}] {\rm associative}('$\times$')
+[($x \times y) \times z = x \times (y \times z)$]
+
+\hrulefill
+
+Figure 2 illustrate our language for defining categories. Set is defined
+by explicitly listing its operations ('$=$') and its attributes (none).
+SemiGroup is defined as an extension of Set. Square-bracketed expressions
+are comments. The '$==$' signifies a rewrite-rule definition for the
+category Set. Evaluation of ``Set'' causes ``Set'' to be rewritten by the
+category value indicated to the right of the '$==$'. Evaluation of
+``SemiGroup'' similary causes ``SemiGroup'' to be rewritten by the
+corresponding right-hand expression. Further evaluation causes Set to be
+replaced by its value, a category to which the '$\times$' operation and
+associative('$\times$') attribute are added by the {\bf with} operation.
+As implied by this evaluation mechanism, two categories are equivalent
+iff they have equivalent sets of operations and attributes, irrespecitive
+of how they were created.
+
+\begin{center}
+Figure 3. Examples of Category Definitions
+\end{center}
+
+\hrulefill
+
+Module(R:Ring) : Category == AbelianGroup with\\
+\hbox{\hskip 0.5cm} [{\sl operations}] $\times$:(R,\$) $\rightarrow$ \$\\
+\hbox{\hskip 0.5cm} [{\sl attributes}] $\ldots$
+
+Algebra(R:Ring) : Category == (Ring,Module(R)) with\\
+\hbox{\hskip 0.5cm} [{\sl attributes}] $\ldots$
+
+\hrulefill
+
+Figure 3 gives two examples of parameterized categories, that is, categories
+that are produced by functions of one or more arguments. The function
+Module creates the category of all R-modules, that is, modules over a given
+ring R. For example, the function Module applied to Integer produces the
+category of all $Z$-modules, domains D which are abelian groups with
+the additional operations
+\[\times: ({\rm Integer,D}) \rightarrow {\rm Integer}\].
+
+This category includes domain Integer since Integer is an abelian group
+and has the operation
+\[\times: ({\rm Integer,Integer}) \rightarrow {\rm Integer}\].
+
+The function Algebra(R) extends the {\sl join} of a Ring and a Module(R),
+written (Ring,Module(R)). The join designates the category formed by
+directly combining the operations and attributes of Ring with those of
+Module(R).
+
+Another way of parameterizing categories is by operator names. For example,
+the above definition of SemiGroup could be extended to take a binary operation
+as a parameter:\\
+\hbox{\hskip 0.5cm}SemiGroup(op) : Category == Set with\\
+\hbox{\hskip 1.0cm}[{\sl operations}] op: (\$,\$) $\rightarrow$ \$\\
+\hbox{\hskip 1.0cm}[{\sl attributes}] associative(op)
+[$op(op(x,y),z) = op(x,op(y,z))$]
+
+after which we may refer to the multiplicative form of SemiGroup in
+Figure 2 by SemiGroup('$\times$').
+
+{\bf Functor} By a {\bf functor} we mean any function which returns a
+domain. A functor creates a domain, a member of some category. A category
+never creates anything: it simply acts as a template for domains,
+describing which operations and attributes must be present. A functor
+creates a domain by storing functions into a template given by its
+target category. Categories never specify representations for objects;
+functors always do.
+
+Domains can only be produced by functors. Basic domains (e.g. ``the
+integers'') are produced through functors bound to identifiers (e.g.
+Integer). In addition, four built-in functors, List Vector, Struct, and
+Union, build aggregate domains from other domains passed as arguments.
+The functor List can be applied to any domain (e.g. Integer) to produce
+a composite domain (e.g. List(Integer)) with a set of functions which
+provide operations on lists (e.g. first, rest, cons). The functor
+Vector takes two arguments, a positive integer $n$ and a domain $D$,
+and produces the domain ``the set of all vectors of length $n$ with
+elements from $D$''. Struct produces a domain represented by a set of
+name-value pairs, e.g. Struct(real:Integer,imag:Integer) describes
+an appropriate representation for ``the Gaussian integers''.
+Union(A,$\ldots$,B) creates a new domain $D$ form the domains $A,\ldots,B$
+which is the disjoint union of the domains $A,\ldots,B$.
+
+The language permits the building of new functors from these basic
+functors. A simple example is FiniteField in Figure 4.
+\begin{center}
+Figure 4. Example of Functor Definition
+\end{center}
+
+\hrulefill
+
+FiniteField(p:PrimeNumber) : GaloisField ==\\
+\hbox{\hskip 0.5cm} {\bf capsule}\\
+\hbox{\hskip 1.0cm} [{\sl representation}]\\
+\hbox{\hskip 1.5cm} Rep := Integer\\
+\hbox{\hskip 1.0cm} [{\sl declarations}]\\
+\hbox{\hskip 1.5cm} x,y : \$\\
+\hbox{\hskip 1.0cm} [{\sl definitions}]\\
+\hbox{\hskip 1.5cm} 0 == Integer.0\\
+\hbox{\hskip 1.5cm} 1 == Integer.1\\
+\hbox{\hskip 1.5cm} x+y == {\bf if} (w $\leftarrow$ x Integer.$+$ y) $>$ p\\
+\hbox{\hskip 3.0cm} {\bf then} w - p\\
+\hbox{\hskip 3.0cm} {\bf else} w\\
+\hbox{\hskip 1.5cm} $\cdots$
+
+\hrulefill
+
+The functor FiniteField applied to p, a prime number, creates a domain
+``the integers modulo p'', a member of its target category GaloisField
+(``the class of all Galois fields''). The set of operations and
+attributes of this domain are given by GaloisField, the representation
+and set of functions, by the {\sl capsule} part of the definition which
+appears to the right of the `$==$'. The representation is always defined
+by the distinguished symbol Rep in terms of a ``lower level'' functor.
+For FiniteFields, Rep is defined to be Integer (meaning that elements
+of a finite field are represented by integers). In a more complicated
+example, Rep might be defined in terms of a functor Matrix, whose Rep,
+in turn, might be defined in terms of the built-in functor Vector.
+\begin{center}
+Figure 5. Example of Functor Definition
+\end{center}
+
+\hrulefill
+
+IntegerMod(m:Integer | m $>$ 1): T == C {\bf where}\\
+\hbox{\hskip 0.5cm} T == (Ring,Finite) {\bf with}\\
+\hbox{\hskip 2.5cm} {\bf if} isPrime m {\bf then} GaloisField\\
+\hbox{\hskip 0.5cm} C == {\bf capsule}\\
+\hbox{\hskip 1.5cm} $\cdots$\\
+\hbox{\hskip 1.0cm} [{\sl definitions}]\\
+\hbox{\hskip 1.5cm} {\bf if} isPrime m {\bf then}\\
+\hbox{\hskip 2.0cm} x / y == $\ldots$\\
+\hbox{\hskip 1.5cm} $\cdots$
+
+\hrulefill
+
+Figure 5 illustrates the use of conditional expressions to make the target
+category of a functor depend upon the paramters of the functor. Here the
+FiniteField functor of Figure 4 is generalized to IntegerMod, a functor
+which produces the domain ``the integers modulo m'' for any positive
+integer (modulus) m. The domain produced by the IntegerMod functor will
+be a Galois field if m is prime, a finite ring, if it is not. Conditional
+expressions are also used in the capsule part of a functor to conditionally
+provide functions (e.g the operation '/' will be provided by IntegerMod
+only if m is prime), or to provide alternative versions of functions
+(e.g. more efficient implementations for some functions when the modulus
+is small).
+
+Figure 6 illustrates a series of functors for localization which illustrate
+how domains, like categories, can be extended. Localize takes an R-module
+M, and a denominator domain D which is a monoid contained within R. It
+produces an R-module of ``fractions''. LocalAlgebra augments this with a
+definition of multiplication for fractions producing the localization of
+an R-algebra. QuotientField uses LocalAlgebra to produce a ``field of
+fractions'' in the special situation where the numerators and
+denominators both come from the same integral domain. When R has a gcd
+function, QuotientField redefines the arithmetic operations (supplied by
+LocalAlgebra) to produce reduced fractions. Similarly, if R has a
+derivation defined for it, QuotientField extends this derivation to the
+field of fractions.
+
+{\bf Conclusions} Our language provides the useful notions of ``domains''
+and ``categories'' for the abstract description of algorithms for
+computational algebra. Domains are the algebraic structures on which
+computation is performed. Categories are groupings of domains with common
+operations and attributes.
+
+There are several advantages to our design. Algorithms can be written
+to operate over any group, ring, or field, independently of how that
+algebraic structure is defined or represented in the computer. The
+algorithm implementor need not know about which domains have actually
+been created. Rather they need only specify a category which gives the
+required operations and essential algebraic properties of the algorithm.
+Also, as required by many algebraic algorithms, domains and categories
+are dynamically computed objects.
+
+The language we have presented leads to a computer algebra system which is
+easily extended by any user. All categories are defined in the language
+and are available for user modification. All domains are created by
+functions which, with the exception of a few that are built-in, are also
+defined in the language and can be changed by the user. New domains and
+categories can be designed and implemented with minimal effort by extending
+or combining existing structures.
+
+The language permits considerable code economy. An algorithm is
+implemented by a single function which is applicable to any domain of a
+declared category. A matrix functor, for example, will use the same
+compiled function to compute the product of two matrices, regardless of
+whether the actual matrix coefficents are integers, polynomials, or
+other matrices. Parameterized functors help to minimize redundant code by
+providing a set of pre-compiled functions for all domains they can produce.
+The universal applicability of such functors as QuotientField provide
+powerful methods for constructing new algebraic objects.
+
+Our primary goal in presenting a language which deals with algebraic
+objects was to take advantage of as much of the structure implicit in the
+problem domain as possible. The natural algebraic notions of domains
+extending one another, and collecting domains with common properties
+into categories have been show to be useful computational devices. By
+preserving this natural structure, we hope to have eased the task of
+finding computational models for algebraic structures.
+
+\newpage
+\begin{center}
+Figure 6. Definition of Localization Functors
+\end{center}
+\vskip -0.2cm
+\hrulefill
+
+Localize(isZeroDivisor,M,D) : Module(R) == C {\bf where}\\
+\hbox{\hskip 0.5cm} R:Ring\\
+\hbox{\hskip 0.5cm} M: Module(R)\\
+\hbox{\hskip 0.5cm} D: Monoid $\vert$ D $\subseteq$ R\\
+\hbox{\hskip 0.5cm} isZeroDivisor: M $\rightarrow$ Boolean\\
+\hbox{\hskip 0.5cm} C == {\bf capsule} $\ldots$\\
+\hbox{\hskip 1.5cm} [{\sl representation}]\\
+\hbox{\hskip 2.0cm} Rep := Struct(num:M, den:D)\\
+\hbox{\hskip 1.5cm} [{\sl declarations}]\\
+\hbox{\hskip 2.0cm} x,y: \$\\
+\hbox{\hskip 2.0cm} n: Integer\\
+\hbox{\hskip 2.0cm} r:R ; d:D\\
+\hbox{\hskip 1.5cm} [{\sl definitions}]\\
+\hbox{\hskip 2.0cm} 0 == Rep(0,1)\\
+\hbox{\hskip 2.0cm} -x == Rep(-x.num,x.den)\\
+\hbox{\hskip 2.0cm} x=y == isZeroDivisor(y.den $\times$ x.num -
+x.den $\times$ y.num)\\
+\hbox{\hskip 2.0cm} x+y == Rep(y.den $\times$ x.num + x.den $\times$ y.num,
+x.den $\times$ y.den)\\
+\hbox{\hskip 2.0cm} n $\times$ x == Rep(n $\times$ x.num,x.den)\\
+\hbox{\hskip 2.0cm} r $\times$ x == {\bf if} r=x.den {\bf then}
+Rep(x.num,1) {\bf else} Rep(r $\times$ x.num,x.den)\\
+\hbox{\hskip 2.0cm} x / d == Rep(x.num,d $\times$ x.den)
+\vskip 0.2cm
+LocalAlgebra(isZeroDivisor,A,D): T == C {\bf where}\\
+\hbox{\hskip 0.5cm} R: Ring\\
+\hbox{\hskip 0.5cm} A: Algebra(R)\\
+\hbox{\hskip 0.5cm} isZeroDivisor: A $\rightarrow$ Boolean\\
+\hbox{\hskip 0.5cm} D: Monoid $\vert$ D $\subseteq$ R\\
+\hbox{\hskip 0.5cm} T == Algebra(R) {\bf with if} A {\bf has}
+commutative('$\times$') {\bf then} commutative('$\times$')\\
+\hbox{\hskip 0.5cm} C == Localize(isZeroDivisor,A,D) {\bf add} $\ldots$\\
+\hbox{\hskip 2.0cm} 1 == Rep(1,1)\\
+\hbox{\hskip 2.0cm} x $\times$ y == Rep(x.num $\times$ y.num,
+x.den $\times$ y.den)\\
+\hbox{\hskip 2.0cm} characteristic == A.characteristic
+\vskip 0.2cm
+QuotientField(R; IntegralDomain) : T == C {\bf where}\\
+\hbox{\hskip 0.5cm} T == (Field,Algebra(R)) {\bf with if}
+R of DifferentialRing {\bf then} DifferentialRing\\
+\hbox{\hskip 0.5cm} C == LocalAlgebra(\$1 = 0,R,R) {\bf add} $\ldots$\\
+\hbox{\hskip 2.0cm} {\bf if} R {\bf has} gcd: (R,R) $\rightarrow$ R
+{\bf then}\\
+\hbox{\hskip 2.5cm} x + y == $\ldots$\\
+\hbox{\hskip 2.5cm} x $\times$ y == $\ldots$\\
+\hbox{\hskip 2.5cm} {\bf where} cancelGcd(x:\$):\$ == $\ldots$\\
+\hbox{\hskip 2.0cm} {\bf if} R of DifferentialRing {\bf then}\\
+\hbox{\hskip 2.5cm} {\bf if} R {\bf has} gcd: (R,R) $\rightarrow$ R\\
+\hbox{\hskip 3.0cm} {\bf then} deriv(x) == $\ldots$\\
+\hbox{\hskip 3.0cm} {\bf else} deriv(x) == $\ldots$
+\vskip 0.2cm
+RationalFunction(x:Expression, R:Ring) == QuotientField(Polynomial(x,R))
+\vskip 0.2cm
+RationalNumber == QuotientField(Integer)
+\vskip -0.2cm
+\hrulefill
+
+
\chapter{Details for Programmers}
Axiom maintains internal representations for domains.
There are functions for examining the internals of objects of
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 7dc1493..494fe73 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2419,7 +2419,8 @@ paper = "Brea89.pdf"
components may be combined to solve scientific problems that can not
be solved within a single CAS, or may be organised into a system for
distributed parallel computations.",
- paper = "Lint10.pdf"
+ paper = "Lint10.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -2486,7 +2487,7 @@ paper = "Brea89.pdf"
algebraic algorithms at hand and a much better understanding of data
structures and programming constructs than only a few years ago.",
paper = "Loos74.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -7907,7 +7908,8 @@ when shown in factored form.
numbers in the Maple computer algebra system. Exact reals are
represented by potentially infinite lists of binary digits, and
interpreted as sums of negative powers of the golden ratio.",
- paper = "Kels00.pdf"
+ paper = "Kels00.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -9218,11 +9220,15 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\index{Gottlieben, Hanne}
\index{Linton, Steve A.}
\index{Martin, Ursula}
-\begin{chunk}{ignore}
-\bibitem[Adams 99]{Adam99} Adams, A.A.; Gottlieben, H.; Linton, S.A.;
-Martin, U.
+\begin{chunk}{axiom.bib}
+@inproceedings{Adam99,
+ author = "Adams, Andrew A. and Gottlieben, Hanne and Linton, Steve A. and
+ Martin, Ursula",
title = "Automated theorem proving in support of computer algebra:
symbolic definite integration as a case study",
+ booktitle = "ISSAC '99",
+ pages = "253-260",
+ year = "1999",
abstract = "
We assess the current state of research in the application of computer
aided formal reasoning to computer algebra, and argue that embedded
@@ -9240,7 +9246,9 @@ Martin, U.
algebra systems [CAS] do not. We extend upon Fateman's web-based table
by including parametric limits of integration and queries with side
conditions.",
- paper = "Adam99.pdf"
+ paper = "Adam99.pdf",
+ keywords = "axiomref, CAS-Proof"
+}
\end{chunk}
@@ -9271,7 +9279,7 @@ Martin, U.
library. These examples provide proofs which are both illustrative and
applicable to genuine symbolic computation problems.",
paper = "Adam01.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -9358,7 +9366,8 @@ Martin, U.
title = "LEAN proof of GCD",
link =
"\url{http://github.com/leanprover/lean2/blob/master/library/data/nat/gcd.lean}",
- year = "2014"
+ year = "2014",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -9418,7 +9427,8 @@ Martin, U.
we specify syntax translations for the concrete syntax of Maple
which enables the communication between both systems illustrated by
some examples that can be solved by theorems and algorithms",
- paper = "Ball95.pdf"
+ paper = "Ball95.pdf",
+ keywords = "CAS-Proof"
}
@@ -9447,7 +9457,8 @@ Martin, U.
experimental interface therefore uses a computer algebra library. It
is based on theorem templates, which provide formal specifications for
the algorithms.",
- paper = "Ball98.pdf"
+ paper = "Ball98.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -9485,7 +9496,7 @@ Martin, U.
system on the tactic-level of Isabelle and its integration into proof
procedures.",
paper = "Ball99.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -9530,7 +9541,8 @@ Martin, U.
Some examples of communication forms are given that show how the
participants benefit",
- paper = "Bare01.pdf"
+ paper = "Bare01.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -9850,7 +9862,7 @@ Martin, U.
exactly the mathematical dependencies between different structures.
This may ease the achievement of proofs.",
paper = "Boul99.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -10220,7 +10232,8 @@ Martin, U.
title = "Analytica -- A Theorem Prover in Mathematica",
year = "1991",
link = "\url{http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Analytica%20A%20Theorem%20Prover%20in%20Mathematica.pdf}",
- paper = "Clar91.pdf"
+ paper = "Clar91.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -10394,7 +10407,7 @@ Martin, U.
our claim that the Nuprl proof development system is especially well
suited to support this kind of mathematics.",
paper = "Cons98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -10517,7 +10530,8 @@ England, Matthew; Wilson, David
year = "2017",
comment = "BPR presentation, Cambridge, England",
video = "Dave17a.mp4",
- paper = "Dave17a.pdf"
+ paper = "Dave17a.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -10670,7 +10684,7 @@ England, Matthew; Wilson, David
a modest cost. Our approach is based on retargeting the code generator
of the OpenAxiom compiler to the Poly/ML abstract machine.",
paper = "Dosr11.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -10712,7 +10726,7 @@ England, Matthew; Wilson, David
methodology for Aldor program analysis and verification. There are
examples of abstract specifications of Axiom primitives.",
paper = "Duns98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -10763,7 +10777,7 @@ England, Matthew; Wilson, David
case study of abstract specifications of AXIOM primitives, and provide
an interface between these abstractions and Aldor code.",
paper = "Duns99.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -10797,7 +10811,7 @@ England, Matthew; Wilson, David
execution of the algorithms, equivalent to testing over infinite test
sets, aids in debugging, while strengthening beliefs that the correctness
of results is an algebraic truth rather than an accident.",
- paper = "Fate02a.pdf"
+ paper = "Fate02a.pdf, CAS-Proof"
}
\end{chunk}
@@ -10832,7 +10846,8 @@ England, Matthew; Wilson, David
sketch a proof of a numerical program to compute sine, and display a
related approach to a version of a Bessel function algorithm for J0(x)
based on a recurrence.",
- paper = "Fate03a.pdf"
+ paper = "Fate03a.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -10985,7 +11000,7 @@ England, Matthew; Wilson, David
practice. Apart rom the inheritance and reuse of properties, the
algebraic hierarchy has proven very useful for reusing notations.",
paper = "Geuv02.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11076,7 +11091,7 @@ England, Matthew; Wilson, David
of verification conditions, harnesses to ensure more reliable
differential equation solvers, and verifiable look-up tables.",
paper = "Gott05.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11208,7 +11223,7 @@ England, Matthew; Wilson, David
reals which combines the rigour of a theorem prover with the power of
a computer algebra system.",
paper = "Harr94.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11364,7 +11379,7 @@ England, Matthew; Wilson, David
algebra system and the relevance of this work for abstract functional
programming.",
paper = "Jack94.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11421,7 +11436,7 @@ England, Matthew; Wilson, David
discusses the appropriateness of this foundation, and the extent to
which the work relied on it.",
paper = "Jack95.pdf",
- keyword = "axiomref"
+ keyword = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11467,7 +11482,7 @@ England, Matthew; Wilson, David
prototype, but can be straightforwardly scaled up to a practical
computer algebra system.",
paper = "Kali07.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11552,7 +11567,7 @@ England, Matthew; Wilson, David
well-suited for producing a high-level verbalised explication as well
as for a low-level (machine checkable) calculus-level proof.",
paper = "Kerb96.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -11581,7 +11596,8 @@ England, Matthew; Wilson, David
protocol known as SC- SCP. We describe general aspects of viewing
OpenMath terms produced by a CAS in the calculus of Coq, as well as
viewing pure Coq terms in a simpler type system that is behind OpenMath.",
- paper = "Kome11.pdf"
+ paper = "Kome11.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -12143,7 +12159,8 @@ England, Matthew; Wilson, David
given by the approach. The {\tt Agda} functional language is used as an
instrument. This paper is a continuation for the introductory paper
published in this journal in 2014. (In Russian)",
- paper = "Mesh15.pdf"
+ paper = "Mesh15.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -12749,7 +12766,7 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
The paper shows an interesting way to decorate Axiom with pre- and
post-conditions.",
paper = "Poll98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -12791,10 +12808,13 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
-@misc{Poll00,
+@article{Poll00,
author = "Poll, Erik and Thompson, Simon",
title = "Integrating Computer Algebra and Reasoning through the Type
System of Aldor",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1794",
+ pages = "136-150",
year = "2000",
abstract =
"A number of combinations of reasoning and computer algebra systems
@@ -12950,7 +12970,7 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
given algorithm a set of theorems that imply the correctness of this
algorithm.",
paper = "Schw97.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -14068,6 +14088,34 @@ J. Symbolic COmputations 36 pp 855-889
\section{Expression Simplification} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Fortenbacher, Albrecht}
+\begin{chunk}{axiom.bib}
+@article{Fort87,
+ author = "Fortenbacher, Albrecht",
+ title = "An Algebraic Approach to Unification Under Associativity and
+ Commutativity",
+ journal = "J. Symbolic Computation",
+ volume = "3",
+ pages = "217-229",
+ year = "1987",
+ abstract =
+ "From the work of Siekmann and Livesey, and Stickel it is known how to
+ unify two terms in an associative and commutative theory: transfer the
+ terms into Abelian strings, look for mappings which solve the problem
+ in the Abelian monoid, and decide whether a mapping can be regarded as
+ a unifier. Very often most of the mappings are thus eliminated, and
+ so it is crucial for efficiency either to not create these unnecessary
+ solutions or to remove them as soon as possible. The following work
+ formalises the transformations between the free algebra and this
+ monoid. This leads to an algorithm which uses maximal information for
+ its search for solutions in the monoid. It is both very efficient and
+ easily verifiable. Some applications of this algorithm are shown in
+ the appendix.",
+ paper = "Fort87.pdf"
+}
+
+\end{chunk}
+
\index{Carette, Jacques}
\begin{chunk}{ignore}
\bibitem[Carette 04]{Car04} Carette, Jacques
@@ -22657,7 +22705,8 @@ Proc ISSAC 97 pp172-175 (1997)
computations can be done to variable (presumably high) precision. We
introduce notations p-representable and p-negligible where p denotes
precision, and show how this helps in our applications.",
- paper = "Fate03.pdf"
+ paper = "Fate03.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -28235,6 +28284,25 @@ April 8-9, 2013 Portland Oregon
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
+@article{Dave90a,
+ author = "Davenport, James H.",
+ title = "Current Problems in Computer Algebra Systems Design",
+ journal = "LNCS",
+ volume = "429",
+ year = "1990",
+ pages = "1-9",
+ abstract =
+ "Computer Algebra systems have been with us for over twenty years, but
+ there is still no consensus on what an ``ideal'' system would look
+ like. There are all sorts of tradeoffs between portability,
+ functionality, and efficiency. This paper discusses some of those issues.",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
@techreport{Dave92e,
author = "Davenport, James H.",
title = "The AXIOM System",
@@ -28340,6 +28408,7 @@ VM/370 SPAD.SCRIPTS August 24, 1979 SPAD.SCRIPT
(e.g. PLUS could be declared for Integer arguments, or Rational, or
Real, or even Polynomial arguments) and the system will apply the
correct function for the types of the arguments.",
+ paper = "Dave81a.pdf",
keywords = "axiomref"
}
@@ -28581,7 +28650,7 @@ VM/370 SPAD.SCRIPTS August 24, 1979 SPAD.SCRIPT
mathematical equality and with data structure equality, and to
explain how necessary it is to keep a clear distintion between the two.",
paper = "Dave02.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -28821,7 +28890,7 @@ UK / etc., 1989 ISBN 3-540-51517-8 LCCN QA155.7.E4E86 1987
conventional, non-constructive, theory. It is also somewhat different
from the theories of Seidenberg [1974] and his school, who are not
particularly concerned with practical questions of efficiency.",
- paper = "Dave90.pdf",
+ paper = "Dave90c.pdf",
keywords = "axiomref",
beebe = "Davenport:1992:SVAa"
}
@@ -30507,7 +30576,7 @@ Grant citation GR/L48256 Nov 1, 1997-Feb 28, 2001
are inspired by the IMPS Interactive Mathematical Proof System and the
Axiom computer algebra system.",
paper = "Farm03.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -31381,6 +31450,23 @@ LCCN QA155.7.E4 I57 1984
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Galligo, A.}
+\index{Grimm, J.}
+\index{Pottier, L.}
+\begin{chunk}{axiom.bib}
+@article{Gall90,
+ author = "Galligo, A. and Grimm, J. and Pottier, L.",
+ title = "The Design of SISYPHE: A System for doing Symbolic and
+ Algebraic Computations",
+ journal = "LNCS",
+ volume = "429",
+ pages = "30-39",
+ year = "1990",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Gallopoulos, Stratis}
\index{Houstis, Elias}
\index{Rice, John}
@@ -32754,7 +32840,7 @@ April 1976 (private copy)
of computer algebra results proved formally in the HOL theorem prover
with the aid of Maple.",
paper = "Harr98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -33523,6 +33609,8 @@ Springer-Verlag, Berlin, Germany / Heildelberg, Germany / London, UK / etc.,
\end{chunk}
+\subsection{I} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Jacob, G.}
@@ -33958,6 +34046,7 @@ Watson Research Center, Yorktown Heights, NY, USA, 1969 RC2968 July 1970
properties appears novel among programming languages (cf. image
functor of RUSSELL) and leads to a very powerful notion of abstract
algorithms missing from other work on data types known to the authors.",
+ paper = "Jenk81.pdf",
keywords = "axiomref"
}
@@ -34972,7 +35061,7 @@ Ph.D. Thesis, University of St Andrews, 1999
and (iii) interface specifications which assist the verification of
pre- and post conditions of implemented code.",
paper = "Kels00a.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -35020,7 +35109,7 @@ Ph.D. Thesis, University of St Andrews, 1999
on stochastic differentials, of the Mardia-Dryden distribution from
statistical shape theory.",
paper = "Kend01.pdf",
- keywords = "axiomref",
+ keywords = "axiomref, CAS-Proof",
beebe = "Kendall:2001:SIC"
}
@@ -35123,7 +35212,7 @@ Ph.D. Thesis, University of St Andrews, 1999
calculus-level proof. We present an implementation of our ideas and
exemplify them using an automatically solved example.",
paper = "Kerb98.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -35350,6 +35439,20 @@ Ph.D. Thesis, University of St Andrews, 1999
\index{Kredel, Heinz}
\begin{chunk}{axiom.bib}
+@article{Kred90,
+ author = "Kredel, Heinz",
+ title = "MAS Modula-2 Algebra System",
+ journal = "LNCS",
+ volume = "429",
+ pages = "270-271",
+ year = "1990",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Kredel, Heinz}
+\begin{chunk}{axiom.bib}
@article{Kred08,
author = "Kredel, Heinz",
title = "On a Java computer algebra system,
@@ -38568,6 +38671,8 @@ Computers and Mathematics November 1993, Vol 40, Number 9 pp1203-1210
\end{chunk}
+\subsection{Q} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Ralston, Anthony}
@@ -39170,7 +39275,7 @@ J. of Symbolic Computation 36 pp 513-533 (2003)
concepts. The full calculus has been implemented and tested with our
LA compiler which generates executable files.",
paper = "Sant96.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, CAS-Proof"
}
\end{chunk}
@@ -42574,6 +42679,8 @@ Software Preservation Group
\end{chunk}
+\subsection{X} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\subsection{Y} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Yap, Chee Keng}
@@ -42883,6 +42990,17 @@ Dover Publications. (1968)
\end{chunk}
+\begin{chunk}{axiom.bib}
+@book{ADAx83,
+ author = "U.S. Government",
+ title = "The Programming Language Ada Reference Manual",
+ publisher = "U.S. Government",
+ year = "1983",
+ comment = "STD-1815A-1983"
+}
+
+\end{chunk}
+
\index{Altmann, Simon L.}
\begin{chunk}{axiom.bib}
@book{Altm05,
@@ -42930,6 +43048,46 @@ National Physical Laboratory. (1982)
\end{chunk}
+\index{Astesiano, Egidio}
+\index{Bidoit, Michel}
+\index{Kirchner, Helene}
+\index{Krieg-Bruckner, Bernd}
+\index{Mosses, Peter D.}
+\index{Sannella, Donald}
+\index{Tarlecki, Andrzej}
+\begin{chunk}{axiom.bib}
+@article{Aste02,
+ author = "Astesiano, Egidio and Bidoit, Michel and Kirchner, Helene and
+ Krieg-Bruckner, Bernd and Mosses, Peter D. and Sannella, Donald
+ and Tarlecki, Andrzej",
+ title = "CASL: the Common Algebraic Specification Language",
+ journal = "Theoretical Computer Science",
+ volume = "286",
+ number = "2",
+ pages = "153-196",
+ year = "2002",
+ abstract =
+ "The Common Algebraic Specification Language (CASL) is an expressive
+ language for the formal specification of functional requirements and
+ modular design of software. It has been designed by COFI, the
+ international Common Framework Initiative for algebraic specification
+ and development. It is based on a critical selection of features that
+ have already been explored in various contexts, including subsorts,
+ partial functions, first-order logic, and structured and architectural
+ specifications. CASL should facilitate interoperability of many
+ existing algebraic prototyping and verification tools.
+
+ This paper gives an overview of the CASL design. The major issues that
+ had to be resolved in the design process are indicated, and all the
+ main concepts and constructs of CASL are briefly explained and
+ illustrated — the reader is referred to the CASL Language Summary for
+ further details. Some familiarity with the fundamental concepts of
+ algebraic specification would be advantageous.",
+ paper = "Aste02.pdf"
+}
+
+\end{chunk}
+
\index{TriangularSetCategory}
\index{RegularTriangularSetCategory}
\index{NormalizedTriangularSetCategory}
@@ -43048,6 +43206,28 @@ National Physical Laboratory. (1982)
\end{chunk}
+\index{Ausiello, Giovanni Francesco Mascari}
+\begin{chunk}{axiom.bib}
+@article{Ausi79,
+ author = "Ausiello, Giovanni Francesco Mascari",
+ title = "On the Design of Algebraic Data Structures with the
+ Approach of Abstract Data Types",
+ journal = "LNCS",
+ volume = "72",
+ year = "1979",
+ pages = "514-530",
+ abstract =
+ "The problem of giving a formal definition of the representation of
+ algebraic data structures is considered and developped in the frame
+ work of the abstract data types approach. Such concepts as canonical
+ form and simplification are formalized and related to properties of
+ the abstract specification and of the associated term rewriting
+ system.",
+ paper = "Ausi79.pdf"
+}
+
+\end{chunk}
+
\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
@misc{Avig12,
@@ -43056,7 +43236,8 @@ National Physical Laboratory. (1982)
Mathematical Computation",
year = "2012",
comment = "slides",
- paper = "Avig12.pdf"
+ paper = "Avig12.pdf",
+ keywords ="CAS-Proof"
}
\end{chunk}
@@ -43219,6 +43400,37 @@ Comm. ACM. 17, 6 319--320. (1974)
\end{chunk}
+\index{Bauer, Andrej}
+\index{Clarke, Edmund}
+\index{Zhao, Xudong}
+\begin{chunk}{axiom.bib}
+@article{Baue98,
+ author = "Bauer, Andrej and Clarke, Edmund and Zhao, Xudong",
+ title = "Analytica -- An Experiment in Combining Theorem Proving and
+ Symbolic Computation",
+ journal = "Journal of Automated Reasoning",
+ volume = "21",
+ number = "3",
+ pages = "295-325",
+ year = "1998",
+ abstract =
+ "Analytica is an automatic theorem prover for theorems in elementary
+ analysis. The prover is written in the Mathematica language and runs
+ in the Mathematica environment. The goal of the project is to use a
+ powerful symbolic computation system to prove theorems that are beyond
+ the scope of previous automatic theorem provers. The theorem prover is
+ also able to deduce the correctness of certain simplification steps
+ that would otherwise not be performed. We describe the structure of
+ Analytica and explain the main techniques that it uses to construct
+ proofs. Analytica has been able to prove several nontrivial
+ theorems. In this paper, we show how it can prove a series of lemmas
+ that lead to the Bernstein approximation theorem.",
+ paper = "Baue98.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Beauzamy, Bernard}
\begin{chunk}{ignore}
\bibitem[Beauzamy 92]{Bea92} Beauzamy, Bernard
@@ -43265,6 +43477,45 @@ J. Symbolic Computation (1993) 15, 393-413
\end{chunk}
+\index{Bertoli, P.}
+\index{Calmet, J.}
+\index{Guinchiglia, F.}
+\index{Homann, K.}
+\begin{chunk}{axiom.bib}
+@article{Bert98,
+ author = "Bertoli, P. and Calmet, J. and Guinchiglia, F. and Homann, K.",
+ title = "Specification and Integration of Theorem Provers and Computer
+ Algebra Systems",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1476",
+ year = "1998",
+ pages = "94-106",
+ abstract =
+ "Computer algebra systems (CASs) and automated theorem provers (ATPs)
+ exhibit complementary abilities. CASs focus on efficiently solving
+ domain-specific problems. ATPs are designed to allow for the
+ formalization and solution of wide classes of problems within some
+ logical framework. Integrating CASs and ATPs allows for the solution
+ of problems of a higher complexity than those confronted by each class
+ alone. However, most experiments conducted so far followed an ad-hoc
+ approach, resulting in tailored solutions to specific problems. A
+ structured and principled approach is necessary to allow for the sound
+ integration of systems in a modular way. The Open Mechanized Reasoning
+ Systems (OMRS) framework was introduced for the specification and
+ implementation of mechanized reasoning systems, e.g. ATPs. The
+ approach was recasted to the domain of computer algebra systems. In
+ this paper, we introduce a generalization of OMRS, named OMSCS (Open
+ Mechanized Symbolic Computation Systems). We show how OMSCS can be
+ used to soundly express CASs, ATPs, and their integration, by
+ formalizing a combination between the Isabelle prover and the Maple
+ algebra system. We show how the integrated system solves a problem
+ which could not be tackled by each single system alone.",
+ paper = "Bert98.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Bertrand, Laurent}
\begin{chunk}{axiom.bib}
@article{Bert95,
@@ -43575,12 +43826,103 @@ ISBN 3-7643-5901-3 (1998)
series = "ISSAC'98",
year = "1998",
address = "INRIA Sophia Antipolis",
- link = "\url{http://www-sop.inria.fr/cafe/Manuel.Bronstein/publications/issac98.pdf}",
+ link =
+"\url{http://www-sop.inria.fr/cafe/Manuel.Bronstein/publications/issac98.pdf}",
paper = "Bro98b.pdf"
}
\end{chunk}
+\index{de Bruijn, N.G.}
+\begin{chunk}{axiom.bib}
+@article{Brui94,
+ author = "de Bruijn, N.G.",
+ title = "A Survey on the project Automath",
+ journal = "Studies in Logic and the Foundations of Mathematics",
+ volume = "133",
+ year = "1994",
+ pages = "141-161",
+ abstract =
+ "Thus far, much about Automath has been written in separate
+ reports. Most of this work has been made available upon request, but
+ only a small part was published in journals, conference proceedings,
+ etc. Unfortunately, a general survey in the form of a book is still
+ lacking. A short survey was given in [de Bruijn 73c], but the present
+ one will be much more extensive. Naturally, this survey will report
+ about work that has been done, is going on, or is planned for the
+ future. But it will also be used to explain how various parts of the
+ project are related. Moreover we shall try to clarify a few points
+ which many outsiders consider as uncommon or even wierd. In particular
+ we spend quite some attention to our concept of types and the matter
+ of ``propositions as types'' (Section 14). Finally the survey will be
+ used to ventilate opinions and views in mathematics which are not
+ easily set down in more technical reports.",
+ paper = "Brui94.pdf"
+}
+
+\end{chunk}
+
+\index{Buchberger, B.}
+\index{Jebelean, Tudor}
+\index{Kriftner, Franz}
+\index{Vasaru, Daniela}
+\begin{chunk}{axiom.bib}
+@inproceedings{Buch77,
+ author = "Buchberger, B. and Jebelean, Tudor and Kriftner, Franz and
+ Vasaru, Daniela",
+ title = "A Survey on the Theorema Project",
+ booktitle = "ISSAC '97",
+ year = "1997",
+ abstract =
+ "The Theorema project aims at extending current computer algebra
+ systems by facilities for supporting mathematical proving. The present
+ early-prototype version of the Theorema software system is implemented
+ in Mathematica 3.0. The system consists of a general higher-order
+ predicate logic prover and a collection of special provers that call
+ each other depending on the particular proof situations. The
+ individual provers imitate the proof style of human mathematicians and
+ aim at producing human-readable proofs in natural language presented
+ in nested cells that facilitate studying the computer-generated proofs
+ at various levels of detail. The special provers are intimately
+ connected with the functors that build up the various mathematical
+ domains.",
+ paper = "Buch77.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
+\index{Buchberger, B.}
+\begin{chunk}{axiom.bib}
+@book{Buch96,
+ author = "Buchberger, B.",
+ title = "Symbolic Computation: Computer Algebra and Logic",
+ booktitle = "Frontiers of Combining Systems",
+ publisher = "Kluwer Academic",
+ year = "1996",
+ pages = "192-220",
+ abstract =
+ "In this paper we present our personal view of what should be the next
+ step in the development of symbolic computation systems. The main
+ point is that future systems should integrate the power of algebra and
+ logic. We identify four gaps between the future ideal and the systems
+ available at present: the logic, the syntax, the mathematics, and the
+ prover gap, respectively. We discuss higher order logic without
+ extensionality and with set theory as a subtheory as a logic frame for
+ future systems and we propose to start from existing computer algebra
+ systems and proceed by adding new facilities for closing the syntax,
+ mathematics, and the prover gaps. Mathematica seems to be a
+ particularly suitable candidate for such an approach. As the main
+ technique for structuring mathematical knowledge, mathematical methods
+ (including algorithms), and also mathematical proofs, we underline the
+ practical importance of functors and show how they can be naturally
+ embedded into Mathematica.",
+ paper = "Buch96.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Burge, William H.}
\begin{chunk}{axiom.bib}
@article{Burg74,
@@ -43611,6 +43953,20 @@ ISBN 3-7643-5901-3 (1998)
\end{chunk}
+\index{Burstall, R.M.}
+\index{Goguen, J.A.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Burs77,
+ author = "Burstall, R.M. and Goguen, J.A.",
+ title = "Putting THeories together to make Specifications",
+ booktitle = "IJCAI 77 Volume 2",
+ pages = "1045-1058",
+ year = "1977",
+ paper = "Burs77.pdf"
+}
+
+\end{chunk}
+
\index{Butler, Greg}
\begin{chunk}{axiom.bib}
@inproceedings{Butl96,
@@ -43641,6 +43997,41 @@ ISBN 3-7643-5901-3 (1998)
\subsection{C} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Calmet, Jacques}
+\index{Homann, Karsten}
+\begin{chunk}{axiom.bib}
+@book{Calm96,
+ author = "Calmet, Jacques and Homann, Karsten",
+ title = "Classification of Communication and Cooperation Mechanisms for
+ Logical and Symbolic Computation Systems",
+ booktitle = "Frontiers of Combining Systems",
+ publisher = "Kluwer Academic",
+ year = "1996",
+ pages = "221-234",
+ abstract =
+ "The combination of logical and symbolic computation systems has
+ recently emerged from prototype extensions of stand-alone systems to
+ the study of environments allowing interaction among several
+ systems. Communication and cooperation mechanisms of systems
+ performing any kind of mathematical service enable one to study and
+ solve new classes of problems and to perform efficient computation by
+ distributed specialized packages. The classification of communication
+ and cooperation methods for logical and symbolic computation systems
+ given in this paper provides and surveys different methodologies for
+ combining mathematical services and their characteristics,
+ capabilities, requirements, and differences. The methods are
+ illustrated by recent well-known examples. We separate the
+ classification into communication and cooperation methods. The former
+ includes all aspects of the physical connection, the flow of
+ mathematical information, the communication language(s) and its
+ encoding, encryption, and knowledge sharing. The latter concerns the
+ semantic aspects of architectures for cooperative problem solving.",
+ paper = "Calm96.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Cantor, D.}
\begin{chunk}{axiom.bib}
@article{Cant87,
@@ -43750,6 +44141,32 @@ Lecture Notes in Computer Science. 76 (1979) Springer-Verlag
\end{chunk}
+\index{Clarke, Edmund}
+\index{Zhao, Xudong}
+\begin{chunk}{axiom.bib}
+@techreport{Clar94,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Combining Symbolic Computation and Theorem Proving: Some
+ Problems of Ramanujan",
+ year = "1994",
+ type = "technical report",
+ institution = "Carnegie Mellon University",
+ number = "CMU-CS-94-103",
+ abstract =
+ "One way of building more powerful theorem provers is to use
+ techniques from symbolic computation. The challenge problems in this
+ paper are taken from Chapter 2 of Ramanujan''s Notebooks. They were
+ selected because they are non-trivial and require the use of symbolic
+ computation techniques. We have developed a theorem prover based on
+ the symbolic computation system Mathematica, that can prove all the
+ challenge problems completely automatically. The axioms and inference
+ rules for constructing the proofs are also briefly discussed.",
+ paper = "Clar94.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Clausen, M.}
\index{Fortenbacher, A.}
\begin{chunk}{ignore}
@@ -43792,10 +44209,21 @@ Rocky Mountain J. Math. 14 119--139. (1984)
\end{chunk}
-\index{Cohn, P.M.}
+\index{Cohn, Paul Moritz}
+\begin{chunk}{axiom.bib}
+@book{Cohn65,
+ author = "Cohn, Paul Moritz",
+ title = "Universal Algebra",
+ publisher = "Harper and Row",
+ year = "1965"
+}
+
+\end{chunk}
+
+\index{Cohn, Paul Moritz}
\begin{chunk}{axiom.bib}
@book{Cohn91,
- author = "Chon, P.M.",
+ author = "Cohn, Paul Moritz",
title = "Algebra (2nd Ed.)",
publisher = "Wiley",
isbn = "978-0471101697",
@@ -43948,6 +44376,19 @@ Princeton University Press. (1963)
\end{chunk}
+\index{Davenport, J.H.}
+\index{Jenks, R.D.}
+\begin{chunk}{axiom.bib}
+@misc{Dave80b,
+ author = "Davenport, J.H. and Jenks, R.D.",
+ title = "SCRATCHPAD/370: Modes and Domains",
+ year = "1980",
+ comment = "private communication",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@article{Dave81b,
@@ -44027,6 +44468,20 @@ Signum Newsletter. 13 (2) 12--18. (1978)
\end{chunk}
+\index{Demers, A.}
+\index{Donahue, J.}
+\begin{chunk}{axiom.bib}
+@techreport{Deme79,
+ author = "Demers, A. and Donahue, J.",
+ title = "Revised Report on RUSSELL",
+ year = "1979",
+ type = "technical report",
+ institution = "Cornell",
+ number = "TR 79-389"
+}
+
+\end{chunk}
+
\index{Demmel, J. W.}
\begin{chunk}{ignore}
\bibitem[Demmel 89]{Dem89} Demmel J W
@@ -44087,6 +44542,32 @@ SIAM J. Numer. Anal. 19 1286--1304. (1982)
\end{chunk}
+\index{Dolzmann, Andreas},
+\index{Sturm, Thomas}
+\begin{chunk}{axiom.bib}
+@article{Dolz97b,
+ author = "Dolzmann, Andreas and Sturm, Thomas",
+ title = "REDLOG: Computer Algebra meets Computer Logic",
+ journal = "ACM SIGSAM Bulletin",
+ volume = "31",
+ number = "2",
+ year = "1997",
+ pages = "2-9",
+ abstract =
+ "REDLOG is a package that extends the computer algebra system REDUCE
+ to a computer logic system, i.e., a system that provides algorithms
+ for the symbolic manipulation of first-order formulas over some
+ temporarily fixed language and theory. In contrast to theorem provers,
+ the methods applied know about the underlying algebraic theory and
+ make use of it. We illustrate some applications of REDLOG, describe
+ its functionality as it appears to the user, and explain the design
+ issues and implementation techniques. REDLOG is available on the WWW.",
+ paper = "Dolz97b.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Dongarra, Jack J.}
\index{Moler, C. B.}
\index{Bunch, J. R.}
@@ -44186,6 +44667,28 @@ pp 18-28
\end{chunk}
+\index{Dowek, Gilles}
+\begin{chunk}{axiom.bib}
+@article{Dowe00,
+ author = "Dowek, Gilles",
+ title = "Axioms vs Rewrite Rules: From Completeness to Cut Elimination",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1794",
+ pages = "62-72",
+ year = "2000",
+ abstract =
+ "Combining a standard proof search method, such as resolution or
+ tableaux, and rewriting is a powerful way to cut off search space in
+ automated theorem proving, but proving the completeness of such
+ combined methods may be challenging. It may require in particular to
+ prove cut elimination for an extended notion of proof that combines
+ deductions and computations. This suggests new interactions between
+ automated theorem proving and proof theory.",
+ paper = "Dowe00.pdf"
+}
+
+\end{chunk}
+
\index{Ducos, Lionel}
\begin{chunk}{ignore}
\bibitem[Ducos 00]{Duc00} Ducos, Lionel
@@ -44217,6 +44720,29 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\end{chunk}
+\index{Dutertre, Bruno}
+\begin{chunk}{axiom.bib}
+@article{Dute96,
+ author = "Dutertre, Bruno",
+ title = "Elements of Mathematical Analysis in PVS",
+ journal = "LNCS",
+ volume = "1125",
+ pages = "141-156",
+ year = "1996",
+ abstract =
+ "This paper presents the formalization of some elements of
+ mathematical analysis using the PVS verification system. Our main
+ motivation was to extend the existing PVS libraries and provide means
+ of modelling and reasoning about hybrid systems. The paper focuses on
+ several important aspects of PVS including recent extensions of the
+ type system and discusses their merits and effectiveness. We conclude
+ by a brief comparison with similar developments using other theorem
+ provers.",
+ paper = "Dute96.pdf"
+}
+
+\end{chunk}
+
\index{Duval, Dominique}
\index{Gonz\'alez-Vega, L.}
\begin{chunk}{axiom.bib}
@@ -44344,6 +44870,8 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\end{chunk}
+\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Fateman, Richard J.}
@@ -44921,6 +45449,26 @@ Grove, IL, USA and Oxford, UK, 1992
\end{chunk}
+\index{Griss, Martin L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gris76,
+ author = "Griss, Martin L.",
+ title = "The Definition and Use of Data Structures in REDUCE",
+ booktitle = "SYMSAC '76",
+ pages = "53-59",
+ year = "1976",
+ abstract =
+ "This paper gives a brief description and motivation of the mode
+ analyzing and data-structuring extensions to the algebraic language
+ REDUCE. These include generic functions, user defined recursive data
+ structures, mode transfer functions and user modifiable automatic
+ coercion. A number of examples are given to illustrate the style and
+ features of the language, and how it will aid in the construction of
+ more efficient and reliable programs."
+}
+
+\end{chunk}
+
\index{Gruntz, Dominik}
\begin{chunk}{ignore}
\bibitem[Gruntz 93]{Gru93} Gruntz, Dominik
@@ -45188,6 +45736,32 @@ Lecture Notes in Economics and Mathematical Systems. 187 Springer-Verlag. 1981
\index{Homann, Karsten}
\index{Calmet, Jacques}
\begin{chunk}{axiom.bib}
+@article{Homa94,
+ author = "Homann, Karsten and Calmet, Jacques",
+ title = "Combining Theorem Proving and Symbolic Mathematical Computing",
+ journal = "LNCS",
+ volume = "958",
+ pages = "18-29",
+ year = "1994",
+ abstract =
+ "An intelligent mathematical environment must enable symbolic
+ mathematical computation and sophisticated reasoning techniques on the
+ underlying mathematical laws. This paper disscusses different possible
+ levels of interaction between a symbolic calculator based on algebraic
+ algorithms and a theorem prover. A high level of interaction requires
+ a common knowledge representation of the mathematical knowledge of the
+ two systems. We describe a model for such a knowledge base mainly
+ consisting of type and algorithm schemata, algebraic algorithms and
+ theorems.",
+ paper = "Homa94.pdf",
+ keywords = "axiomref, CAS-Proof"
+}
+
+\end{chunk}
+
+\index{Homann, Karsten}
+\index{Calmet, Jacques}
+\begin{chunk}{axiom.bib}
@article{Homa05,
author = "Homann, Karsten and Calmet, Jacques",
title = "Structures for Symbolic Mathematical Reasoning and Computation",
@@ -45204,7 +45778,8 @@ Lecture Notes in Economics and Mathematical Systems. 187 Springer-Verlag. 1981
reasoning and computation theories and structures provide a formal
framework for the specification of symbolic mathematical problem
solving by cooperation of algorithms and theorems.",
- paper = "Homa05.pdf"
+ paper = "Homa05.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -45739,7 +46314,8 @@ J. Symbolic Computations 8, 545-552 (1989)
version = "2.2.2",
year = "2017",
link = "\url{}",
- paper = "Kono17.pdf"
+ paper = "Kono17.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -45981,7 +46557,18 @@ Prentice-Hall. (1974)
\end{chunk}
-\index{Lewis, J. G,}
+\index{Levenworth, B.}
+\begin{chunk}{axiom.bib}
+@misc{Leve80,
+ author = "Levenworth, B.",
+ title = "ADAPT Reference Manual",
+ comment = "IBM Research",
+ year = "1980"
+}
+
+\end{chunk}
+
+`\index{Lewis, J. G,}
\begin{chunk}{ignore}
\bibitem[Lewis 77]{Lew77} Lewis J G,
title = "Algorithms for sparse matrix eigenvalue problems",
@@ -46011,7 +46598,8 @@ Addison-Wesley (March 1979) ISBN 0201144611
volume = "34",
pages = "239-239",
year = "2002",
- paper = "Lint02.pdf"
+ paper = "Lint02.pdf",
+ keywords = "CAS-Proof"
}
\end{chunk}
@@ -46438,6 +47026,32 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
\end{chunk}
+\index{Melham, Thomas F.}
+\begin{chunk}{axiom.bib}
+@article{Melh02,
+ author = "Melham, Thomas F.",
+ title = "PROSPER An Investigation into Software Architecture for Embedded
+ Proof Engines",
+ journal = "LNCS",
+ volume = "2309",
+ pages = "193-206",
+ year = "2002",
+ abstract =
+ "Prosper is a recently-completed ESPRIT Framework IV research project
+ that investigated software architectures for component-based, embedded
+ formal verification tools. The aim of the project was to make
+ mechanized formal analysis more accessible in practice by providing a
+ framework for integrating formal proof tools inside other software
+ applications. This paper is an extended abstract of an invited
+ presentation on Prosper given at FroCoS 2002. It describes the vision
+ of the Prosper project and provides a summary of the technical
+ approach taken and some of the lessons learned.",
+ paper = "Melh02.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Mignotte, Maurice}
\begin{chunk}{ignore}
\bibitem[Mignotte 82]{Mig82} Mignotte, Maurice
@@ -47658,6 +48272,35 @@ The University of Chicago Press. 1974
\end{chunk}
+\index{Sorge, Volker}
+\begin{chunk}{axiom.bib}
+@article{Sorg00,
+ author = "Sorge, Volker",
+ title = "Non-trivial Symbolic Computations in Proof Planning",
+ journal = "LNCS",
+ volume = "1794",
+ pages = "121-135",
+ year = "2000",
+ abstract =
+ "We discuss a pragmatic approach to integrate computer algebra into
+ proof planning. It is based on the idea to separate computation and
+ verification and can thereby exploit the fact that many elaborate
+ symbolic computations are trivially checked. In proof planning the
+ separation is realized by using a powerful computer algebra system
+ during the planning process to do non-trivial symbolic
+ computations. Results of these computations are checked during the
+ refinement of a proof plan to a calculus level proof using a small,
+ self-implemented system that gives us protocol information on its
+ calculation. This protocol can be easily expanded into a checkable
+ low-level calculus proof ensuring the correctness of the
+ computation. We demonstrate our approach with the concrete
+ implementation in the $\Omega$MEGA system.",
+ paper = "Sorg00.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{DoubleFloatSpecialFunctions}
\index{Steele, Guy L.}
\begin{chunk}{axiom.bib}
@@ -47782,6 +48425,37 @@ J. Comput. Phys. 52 340--350. (1983)
\end{chunk}
+\index{Thatcher, J.W.}
+\index{Wagner, E.G.}
+\index{Wright, J.B.}
+\begin{chunk}{axiom.bib}
+@article{That82,
+ author = "Thatcher, J.W. and Wagner, E.G. and Wright, J.B.",
+ title = "Data Type Specification: Parameterization and the Power of
+ Specification Techniques",
+ journal = "ACM TOPLAS",
+ volume = "4",
+ number = "4",
+ pages = "711-732",
+ year = "1982",
+ abstract =
+ "Our earlier work on abstract data types is extended by the answers to
+ a number of questions on the power and limitations of algebraic
+ specification techniques and by an algebraic treatment of
+ parameterized data types like {\bf sets-of()} and
+ {\bf stacks-of-()}. The ``hidden function'' problem (the need to include
+ operations in specifications which are wanted hidden from the user) is
+ investigated; the relative power of conditional specifications and
+ equational specifications is investigated; the relative power of
+ conditional specifications and equational specifications is
+ investigated; and it is shown that parameterized specifications must
+ contain ``side conditions'' (e.g. that {\bf finite-sets-of-d} requires
+ an equality predicate on {\bf d}).",
+ paper = "That82.pdf"
+}
+
+\end{chunk}
+
\index{Thurston, William P.}
\begin{chunk}{axiom.bib}
@article{Thur94,
@@ -47959,6 +48633,32 @@ SIAM J. Numer. Anal. 12 835--853. 1975
\end{chunk}
+\index{Wegbreit, Ben}
+\begin{chunk}{axiom.bib}
+@article{Wegb74,
+ author = "Wegbreit, Ben",
+ title = "The Treatment of Data Types in EL1",
+ journal = "Communications of the ACM",
+ volume = "17",
+ number = "5",
+ year = "1974",
+ pages = "251-264",
+ abstract =
+ "In constructing a general purpose programming language, a key issue
+ is providing a sufficient set of data types and associated operations
+ in a manner that permits both natural problem-oriented notation and
+ efficient implementation. The EL1 language contains a number of
+ features specifically designed to simultaneously satisfy both
+ requirements. The resulting treatment of data types includes provision
+ for programmer-defined data types and generaic routines, programmer
+ control over type conversion, and very flexible data type behavior, in
+ a context that allows efficient compiled code and compact data
+ representation.",
+ paper = "Wegb74.pdf"
+}
+
+\end{chunk}
+
\index{Weil, Andr\'{e}}
\begin{chunk}{axiom.bib}
@misc{Weil71,
@@ -48150,6 +48850,44 @@ MM Research Preprints, 1987
\end{chunk}
+\index{Wulf, William A.}
+\index{London, Ralph L.}
+\index{Shaw, Mary}
+\begin{chunk}{axiom.bib}
+@article{Wulf76,
+ author = "Wulf, William A. and London, Ralph L. and Shaw, Mary",
+ title = "An Introduction to the Construction and Verification of
+ Alphard Programs",
+ journal = "IEEE Tr. Software Engineering",
+ volume = "SE-2",
+ number = "4",
+ year = "1976",
+ pages = "253-265",
+ abstract =
+ "The programming language Alphard is designed to provide support for
+ both the methodologies of ``well-structured'' programming and the
+ techniques of formal program verification. Language constructs allow
+ a programmer to isolate an abstraction, specifying its behavior
+ publicly while localizing. knowledge about its implementation. The
+ verification of such an abstraction consists of showing that its
+ implementation behaves in accordance with its public specifications;
+ the abstraction can then be used with confidence in constructing
+ other programs, and the verification of that use employs only the
+ public specifications. This paper introduces Alphard by developing
+ and verifying a data structure definition and a program that uses it.
+ It shows how each language construct contributes to the development of
+ the abstraction and discusses the way the language design and the
+ verification methodology wete tailored to each other. It serves not
+ only as an introduction to Alphard, but also as an example of the
+ symbiosis between verification and methodology in language design.
+ The strategy of program structuring, illustrated for Alphard, is
+ also applicable to most of the ``data abstraction'' mechanisms now
+ appearing.",
+ paper = "Wulf76.pdf"
+}
+
+\end{chunk}
+
\index{Wynn, P.}
\begin{chunk}{ignore}
\bibitem[Wynn 56]{Wynn56} Wynn P.
@@ -48158,6 +48896,8 @@ Math. Tables Aids Comput. 10 91--96. (1956)
\end{chunk}
+\subsection{X} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\subsection{Y} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Z} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/changelog b/changelog
index 23f7786..0fee1a4 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,7 @@
+20170905 tpd src/axiom-website/patches.html 20170905.01.tpd.patch
+20170905 tpd books/bookvol3 Additional explanations and references
+20170905 tpd books/bookvolbib Additional explanations and references
+20170905 tpd books/axiom.bib publish the bibliography
20170902 tpd src/axiom-website/patches.html 20170902.01.tpd.patch
20170902 tpd src/axiom-website/documentation.html add Caviness quote
20170901 tpd src/axiom-website/patches.html 20170901.01.tpd.patch
diff --git a/patch b/patch
index 4b3db8d..a20c42d 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,664 @@
-src/axiom-website/documentation.html add Caviness quote
+books/bookvol3 Additional explanations and references
-Goal: Axiom Literate Programming
+Goal: Proving Axiom Correct
+
+\index{Bertoli, P.}
+\index{Calmet, J.}
+\index{Guinchiglia, F.}
+\index{Homann, K.}
+\begin{chunk}{axiom.bib}
+@article{Bert98,
+ author = "Bertoli, P. and Calmet, J. and Guinchiglia, F. and Homann, K.",
+ title = "Specification and Integration of Theorem Provers and Computer
+ Algebra Systems",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1476",
+ year = "1998",
+ pages = "94-106",
+ abstract =
+ "Computer algebra systems (CASs) and automated theorem provers (ATPs)
+ exhibit complementary abilities. CASs focus on efficiently solving
+ domain-specific problems. ATPs are designed to allow for the
+ formalization and solution of wide classes of problems within some
+ logical framework. Integrating CASs and ATPs allows for the solution
+ of problems of a higher complexity than those confronted by each class
+ alone. However, most experiments conducted so far followed an ad-hoc
+ approach, resulting in tailored solutions to specific problems. A
+ structured and principled approach is necessary to allow for the sound
+ integration of systems in a modular way. The Open Mechanized Reasoning
+ Systems (OMRS) framework was introduced for the specification and
+ implementation of mechanized reasoning systems, e.g. ATPs. The
+ approach was recasted to the domain of computer algebra systems. In
+ this paper, we introduce a generalization of OMRS, named OMSCS (Open
+ Mechanized Symbolic Computation Systems). We show how OMSCS can be
+ used to soundly express CASs, ATPs, and their integration, by
+ formalizing a combination between the Isabelle prover and the Maple
+ algebra system. We show how the integrated system solves a problem
+ which could not be tackled by each single system alone.",
+ paper = "Bert98.pdf"
+}
+
+\end{chunk}
+
+\index{Dolzmann, Andreas},
+\index{Sturm, Thomas}
+\begin{chunk}{axiom.bib}
+@article{Dolz97b,
+ author = "Dolzmann, Andreas and Sturm, Thomas",
+ title = "REDLOG: Computer Algebra meets Computer Logic",
+ journal = "ACM SIGSAM Bulletin",
+ volume = "31",
+ number = "2",
+ year = "1997",
+ pages = "2-9",
+ abstract =
+ "REDLOG is a package that extends the computer algebra system REDUCE
+ to a computer logic system, i.e., a system that provides algorithms
+ for the symbolic manipulation of first-order formulas over some
+ temporarily fixed language and theory. In contrast to theorem provers,
+ the methods applied know about the underlying algebraic theory and
+ make use of it. We illustrate some applications of REDLOG, describe
+ its functionality as it appears to the user, and explain the design
+ issues and implementation techniques. REDLOG is available on the WWW.",
+ paper = "Dolz97b.pdf"
+}
+
+\end{chunk}
+
+\index{Calmet, Jacques}
+\index{Homann, Karsten}
+\begin{chunk}{axiom.bib}
+@book{Calm96,
+ author = "Calmet, Jacques and Homann, Karsten",
+ title = "Classification of Communication and Cooperation Mechanisms for
+ Logical and Symbolic Computation Systems",
+ booktitle = "Frontiers of Combining Systems",
+ publisher = "Kluwer Academic",
+ year = "1996",
+ pages = "221-234",
+ abstract =
+ "The combination of logical and symbolic computation systems has
+ recently emerged from prototype extensions of stand-alone systems to
+ the study of environments allowing interaction among several
+ systems. Communication and cooperation mechanisms of systems
+ performing any kind of mathematical service enable one to study and
+ solve new classes of problems and to perform efficient computation by
+ distributed specialized packages. The classification of communication
+ and cooperation methods for logical and symbolic computation systems
+ given in this paper provides and surveys different methodologies for
+ combining mathematical services and their characteristics,
+ capabilities, requirements, and differences. The methods are
+ illustrated by recent well-known examples. We separate the
+ classification into communication and cooperation methods. The former
+ includes all aspects of the physical connection, the flow of
+ mathematical information, the communication language(s) and its
+ encoding, encryption, and knowledge sharing. The latter concerns the
+ semantic aspects of architectures for cooperative problem solving.",
+ paper = "Calm96.pdf"
+}
+
+\end{chunk}
+
+\index{Dowek, Gilles}
+\begin{chunk}{axiom.bib}
+@article{Dowe00,
+ author = "Dowek, Gilles",
+ title = "Axioms vs Rewrite Rules: From Completeness to Cut Elimination",
+ journal = "Lecture Notes in Computer Science",
+ volume = "1794",
+ pages = "62-72",
+ year = "2000",
+ abstract =
+ "Combining a standard proof search method, such as resolution or
+ tableaux, and rewriting is a powerful way to cut off search space in
+ automated theorem proving, but proving the completeness of such
+ combined methods may be challenging. It may require in particular to
+ prove cut elimination for an extended notion of proof that combines
+ deductions and computations. This suggests new interactions between
+ automated theorem proving and proof theory.",
+ paper = "Dowe00.pdf"
+}
+
+\end{chunk}
+
+\index{Sorge, Volker}
+\begin{chunk}{axiom.bib}
+@article{Sorg00,
+ author = "Sorge, Volker",
+ title = "Non-trivial Symbolic Computations in Proof Planning",
+ journal = "LNCS",
+ volume = "1794",
+ pages = "121-135",
+ year = "2000",
+ abstract =
+ "We discuss a pragmatic approach to integrate computer algebra into
+ proof planning. It is based on the idea to separate computation and
+ verification and can thereby exploit the fact that many elaborate
+ symbolic computations are trivially checked. In proof planning the
+ separation is realized by using a powerful computer algebra system
+ during the planning process to do non-trivial symbolic
+ computations. Results of these computations are checked during the
+ refinement of a proof plan to a calculus level proof using a small,
+ self-implemented system that gives us protocol information on its
+ calculation. This protocol can be easily expanded into a checkable
+ low-level calculus proof ensuring the correctness of the
+ computation. We demonstrate our approach with the concrete
+ implementation in the $\Omega$MEGA system.",
+ paper = "Sorg00.pdf"
+}
+
+\end{chunk}
+
+\index{Melham, Thomas F.}
+\begin{chunk}{axiom.bib}
+@article{Melh02,
+ author = "Melham, Thomas F.",
+ title = "PROSPER An Investigation into Software Architecture for Embedded
+ Proof Engines",
+ journal = "LNCS",
+ volume = "2309",
+ pages = "193-206",
+ year = "2002",
+ abstract =
+ "Prosper is a recently-completed ESPRIT Framework IV research project
+ that investigated software architectures for component-based, embedded
+ formal verification tools. The aim of the project was to make
+ mechanized formal analysis more accessible in practice by providing a
+ framework for integrating formal proof tools inside other software
+ applications. This paper is an extended abstract of an invited
+ presentation on Prosper given at FroCoS 2002. It describes the vision
+ of the Prosper project and provides a summary of the technical
+ approach taken and some of the lessons learned.",
+ paper = "Melh02.pdf"
+}
+
+\end{chunk}
+
+\index{Adams, Andrew A.}
+\index{Gottlieben, Hanne}
+\index{Linton, Steve A.}
+\index{Martin, Ursula}
+\begin{chunk}{axiom.bib}
+@inproceedings{Adam99,
+ author = "Adams, Andrew A. and Gottlieben, Hanne and Linton, Steve A. and
+ Martin, Ursula",
+ title = "Automated theorem proving in support of computer algebra:
+ symbolic definite integration as a case study",
+ booktitle = "ISSAC '99",
+ pages = "253-260",
+ year = "1999",
+ abstract = "
+ 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.",
+ paper = "Adam99.pdf"
+
+\end{chunk}
+
+\index{Buchberger, B.}
+\index{Jebelean, Tudor}
+\index{Kriftner, Franz}
+\index{Vasaru, Daniela}
+\begin{chunk}{axiom.bib}
+@inproceedings{Buch77,
+ author = "Buchberger, B. and Jebelean, Tudor and Kriftner, Franz and
+ Vasaru, Daniela",
+ title = "A Survey on the Theorema Project",
+ booktitle = "ISSAC '97",
+ year = "1997",
+ abstract =
+ "The Theorema project aims at extending current computer algebra
+ systems by facilities for supporting mathematical proving. The present
+ early-prototype version of the Theorema software system is implemented
+ in Mathematica 3.0. The system consists of a general higher-order
+ predicate logic prover and a collection of special provers that call
+ each other depending on the particular proof situations. The
+ individual provers imitate the proof style of human mathematicians and
+ aim at producing human-readable proofs in natural language presented
+ in nested cells that facilitate studying the computer-generated proofs
+ at various levels of detail. The special provers are intimately
+ connected with the functors that build up the various mathematical
+ domains.",
+ paper = "Buch77.pdf"
+}
+
+\end{chunk}
+
+\index{Clarke, Edmund}
+\index{Zhao, Xudong}
+\begin{chunk}{axiom.bib}
+@techreport{Clar94,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Combining Symbolic Computation and Theorem Proving: Some
+ Problems of Ramanujan",
+ year = "1994",
+ type = "technical report",
+ institution = "Carnegie Mellon University",
+ number = "CMU-CS-94-103",
+ abstract =
+ "One way of building more powerful theorem provers is to use
+ techniques from symbolic computation. The challenge problems in this
+ paper are taken from Chapter 2 of Ramanujan''s Notebooks. They were
+ selected because they are non-trivial and require the use of symbolic
+ computation techniques. We have developed a theorem prover based on
+ the symbolic computation system Mathematica, that can prove all the
+ challenge problems completely automatically. The axioms and inference
+ rules for constructing the proofs are also briefly discussed.",
+ paper = "Clar94.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
+\index{de Bruijn, N.G.}
+\begin{chunk}{axiom.bib}
+@article{Brui94,
+ author = "de Bruijn, N.G.",
+ title = "A Survey on the project Automath",
+ journal = "Studies in Logic and the Foundations of Mathematics",
+ volume = "133",
+ year = "1994",
+ pages = "141-161",
+ abstract =
+ "Thus far, much about Automath has been written in separate
+ reports. Most of this work has been made available upon request, but
+ only a small part was published in journals, conference proceedings,
+ etc. Unfortunately, a general survey in the form of a book is still
+ lacking. A short survey was given in [de Bruijn 73c], but the present
+ one will be much more extensive. Naturally, this survey will report
+ about work that has been done, is going on, or is planned for the
+ future. But it will also be used to explain how various parts of the
+ project are related. Moreover we shall try to clarify a few points
+ which many outsiders consider as uncommon or even wierd. In particular
+ we spend quite some attention to our concept of types and the matter
+ of ``propositions as types'' (Section 14). Finally the survey will be
+ used to ventilate opinions and views in mathematics which are not
+ easily set down in more technical reports.",
+ paper = "Brui94.pdf"
+}
+
+\end{chunk}
+
+\index{Dutertre, Bruno}
+\begin{chunk}{axiom.bib}
+@article{Dute96,
+ author = "Dutertre, Bruno",
+ title = "Elements of Mathematical Analysis in PVS",
+ journal = "LNCS",
+ volume = "1125",
+ pages = "141-156",
+ year = "1996",
+ abstract =
+ "This paper presents the formalization of some elements of
+ mathematical analysis using the PVS verification system. Our main
+ motivation was to extend the existing PVS libraries and provide means
+ of modelling and reasoning about hybrid systems. The paper focuses on
+ several important aspects of PVS including recent extensions of the
+ type system and discusses their merits and effectiveness. We conclude
+ by a brief comparison with similar developments using other theorem
+ provers.",
+ paper = "Dute96.pdf"
+}
+
+\end{chunk}
+
+\index{Homann, Karsten}
+\index{Calmet, Jacques}
+\begin{chunk}{axiom.bib}
+@article{Homa94,
+ author = "Homann, Karsten and Calmet, Jacques",
+ title = "Combining Theorem Proving and Symbolic Mathematical Computing",
+ journal = "LNCS",
+ volume = "958",
+ pages = "18-29",
+ year = "1994",
+ abstract =
+ "An intelligent mathematical environment must enable symbolic
+ mathematical computation and sophisticated reasoning techniques on the
+ underlying mathematical laws. This paper disscusses different possible
+ levels of interaction between a symbolic calculator based on algebraic
+ algorithms and a theorem prover. A high level of interaction requires
+ a common knowledge representation of the mathematical knowledge of the
+ two systems. We describe a model for such a knowledge base mainly
+ consisting of type and algorithm schemata, algebraic algorithms and
+ theorems.",
+ paper = "Homa94.pdf",
+ keywords = "CAS-Proof"
+}
+
+\end{chunk}
+
+\index{Kredel, Heinz}
+\begin{chunk}{axiom.bib}
+@article{Kred90,
+ author = "Kredel, Heinz",
+ title = "MAS Modula-2 Algebra System",
+ journal = "LNCS",
+ volume = "429",
+ pages = "270-271",
+ year = "1990",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Fortenbacher, Albrecht}
+\begin{chunk}{axiom.bib}
+@article{Fort87,
+ author = "Fortenbacher, Albrecht",
+ title = "An Algebraic Approach to Unification Under Associativity and
+ Commutativity",
+ journal = "J. Symbolic Computation",
+ volume = "3",
+ pages = "217-229",
+ year = "1987",
+ abstract =
+ "From the work of Siekmann & Livesey, and Stickel it is known how to
+ unify two terms in an associative and commutative theory: transfer the
+ terms into Abelian strings, look for mappings which solve the problem
+ in the Abelian monoid, and decide whether a mapping can be regarded as
+ a unifier. Very often most of the mappings are thus eliminated, and
+ so it is crucial for efficiency either to not create these unnecessary
+ solutions or to remove them as soon as possible. The following work
+ formalises the transformations between the free algebra and this
+ monoid. This leads to an algorithm which uses maximal information for
+ its search for solutions in the monoid. It is both very efficient and
+ easily verifiable. Some applications of this algorithm are shown in
+ the appendix.",
+ paper = "Fort87.pdf"
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@book{ADAx83,
+ author = "U.S. Government",
+ title = "The Programming Language Ada Reference Manual",
+ publisher = "U.S. Government",
+ year = "1983",
+ comment = "STD-1815A-1983"
+}
+
+\end{chunk}
+
+\index{Ausiello, Giovanni Francesco Mascari}
+\begin{chunk}{axiom.bib}
+@article{Ausi79,
+ author = "Ausiello, Giovanni Francesco Mascari",
+ title = "On the Design of Algebraic Data Structures with the
+ Approach of Abstract Data Types",
+ journal = "LNCS",
+ volume = "72",
+ year = "1979",
+ pages = "514-530",
+ abstract =
+ "The problem of giving a formal definition of the representation of
+ algebraic data structures is considered and developped in the frame
+ work of the abstract data types approach. Such concepts as canonical
+ form and simplification are formalized and related to properties of
+ the abstract specification and of the associated term rewriting
+ system.",
+ paper = "Ausi79.pdf"
+}
+
+\end{chunk}
+
+\index{Burstall, R.M.}
+\index{Goguen, J.A.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Burs77,
+ author = "Burstall, R.M. and Goguen, J.A.",
+ title = "Putting THeories together to make Specifications",
+ booktitle = "IJCAI 77 Volume 2",
+ pages = "1045-1058",
+ year = "1977",
+ paper = "Burs77.pdf"
+}
+
+\end{chunk}
+
+\index{Cohn, Paul Moritz}
+\begin{chunk}{axiom.bib}
+@book{Cohn65,
+ author = "Cohn, Paul Moritz",
+ title = "Universal Algebra",
+ publisher = "Harper and Row",
+ year = "1965"
+}
+
+\end{chunk}
+
+\index{Davenport, J.H.}
+\index{Jenks, R.D.}
+\begin{chunk}{axiom.bib}
+@misc{Dave80b,
+ author = "Davenport, J.H. and Jenks, R.D.",
+ title = "SCRATCHPAD/370: Modes and Domains",
+ year = "1980",
+ comment = "private communication"
+}
+
+\end{chunk}
+
+\index{Demers, A.}
+\index{Donahue, J.}
+\begin{chunk}{axiom.bib}
+@techreport{Deme79,
+ author = "Demers, A. and Donahue, J.",
+ title = "Revised Report on RUSSELL",
+ year = "1979",
+ type = "technical report",
+ institution = "Cornell",
+ number = "TR 79-389"
+}
+
+\end{chunk}
+
+\index{Griss, Martin L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gris76,
+ author = "Griss, Martin L.",
+ title = "The Definition and Use of Data Structures in REDUCE",
+ booktitle = "SYMSAC '76",
+ pages = "53-59",
+ year = "1976",
+ abstract =
+ "This paper gives a brief description and motivation of the mode
+ analyzing and data-structuring extensions to the algebraic language
+ REDUCE. These include generic functions, user defined recursive data
+ structures, mode transfer functions and user modifiable automatic
+ coercion. A number of examples are given to illustrate the style and
+ features of the language, and how it will aid in the construction of
+ more efficient and reliable programs."
+}
+
+\end{chunk}
+
+\index{Loos, Ruediger G. K.}
+\begin{chunk}{axiom.bib}
+@article{Loos74,
+ author = "Loos, Ruediger G. K.",
+ title = "Toward a Formal Implementation of Computer Algebra",
+ journal = "SIGSAM",
+ volume = "8",
+ number = "3",
+ pages = "9-16",
+ year = "1974",
+ abstract =
+ "We consider in this paper the task of synthesizing an algebraic
+ system. Today the task is significantly simpler than in the pioneer
+ days of symbol manipulation, mainly because of the work done by the
+ pioneers in our area, but also because of the progress in other areas
+ of Computer Science. There is now a considerable collection of
+ algebraic algorithms at hand and a much better understanding of data
+ structures and programming constructs than only a few years ago.",
+ paper = "Loos74.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Levenworth, B.}
+\begin{chunk}{axiom.bib}
+@misc{Leve80,
+ author = "Levenworth, B.",
+ title = "ADAPT Reference Manual",
+ comment = "IBM Research",
+ year = "1980"
+}
+
+\end{chunk}
+
+
+\index{Wegbreit, Ben}
+\begin{chunk}{axiom.bib}
+@article{Wegb74,
+ author = "Wegbreit, Ben",
+ title = "The Treatment of Data Types in EL1",
+ journal = "Communications of the ACM",
+ volume = "17",
+ number = "5",
+ year = "1974",
+ pages = "251-264",
+ abstract =
+ "In constructing a general purpose programming language, a key issue
+ is providing a sufficient set of data types and associated operations
+ in a manner that permits both natural problem-oriented notation and
+ efficient implementation. The EL1 language contains a number of
+ features specifically designed to simultaneously satisfy both
+ requirements. The resulting treatment of data types includes provision
+ for programmer-defined data types and generaic routines, programmer
+ control over type conversion, and very flexible data type behavior, in
+ a context that allows efficient compiled code and compact data
+ representation.",
+ paper = "Wegb74.pdf"
+}
+
+\end{chunk}
+
+\index{Wulf, William A.}
+\index{London, Ralph L.}
+\index{Shaw, Mary}
+\begin{chunk}{axiom.bib}
+@article{Wulf76,
+ author = "Wulf, William A. and London, Ralph L. and Shaw, Mary",
+ title = "An Introduction to the Construction and Verification of
+ Alphard Programs",
+ journal = "IEEE Tr. Software Engineering",
+ volume = "SE-2",
+ number = "4",
+ year = "1976",
+ pages = "253-265",
+ abstract =
+ "The programming language Alphard is designed to provide support for
+ both the methodologies of ``well-structured'' programming and the
+ techniques of formal program verification. Language constructs allow
+ a programmer to isolate an abstraction, specifying its behavior
+ publicly while localizing. knowledge about its implementation. The
+ verification of such an abstraction consists of showing that its
+ implementation behaves in accordance with its public specifications;
+ the abstraction can then be used with confidence in constructing
+ other programs, and the verification of that use employs only the
+ public specifications. This paper introduces Alphard by developing
+ and verifying a data structure definition and a program that uses it.
+ It shows how each language construct contributes to the development of
+ the abstraction and discusses the way the language design and the
+ verification methodology wete tailored to each other. It serves not
+ only as an introduction to Alphard, but also as an example of the
+ symbiosis between verification and methodology in language design.
+ The strategy of program structuring, illustrated for Alphard, is
+ also applicable to most of the "data abstraction" mechanisms now
+ appearing.",
+ paper = "Wulf76.pdf"
+}
+
+\end{chunk}
+
+\index{Astesiano, Egidio}
+\index{Bidoit, Michel}
+\index{Kirchner, Helene}
+\index{Krieg-Bruckner, Bernd}
+\index{Mosses, Peter D.}
+\index{Sannella, Donald}
+\index{Tarlecki, Andrzej}
+\begin{chunk}{axiom.bib}
+@article{Aste02,
+ author = "Astesiano, Egidio and Bidoit, Michel and Kirchner, Helene and
+ Krieg-Bruckner, Bernd and Mosses, Peter D. and Sannella, Donald
+ and Tarlecki, Andrzej",
+ title = "CASL: the Common Algebraic Specification Language",
+ journal = "Theoretical Computer Science",
+ volume = "286",
+ number = "2",
+ pages = "153-196",
+ year = "2002",
+ abstract =
+ "The Common Algebraic Specification Language (CASL) is an expressive
+ language for the formal specification of functional requirements and
+ modular design of software. It has been designed by COFI, the
+ international Common Framework Initiative for algebraic specification
+ and development. It is based on a critical selection of features that
+ have already been explored in various contexts, including subsorts,
+ partial functions, first-order logic, and structured and architectural
+ specifications. CASL should facilitate interoperability of many
+ existing algebraic prototyping and verification tools.
+
+ This paper gives an overview of the CASL design. The major issues that
+ had to be resolved in the design process are indicated, and all the
+ main concepts and constructs of CASL are briefly explained and
+ illustrated — the reader is referred to the CASL Language Summary for
+ further details. Some familiarity with the fundamental concepts of
+ algebraic specification would be advantageous.",
+ paper = "Aste02.pdf"
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
+@article{Dave90a,
+ author = "Davenport, James H.",
+ title = "Current Problems in Computer Algebra Systems Design",
+ journal = "LNCS",
+ volume = "429",
+ year = "1990",
+ pages = "1-9",
+ abstract =
+ "Computer Algebra systems have been with us for over twenty years, but
+ there is still no consensus on what an ``ideal'' system would look
+ like. There are all sorts of tradeoffs between portability,
+ functionality, and efficiency. This paper discusses some of those issues.",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Galligo, A.}
+\index{Grimm, J.}
+\index{Pottier, L.}
+\begin{chunk}{axiom.bib}
+@article{Gall90,
+ author = "Galligo, A. and Grimm, J. and Pottier, L.",
+ title = "The Design of SISYPHE: A System for doing Symbolic and
+ Algebraic Computations",
+ journal = "LNCS",
+ volume = "429"
+ pages = "30-39",
+ year = "1990"
+ keywords = "axiomref"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 39343b0..4b16aec 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5818,6 +5818,8 @@ books/bookvolbib add Doye references

books/bookvolbib add Computer Algebra - Proof references

20170902.01.tpd.patch
src/axiom-website/documentation.html add Caviness quote

+20170905.01.tpd.patch
+books/bookvol3 Additional explanations and references

--
1.9.1