From b31a39e530c70119464299f854c759707c1bcd6a Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 16 Oct 2017 09:28:33 0400
Subject: [PATCH] books/bookvolbib Proving Axiom Correct references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Berndt, B.C.}
\begin{chunk}{axiom.bib}
@misc{Bern85,
author = "Berndt, B.C.",
title = "Ramanujan's Notebooks, Part I",
publisher = "SpringerVerlag",
year = "1985",
pages = "2543"
}
\end{chunk}
\index{London, Ralph L.}
\index{Musser, David R.}
\begin{chunk}{axiom.bib}
@misc{Lond74,
author = "London, Ralph L. and Musser, David R.",
title = "The Application of a Symbolic Mathematical System to Program
Verification",
publisher = "USC Information Sciences Institute",
year = "1974",
abstract =
"Program verification is a relatively new application area for
symbolic mathematical systems. We report on an interactive
program verification system, based on the inductive assertion method,
which system is implemented using an existing symbolic mathematical
language and supporting system, Reduce. Reduce has been augmented
with a number of capabilities which are important to program
verification, particularly transformations on relational and Boolean
expressions. We believe these capabilities would be valuable in other
contexts and should be incorporated more widely into symbolic
mathematical systems for general use. The program verification
application can serve as a guide to an appropriate definition of
such capabilities, particularly with regard to the need to distinguish
between undefined program variables and polynomial indeterminates.
Additional capabilities which would benefit the program verification
application include representation of userdefined functions by
internal forms which directly incorporate properties such as
commutativity and associativity (as is commonly done with plus and
times), and a comprehensive facility for defining conditionally
applicable transformations.",
paper = "Lond74.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Suppes, Patrick}
\index{Takahashi, Shuzo}
\begin{chunk}{axiom.bib}
@article{Supp89,
author = "Suppes, Patrick and Takahashi, Shuzo",
title = "An Interactive Calculus TheoremProver for Continuity Properties",
journal = "J. Symbolic Computation",
volume = "7",
number = "6",
pages = "573590",
year = "1989",
abstract =
"The work reported concerns the development of an interactive
theoremprover for the foundationsof the differential and integral
calculus. The main tools are a resolution theoremprover VERIFY,
previously developed for interactive proofs in set theory, and the
symbolic computation program REDUCE. The use of REDUCE in a
theoremproving context is described in detail. Sample proofs are
given with data on computation time per step on an IBM4381.",
paper = "Supp89.pdf"
}
\end{chunk}
\index{Walsh, Toby}
\index{Nunes, Alex}
\index{Bundy, Alan}
\begin{chunk}{axiom.bib}
@misc{Wals92,
author = "Walsh, Toby and Nunes, Alex and Bundy, Alan",
title = "The Use of Proof Plans to Sum Series",
booktitle = "Proc. of 11th Int. Conf. on Automated Deduction",
year = "1992",
abstract =
"We describe a program for finding closed form solutions to finite
sums. The program was built to test the applicability of the proof
planning search control technique in a domain of mathematics outwith
induction. This experiment was successful. The series summing program
extends previous work in this area and was built in a short time just
by providing new series summing methods to our existing inductive
theorem proving system CLAM.
One surprising discovery was the
usefulness of the ripple tactic in summing series. Rippling is the key
tactic for controlling inductive proofs, and was previously thought to
be specialised to such proofs. However, it turns out to be the key
subtactic used by all the main tactics for summing series. The only
change required was that it had to be supplemented by a difference
matching algorithm to set up some initial metalevel annotations to
guide the rippling process. In inductive proofs these annotations are
provided by the application of mathematical induction. This evidence
suggests that rippling, supplemented by difference matching, will find
wide application in controlling mathematical proofs. The research
reported in this paper was supported by SERC grant GR/F/71799, a SERC
PostDoctoral Fellowship to the first author and a SERC Senior
Fellowship to the third author. We would like to thank the other
members of the mathematical reasoning group for their feedback on this
project.",
paper = "Wals92.pdf"
}
\end{chunk}
\index{Blair, Fred W.}
\index{Griesmer, James H.}
\index{Jenks, Richard D.}
\begin{chunk}{axiom.bib}
@article{Blai70a,
author = "Blair, Fred W. and Griesmer, James H. and Jenks, Richard D.",
title = "An interactive facility for symbolic mathematics",
journal = "ACM SIGSAM",
volume = "14",
year = "1970",
pages = "1718",
abstract =
"This paper describes a system designed to provide an interactive
symbolic computational facility for the mathematician user. To carry
out this objective, an experimental LISP system has been implemented
for IBM System/360 computers. Using this LISP system as a base,
portions of several systems have been combined and augmented to
provide the following facilities to a user:(1) rational function
manipulation and simplification; symbolic differentiation (Anthony
Hearn's REDUCE)(2) symbolic integration (Joel Moses' SIN)(3)
polynomial factorization, solution of linear differential equations,
direct and inverse symbolic Laplace transforms (Carl Engelman's
MATHLAB, including Knut Korsvold's simplification system)(4) unlimited
precision integer arithmetic(5) manipulation of arrays containing
symbolic entries(6) twodimensional output on IBM 2741 terminals or
IBM 2250 displays (William Martin's Symbolic Mathematical Laboratory,
and Jonathan Millen's CHARYBDIS program from MATHLAB)(7)
selfextending language facility (META/LISP).The user language created
for the system incorporates a subset of "customary" mathematical
notation. Data objects include sequences (both finite and infinite)
and arrays of arbitrary rank. Assignment statements are the
fundamental commands in the user language; they may contain
"for"clauses which restrict the domain for which the assignment is
valid and permit "piecewise" and recursive definition of new operators
and functions. The user may also enter syntax definition statements in
order to introduce new notations into the system.Expressions appearing
in assignment statements may include "where"clauses which allow user
control over the "environment" used in evaluation. Otherwise,
evaluation of expressions occurs in the current environment created by
the successive user commands, with certain operations such as
integration, differentiation, and simplification performed
automatically.Translators for the user language and for a resident
higherlevel procedural language facility are written in META/LISP, a
new selfcompiling translatorwriting system. As a result, all input
language facilities as well as the underlying manipulation routines
may be interactively extended by an experienced user.",
paper = "Blai70a.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Sturmfels, B.}
\begin{chunk}{axiom.bib}
@book{Stur93,
author = "Sturmfels, B.",
title = "Algorithms in Invariant Theory",
year = "1993",
publisher = "Springer"
}
\end{chunk}
\index{Wu, Wentsun}
\begin{chunk}{axiom.bib}
@book{Wuxx94,
author = "Wu, Wentsun",
title = "Mechanical Theorem Proving in Geometries",
isbn = "9783709166390",
publisher = "Springer",
year = "1994"
}
\end{chunk}
\index{Buchberger, B.}
\index{Lichtenberger, F.}
\begin{chunk}{axiom.bib}
@book{Buch81,
author = "Buchberger, B. and Lichtenberger, F.",
title = "Mathematics for Computer Science I  The Method of Mathematics",
publisher = "Springer",
year = "1981",
comment = "German"
}
\end{chunk}
\index{Clarke, Edmund}
\index{Zhao, Xudong}
\begin{chunk}{axiom.bib}
@article{Clar93,
author = "Clarke, Edmund and Zhao, Xudong",
title = "Analytica  A Theorem Prover for Mathematica",
journal = "The Mathematica Journal",
volume = "3",
number = "1",
year = "1993",
pages = "761765",
abstract =
"Analytica is an automatic theorem prover for theorems in
elementary analysis. The prover is written in 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 guarantee the
correctness of certain steps that are made by the symbolic
computation system and therefore prevent common errors like
division by a symbolic expression that could be zero. In this
paper we describe the structure of Analytica and explain the main
techniques that it uses to construct proofs. We have tried to make
the paper as selfcontained as possible so that it will be
accessible to a wide audience of potential users. We illustrate
the power of our theorem prover by several nontrivial examples
including the basic properties of the stereographic projection and
a series of three lemmas that lead to a proof of Weierstrass's
example of a continuous nowhere differentiable function. Each of
the lemmas in the latter example is proved completely
automatically."
}
\end{chunk}
\index{Dolzmann, A.}
\index{Seidl, A.}
\index{Sturm, T.}
\begin{chunk}{axiom.bib}
@misc{Dolz04,
author = "Dolzmann, A. and Seidl, A. and Sturm, T.",
title = "Redlog User Manual",
year = "2004",
comment = "Edition 3.0",
link = "\url{http://www.reducealgebra.com/reduce38docs/redlog.pdf}",
paper = "Dolz04.pdf"
}
\end{chunk}
\index{Van Hamelen, Frank}
\begin{chunk}{axiom.bib}
@misc{Hame89,
author = "Van Hamelen, Frank",
title = "The CLAM Proof Planner",
year = "1989",
publisher = "Dept. of AI, Univ. of Edinburgh"
}
\end{chunk}
\index{Gordon, Mike J.C.}
\index{Melham, T.F.}
\begin{chunk}{axiom.bib}
@book{Gord93,
author = "Gordon, Mike J.C. and Melham, T.F.",
title = "Introduction to HOL: A Theorem Proving Environment for Higher
Order Logic",
link = "\url{http://www.cs.ox.ac.uk/tom.melham/pub/Gordon1993ITH.html}",
publisher = "Cambridge University Press",
year = "1993",
isbn = "0521441897"
}
\end{chunk}
\index{Constable, R.L.}
\index{Allen, S.F.}
\index{Bromley, H.M.}
\index{Cremer, J.F.}
\index{Harper, R.W.}
\index{Howe, D.J.}
\index{Knoblock, T.B.}
\index{Mendler, N.P.}
\index{Panagaden, P.}
\index{Tsaaki, J.T.}
\index{Smith, S.F.}
\begin{chunk}{axiom.bib}
@book{Cons85,
author = "Constable, R.L. and Allen, S.F. and Bromley, H.M. and Cremer, J.F.
and Harper, R.W. and Howe, D.J. and Knoblock, T.B. and
Mendler, N.P. and Panagaden, P. and Tsaaki, J.T. and Smith, S.F.",
title = "Implementing Mathematics with The Nuprl Proof Development System",
publisher = "PrenticeHall",
year = "1985"
}
\end{chunk}
\index{Boyer, R.S.}
\index{Moore, J.S.}
\begin{chunk}{axiom.bib}
@book{Boye88,
author = "Boyer, R.S. and Moore, J.S.",
title = "A Computational Logic Handbook",
publisher = "Academic Press",
year = "1988"
}
\end{chunk}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@misc{Paul98,
author = "Paulson, Lawrence C.",
title = "Introduction to Isabelle",
publisher = "Computer Laboratory, Univ. of Cambridge",
year = "1998"
}
\end{chunk}
\index{Seger, C.}
\incdex{Joyce, J.J.}
\begin{chunk}{axiom.bib}
@techreport{Sege91,
author = "Seger, C. and Joyce, J.J.",
title = "A Twolevel Formal Verification Methodology using HOL and COSMOS",
type = "technical report",
year = "1991",
number = "9110",
institution = "Dept. of Comp. Sci. Univ. of British Columbia",
abstract =
"Theoremproving and symbolic simulation are both described as methods
for the formal verification of hardware. They are both used to achieve
a common goal  correctly designed hardware  and both are intended
to be an alternative to conventional methods based on nonexhaustive
simulation. However, they have different strengths and weaknesses. The
main significance of this paper  and its most original contribution
 is the suggestion that symbolic simulation and theoremproving can
be combined in a complementary manner. We also outline our plans for
the development of a mathematical interface between the two approaches
 in particular, a semantic link between the formulation of
higherorder logic used in the Cambridge HOL system and the
specification language used in the COSMOS system. We believe that this
combination offers great potential as a practical formal verification
methodology which combines the ability to accurately model circuit
level behavior with the ability to reason about digital hardware at
higher levels of abstraction"
}
\end{chunk}
\index{Backus, John}
\begin{chunk}{axiom.bib}
@techreport{Back73,
author = "Backus, John",
title = "Programming Language Semantics and Closed Applicative Language",
type = "technical report",
institution = "IBM",
number = "RJ 1245",
year = "1973"
}
\end{chunk}
\index{Howe, Douglas J.}
\begin{chunk}{axiom.bib}
@article{Howe88,
author = "Howe, Douglas J.",
title = "Computational Metatheory in Nuprl",
journal = "LNCS",
volume = "310",
pages = "238257",
year = "1988",
publisher = "SpringerVerlag",
abstract =
"This paper describes an implementation within Nuprl of mechanisms
that support the use of Nuprl's type theory as a language for
constructing theoremprovind procedures. The main componenet of the
implementation is a large library of definitions, theorems and
proofs. This library may be regarded as the beginning of a book of
formal mathematics; it contains the formal development and explanation
of a useful subset of Nuprl's metatheory, and of a mechanism for
translating results established about this embedded metatheory to the
object level. Nuprl's rich type theory, besides permitting the
internal development of this partial reflection mechanism, allows us
to make abstractions that drastically reduce the burden of
establishing the correctness of new theoremproving procedures. Our
library includes a formally verified termrewriting system"
}
\end{chunk}
\index{Pelletier, Francis Jeffry}
\begin{chunk}{axiom.bib}
@inproceedings{Pell91,
author = "Pelletier, Francis Jeffry",
title = "The Philosophy of Automated Theorem Proving",
booktitle = "Proc 12th IJCAI",
pages = "538543",
year = "1991",
publisher = "Morgan Kaufmann",
paper = "Pell91.pdf"
}
\end{chunk}
\index{Smith, Brian Cantwell}
\begin{chunk}{axiom.bib}
@misc{Smit60,
author = "Smith, Brian Cantwell",
title = "The Limits of Correctness",
year = "1960",
link = "\url{http://eliza.newhaven.edu/ethics/Resources/14.ReliabilityResponsibility/LimitsOfCorrectness.pdf}",
paper = "Smit60.pdf"
}
\end{chunk}
\index{Naumowicz, Adam}
\begin{chunk}{axiom.bib}
@article{Naum06,
author = "Naumowicz, Adam",
title = "An Example of Formalizing Recent Mathematical Results in Mizar",
journal = "Journal of Applied Logic",
volume = "4",
number = "4",
year = "2006",
pages = "396413",
abstract =
"This paper describes an example of the successful formalization of
quite advanced and new mathematics using the Mizar system. It shows
that although much effort is required to formalize nontrivial facts in
a formal computer deduction system, still it is possible to obtain the
level of full logical correctness of all inference steps. We also
discuss some problems encountered during the formalization, and try to
point out some of the features of the Mizar system responsible for
that. The formalization described in this paper allows also for
contrasting the linguistic capability of the Mizar language and some
of the phrases commonly used in “informal” mathematical papers that
the Mizar system lacks, and consequently presents the methods of how
to cope with it during the formalization. Yet, apart from the
problems, this paper shows some definite benefits from using a formal
computer system in the work of a mathematician.",
paper = "Naum06.pdf"
}
\end{chunk}
\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
@misc{Wied07,
author = "Wiedijk, Freek",
title = "The Seventeen Provers of the World",
link = "\url{http://www.cs.kun.nl/~freek/comparison/comparison.pdf}",
year = "2007",
abstract =
"We compare the styles of several proof assistants for mathematics.
We present Pythagoras' proof of the irrationality of $\sqrt{2}$ both
informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq,
(5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX,
(10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl,
(15) $\Omega$mega, (16) B method, (17) Minlog",
paper = "Wied07.pdf"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{QED94,
author = "Anonymous",
title = "The QED Manifesto",
link = "\url{}",
paper = "QED94.txt"
}
\end{chunk}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@book{Paul94,
author = "Paulson, Lawrence C.",
title = "ISABELLE: A Generic Theorem Prover",
year = "1994",
publisher = "Springer",
isbn = "9783540582441",
}
\end{chunk}
\index{Cannon, John}
\index{Bosma, Wieb}
\begin{chunk}{axiom.bib}
@book{Cann05,
author = "Cannon, John and Bosma, Wieb",
title = "Handbook of Magma Functions",
year = "2005",
publisher = "University of Sydney, School of Math and Statistics"
}
\end{chunk}
\index{Kajler, Norbert}
\index{Soiffer, Neil}
\begin{chunk}{axiom.bib}
@article{Kajl98,
author = "Kajler, Norbert and Soiffer, Neil",
title = "A Survey of User Interfaces for Computer Algebra Systems",
journal = "J. Symbolic Computation",
volume = "25",
pages = "127159",
year = "1998",
abstract =
"This paper surveys work within the Computer Algebra community (and
elsewhere) directed towards improving user interfaces for scientific
computation during the period 19631994. It is intended to be useful
to two groups of people: those who wish to know what work has been
done and those who would like to do work in the field. It contains an
extensive bibliography to assist readers in exploring the field in more
depth. Work related to improving human interaction with computer
algebra systems is the main focus of the paper. However, the paper
includes additional materials on some closely related issues such as
structured document editing, graphics, and communication protocols.",
paper = "Kajl98.pdf"
}
\end{chunk}

books/axiom.bib  514 ++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  685 ++++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  586 +++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1664 insertions(+), 125 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 1e977b3..dff8562 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 2090,6 +2090,13 @@ paper = "Brea89.pdf"
year = "1985"
}
+@misc{QED94,
+ author = "Anonymous",
+ title = "The QED Manifesto",
+ link = "\url{}",
+ paper = "QED94.txt"
+}
+
@InCollection{Rect89,
author = "Rector, D. L.",
title = "Semantics in Algebraic Computation",
@@ 6869,6 +6876,15 @@ paper = "Brea89.pdf"
paper = "Aker93.pdf"
}
+@inproceedings{Arch93,
+ author = "Archer, M. and Fink, G. and Yang, L.",
+ title = "Linking Other Theorem Provers to HOL Using PM: Proof Manager",
+ booktitle = "Int Workshop on the HOL Theorem Proving System and its
+ Applications",
+ publisher = "NorthHolland",
+ year = "1993"
+}
+
@article{Avig12a,
author = "Avigad, Jeremy",
title = "Type Inference in Mathematics",
@@ 6915,6 +6931,15 @@ paper = "Brea89.pdf"
paper = "Avig17.pdf"
}
+@techreport{Back73,
+ author = "Backus, John",
+ title = "Programming Language Semantics and Closed Applicative Language",
+ type = "technical report",
+ institution = "IBM",
+ number = "RJ 1245",
+ year = "1973"
+}
+
@inproceedings{Ball95,
author = "Ballarin, Clemens and Homann, Karsten and Calmet, Jacques",
title = "Theorems and Algorithms: An Interface between Isabelle and Maple",
@@ 7406,6 +7431,20 @@ paper = "Brea89.pdf"
paper = "Bove08.pdf"
}
+@misc{Boye81,
+ author = "Boyer, Bob and Kaufmann, Matt and Moore, J",
+ title = "Metafunctions in Nqthm and Acl2",
+ link = "\url{https://www.cs.utexas.edu/users/boyer/metanqthmacl2.text}",
+ year = "1981"
+}
+
+@book{Boye88,
+ author = "Boyer, R.S. and Moore, J.S.",
+ title = "A Computational Logic Handbook",
+ publisher = "Academic Press",
+ year = "1988"
+}
+
@book{Brad07,
author = "Bradley, Aaron R. and Manna, Zohar",
title = "The Calculus of Computation",
@@ 7551,6 +7590,17 @@ paper = "Brea89.pdf"
paper = "Bund88.pdf"
}
+@article{Bund90,
+ author = "Bundy, Alan and van Harmelen, Frank and Horn, Christian and
+ Smaill, Alan",
+ title = "The OysterClam System",
+ journal = "Lecture Notes in Artificial Intelligence",
+ volume = "449",
+ year = "1990",
+ pages = "647648",
+ paper = "Bund90.pdf"
+}
+
@article{Bund93b,
author = "Bundy, Alan and Stevens, Andrew and van Hemelen, Frank and
Ireland, Andrew and Smaill, Alan",
@@ 7570,7 +7620,8 @@ paper = "Brea89.pdf"
which embodies these extensions as special cases. We prove that
generalised rippling always terminates, and we discuss the
implementation of the tactic and its relation with other inductive
 proof search heuristics."
+ proof search heuristics.",
+ paper = "Bund93b.pdf"
}
@misc{Byrd17,
@@ 7580,6 +7631,13 @@ paper = "Brea89.pdf"
comment = "See miniKanren and Barliman (program synthesis with proof)"
}
+@book{Cann05,
+ author = "Cannon, John and Bosma, Wieb",
+ title = "Handbook of Magma Functions",
+ year = "2005",
+ publisher = "University of Sydney, School of Math and Statistics"
+}
+
@misc{Cast16,
author = "Casteran, Pierre and Sozeau, Mattieu",
title = "A Gentle Introduction to Type Classses and Relations in Coq",
@@ 7673,6 +7731,36 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@article{Clar93,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Analytica  A Theorem Prover for Mathematica",
+ journal = "The Mathematica Journal",
+ volume = "3",
+ number = "1",
+ year = "1993",
+ pages = "761765",
+ abstract =
+ "Analytica is an automatic theorem prover for theorems in
+ elementary analysis. The prover is written in 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 guarantee the
+ correctness of certain steps that are made by the symbolic
+ computation system and therefore prevent common errors like
+ division by a symbolic expression that could be zero. In this
+ paper we describe the structure of Analytica and explain the main
+ techniques that it uses to construct proofs. We have tried to make
+ the paper as selfcontained as possible so that it will be
+ accessible to a wide audience of potential users. We illustrate
+ the power of our theorem prover by several nontrivial examples
+ including the basic properties of the stereographic projection and
+ a series of three lemmas that lead to a proof of Weierstrass's
+ example of a continuous nowhere differentiable function. Each of
+ the lemmas in the latter example is proved completely
+ automatically."
+}
+
@article{Como88,
author = "Comon, H. and Lugiez, D. and Schnoebelen, P.H.",
title = "A Rewritebased Type Discipline for a Subset of Computer Algebra",
@@ 7696,6 +7784,15 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@book{Cons85,
+ author = "Constable, R.L. and Allen, S.F. and Bromley, H.M. and Cremer, J.F.
+ and Harper, R.W. and Howe, D.J. and Knoblock, T.B. and
+ Mendler, N.P. and Panagaden, P. and Tsaaki, J.T. and Smith, S.F.",
+ title = "Implementing Mathematics with The Nuprl Proof Development System",
+ publisher = "PrenticeHall",
+ year = "1985"
+}
+
@techreport{Coqu86,
author = {Coquand, Thierry and Huet, G\'erard},
title = "The Calculus of Constructions",
@@ 7918,6 +8015,15 @@ paper = "Brea89.pdf"
isbn = "9780387904412"
}
+@misc{Dolz04a,
+ author = "Dolzmann, A. and Seidl, A. and Sturm, T.",
+ title = "Redlog User Manual",
+ year = "2004",
+ comment = "Edition 3.0",
+ link = "\url{http://www.reducealgebra.com/reduce38docs/redlog.pdf}",
+ paper = "Dolz04a.pdf"
+}
+
@inproceedings{Dybj90,
author = "Dybjer, Peter",
title = {Inductive Sets and Families in MarinL\"of's Type Theory and
@@ 8157,6 +8263,13 @@ paper = "Brea89.pdf"
isbn = "9780262062794"
}
+@book{Gedd94,
+ author = "Geddes, D.",
+ title = "The DTP Manual",
+ publisher = "Stanford University",
+ year = "1994"
+}
+
@misc{Gent35,
author = "Gentzen, Gerhard",
title = "Investigations into Logical Deduction",
@@ 8285,14 +8398,6 @@ paper = "Brea89.pdf"
paper = "Gogu82.pdf",
}
@misc{Gord96,
 author = "Gordon, Mike",
 title = "From LCF to HOL: a short history",
 year = "1996",
 link = "\url{http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf}",
 paper = "Gord96.pdf"
}

@article{Gogu06,
author = "Goguen, Healfdene and McBride, Conor and McKinna, James",
title = "Eliminating Dependent Pattern Matching",
@@ 8313,6 +8418,24 @@ paper = "Brea89.pdf"
paper = "Gogu06.pdf"
}
+@misc{Gord96,
+ author = "Gordon, Mike",
+ title = "From LCF to HOL: a short history",
+ year = "1996",
+ link = "\url{http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf}",
+ paper = "Gord96.pdf"
+}
+
+@book{Gord93,
+ author = "Gordon, Mike J.C. and Melham, T.F.",
+ title = "Introduction to HOL: A Theorem Proving Environment for Higher
+ Order Logic",
+ link = "\url{http://www.cs.ox.ac.uk/tom.melham/pub/Gordon1993ITH.html}",
+ publisher = "Cambridge University Press",
+ year = "1993",
+ isbn = "0521441897"
+}
+
@article{Gott05,
author = "Gottliebsen, Hanne and Kelsey, Tom and Martin, Ursula",
title = "Hidden verification for computational mathematics",
@@ 8377,6 +8500,13 @@ paper = "Brea89.pdf"
isbn = "3540940065"
}
+@misc{Hame89,
+ author = "Van Hamelen, Frank",
+ title = "The CLAM Proof Planner",
+ year = "1989",
+ publisher = "Dept. of AI, Univ. of Edinburgh"
+}
+
@misc{Hard13,
author = "Hardin, David S. and McClurg, Jedidiah R. and Davis, Jennifer A.",
title = "Creating Formally Verified Components for Layered Assurance
@@ 8520,6 +8650,30 @@ paper = "Brea89.pdf"
paper = "Howa80.pdf"
}
+@article{Howe88,
+ author = "Howe, Douglas J.",
+ title = "Computational Metatheory in Nuprl",
+ journal = "LNCS",
+ volume = "310",
+ pages = "238257",
+ year = "1988",
+ publisher = "SpringerVerlag",
+ abstract =
+ "This paper describes an implementation within Nuprl of mechanisms
+ that support the use of Nuprl's type theory as a language for
+ constructing theoremprovind procedures. The main componenet of the
+ implementation is a large library of definitions, theorems and
+ proofs. This library may be regarded as the beginning of a book of
+ formal mathematics; it contains the formal development and explanation
+ of a useful subset of Nuprl's metatheory, and of a mechanism for
+ translating results established about this embedded metatheory to the
+ object level. Nuprl's rich type theory, besides permitting the
+ internal development of this partial reflection mechanism, allows us
+ to make abstractions that drastically reduce the burden of
+ establishing the correctness of new theoremproving procedures. Our
+ library includes a formally verified termrewriting system"
+}
+
@inproceedings{Huet87,
author = {Huet, G\'erard},
title = "Induction Principles Formalized in the Calculus of Constructions",
@@ 8900,6 +9054,62 @@ paper = "Brea89.pdf"
paper = "Kell12.pdf"
}
+@inproceeding{Kuma91,
+ author = "Kumar, Ramayya and Kropf, Thomas and Schneider, Klaus",
+ title = "Integrating a FirstOrder Automatic Prover in the HOL Environment",
+ booktitle = "Int. Workshop on the HOL Theorem Prover System and its
+ Applications",
+ publisher = "IEEE Computer Society Press",
+ year = "1991",
+ abstract =
+ "The HOL system is a powerful tool for proving higher order formulae.
+ However, proofs have to be performed interactively and only little
+ automation using tactics is possible. Even though interaction is
+ desirable to guide major and creative backward proof steps of complex
+ proofs, a deluge of simple subgoals may evolve which all have to be
+ proven manually in order to accomplish the proof. Although these
+ subgoals are often simple formulae, their proof has not yet been
+ automated in HOL.
+
+ In this paper it is shown how it is possible to
+ automate these tasks by integrating a firstorder automated theorem
+ proving tool, called FAUST, into HOL. It is based on an efficient
+ variant of the wellknown sequent calculus. In order to maintain the
+ high confdence in HOLgenerated proofs, FAUST is able to generate HOL
+ tactics which may be used to postjustifr the theorem derived by FAUST
+ in HOL. The underlying calculus of FAUST, the tactic generation, as
+ well as experimental results are presented.",
+ paper = "Kuma91.pdf"
+}
+
+@article{Kutz86,
+ author = "Kutzler, B. and Stifter, S.",
+ title = "On the application of Buchberger's algorithm to automated
+ geometry theorem proving",
+ journal = "J. Symbolic Computation",
+ volume = "2",
+ number = "4",
+ year = "1986",
+ pages = "389397",
+ abstract =
+ "In this paper we present a new approach to automated geometry theorem
+ proving that is based on Buchberger's Gröbner bases method. The goal
+ is to automatically prove geometry theorems whose hypotheses and
+ conjecture can be expressed algebraically, i.e. by polynomial
+ equations. After shortly reviewing the problem considered and
+ discussing some new aspects of confirming theorems, we present two
+ different methods for applying Buehberger's algorithm to geometry
+ theorem proving, each of them being more efficient than the other on a
+ certain class of problems. The second method requires a new notion of
+ reduction, which we call pseudoreduction. This pseudoreduction yields
+ results on polynomials over some rational function field by
+ computations that are done merely over the rationals and, therefore,
+ is of general interest also. Finally, computing time statistics on 70
+ nontrivial examples are given, based on an implementation of the
+ methods in the computer algebra system SAC2 on an IBM 4341.",
+ paper = "Kutz86.pdf"
+}
+
@book{Lamp02,
author = "Lamport, Leslie",
title = "Specifying Systems",
@@ 8959,6 +9169,36 @@ paper = "Brea89.pdf"
abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
}
+@misc{Lond74,
+ author = "London, Ralph L. and Musser, David R.",
+ title = "The Application of a Symbolic Mathematical System to Program
+ Verification",
+ publisher = "USC Information Sciences Institute",
+ year = "1974",
+ abstract =
+ "Program verification is a relatively new application area for
+ symbolic mathematical systems. We report on an interactive
+ program verification system, based on the inductive assertion method,
+ which system is implemented using an existing symbolic mathematical
+ language and supporting system, Reduce. Reduce has been augmented
+ with a number of capabilities which are important to program
+ verification, particularly transformations on relational and Boolean
+ expressions. We believe these capabilities would be valuable in other
+ contexts and should be incorporated more widely into symbolic
+ mathematical systems for general use. The program verification
+ application can serve as a guide to an appropriate definition of
+ such capabilities, particularly with regard to the need to distinguish
+ between undefined program variables and polynomial indeterminates.
+ Additional capabilities which would benefit the program verification
+ application include representation of userdefined functions by
+ internal forms which directly incorporate properties such as
+ commutativity and associativity (as is commonly done with plus and
+ times), and a comprehensive facility for defining conditionally
+ applicable transformations.",
+ paper = "Lond74.pdf",
+ keywords = "axiomref"
+}
+
@article{Mahb06,
author = "Mahboubi, Assia",
title = "Proving Formally the Implementation of an Efficient gcd
@@ 9459,6 +9699,32 @@ paper = "Brea89.pdf"
keywords = "coercion"
}
+@article{Naum06,
+ author = "Naumowicz, Adam",
+ title = "An Example of Formalizing Recent Mathematical Results in Mizar",
+ journal = "Journal of Applied Logic",
+ volume = "4",
+ number = "4",
+ year = "2006",
+ pages = "396413",
+ abstract =
+ "This paper describes an example of the successful formalization of
+ quite advanced and new mathematics using the Mizar system. It shows
+ that although much effort is required to formalize nontrivial facts in
+ a formal computer deduction system, still it is possible to obtain the
+ level of full logical correctness of all inference steps. We also
+ discuss some problems encountered during the formalization, and try to
+ point out some of the features of the Mizar system responsible for
+ that. The formalization described in this paper allows also for
+ contrasting the linguistic capability of the Mizar language and some
+ of the phrases commonly used in “informal” mathematical papers that
+ the Mizar system lacks, and consequently presents the methods of how
+ to cope with it during the formalization. Yet, apart from the
+ problems, this paper shows some definite benefits from using a formal
+ computer system in the work of a mathematician.",
+ paper = "Naum06.pdf"
+}
+
@misc{Neup13,
author = "Neuper, Walther",
title = "Computer Algebra implemented in Isabelle's Function Package
@@ 9642,6 +9908,21 @@ paper = "Brea89.pdf"
paper = "Pare97.pdf"
}
+@book{Paul94,
+ author = "Paulson, Lawrence C.",
+ title = "ISABELLE: A Generic Theorem Prover",
+ year = "1994",
+ publisher = "Springer",
+ isbn = "9783540582441",
+}
+
+@misc{Paul98,
+ author = "Paulson, Lawrence C.",
+ title = "Introduction to Isabelle",
+ publisher = "Computer Laboratory, Univ. of Cambridge",
+ year = "1998"
+}
+
@article{Pela14,
author = "Pelayo, Alvaro and Warren, Michael A.",
title = "Homotopy Type Theory and Voevodsky's Univalent Foundations",
@@ 9682,6 +9963,16 @@ paper = "Brea89.pdf"
paper = "Pela14.pdf"
}
+@inproceedings{Pell91,
+ author = "Pelletier, Francis Jeffry",
+ title = "The Philosophy of Automated Theorem Proving",
+ booktitle = "Proc 12th IJCAI",
+ pages = "538543",
+ year = "1991",
+ publisher = "Morgan Kaufmann",
+ paper = "Pell91.pdf"
+}
+
@techreport{Pfen89,
author = "Pfenning, Frank and PaulinMohring, Christine",
title = "Inductively Defined Types in the Calculus of Constructions",
@@ 10005,6 +10296,32 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
+@techreport{Sege91,
+ author = "Seger, C. and Joyce, J.J.",
+ title = "A Twolevel Formal Verification Methodology using HOL and COSMOS",
+ type = "technical report",
+ year = "1991",
+ number = "9110",
+ institution = "Dept. of Comp. Sci. Univ. of British Columbia",
+ abstract =
+ "Theoremproving and symbolic simulation are both described as methods
+ for the formal verification of hardware. They are both used to achieve
+ a common goal  correctly designed hardware  and both are intended
+ to be an alternative to conventional methods based on nonexhaustive
+ simulation. However, they have different strengths and weaknesses. The
+ main significance of this paper  and its most original contribution
+  is the suggestion that symbolic simulation and theoremproving can
+ be combined in a complementary manner. We also outline our plans for
+ the development of a mathematical interface between the two approaches
+  in particular, a semantic link between the formulation of
+ higherorder logic used in the Cambridge HOL system and the
+ specification language used in the COSMOS system. We believe that this
+ combination offers great potential as a practical formal verification
+ methodology which combines the ability to accurately model circuit
+ level behavior with the ability to reason about digital hardware at
+ higher levels of abstraction"
+}
+
@misc{Seli13,
author = "Selinger, Peter",
title = "Lecture Notes on the Lambda Calculus",
@@ 10031,6 +10348,14 @@ paper = "Brea89.pdf"
isbn = "0521771730"
}
+@misc{Smit60,
+ author = "Smith, Brian Cantwell",
+ title = "The Limits of Correctness",
+ year = "1960",
+ link = "\url{http://eliza.newhaven.edu/ethics/Resources/14.ReliabilityResponsibility/LimitsOfCorrectness.pdf}",
+ paper = "Smit60.pdf"
+}
+
@article{Soze08,
author = "Sozeau, Mattieu and Oury, Nicolas",
title = "FirstClass Type Classes",
@@ 10196,6 +10521,39 @@ paper = "Brea89.pdf"
paper = "Wadl14.pdf"
}
+@misc{Wals92,
+ author = "Walsh, Toby and Nunes, Alex and Bundy, Alan",
+ title = "The Use of Proof Plans to Sum Series",
+ booktitle = "Proc. of 11th Int. Conf. on Automated Deduction",
+ year = "1992",
+ abstract =
+ "We describe a program for finding closed form solutions to finite
+ sums. The program was built to test the applicability of the proof
+ planning search control technique in a domain of mathematics outwith
+ induction. This experiment was successful. The series summing program
+ extends previous work in this area and was built in a short time just
+ by providing new series summing methods to our existing inductive
+ theorem proving system CLAM.
+
+ One surprising discovery was the
+ usefulness of the ripple tactic in summing series. Rippling is the key
+ tactic for controlling inductive proofs, and was previously thought to
+ be specialised to such proofs. However, it turns out to be the key
+ subtactic used by all the main tactics for summing series. The only
+ change required was that it had to be supplemented by a difference
+ matching algorithm to set up some initial metalevel annotations to
+ guide the rippling process. In inductive proofs these annotations are
+ provided by the application of mathematical induction. This evidence
+ suggests that rippling, supplemented by difference matching, will find
+ wide application in controlling mathematical proofs. The research
+ reported in this paper was supported by SERC grant GR/F/71799, a SERC
+ PostDoctoral Fellowship to the first author and a SERC Senior
+ Fellowship to the third author. We would like to thank the other
+ members of the mathematical reasoning group for their feedback on this
+ project.",
+ paper = "Wals92.pdf"
+}
+
@misc{Warn17,
author = "Warner, Evan",
title = "Splash Talk: The Foundational Crisis of Mathematics",
@@ 10215,6 +10573,21 @@ paper = "Brea89.pdf"
paper = "Warn17.pdf"
}
+@misc{Wied07,
+ author = "Wiedijk, Freek",
+ title = "The Seventeen Provers of the World",
+ link = "\url{http://www.cs.kun.nl/~freek/comparison/comparison.pdf}",
+ year = "2007",
+ abstract =
+ "We compare the styles of several proof assistants for mathematics.
+ We present Pythagoras' proof of the irrationality of $\sqrt{2}$ both
+ informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq,
+ (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX,
+ (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl,
+ (15) $\Omega$mega, (16) B method, (17) Minlog",
+ paper = "Wied07.pdf"
+}
+
@misc{Wijn68,
author = "Wijngarrden, A. van and Mailloux, B.J. and Peck, J.E.L. and
Koster, C.H.A. and Sintzoff, M. and Lindsey, C.H. and
@@ 14627,7 +15000,7 @@ paper = "Brea89.pdf"
measures on both the projection sets and the entire computation, which
turn out to be highly correlated. The statistical data also shows that
the orders generated by our algorithm are significantly close to optimal.",
 paper = "Doze04.pdf"
+ paper = "Dolz04.pdf"
}
@misc{Engl16,
@@ 15769,6 +16142,27 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Kajl98,
+ author = "Kajler, Norbert and Soiffer, Neil",
+ title = "A Survey of User Interfaces for Computer Algebra Systems",
+ journal = "J. Symbolic Computation",
+ volume = "25",
+ pages = "127159",
+ year = "1998",
+ abstract =
+ "This paper surveys work within the Computer Algebra community (and
+ elsewhere) directed towards improving user interfaces for scienti c
+ computation during the period 19631994. It is intended to be useful
+ to two groups of people: those who wish to know what work has been
+ done and those who would like to do work in the field. It contains an
+ extensive bibliography to assist readers in exploring the field in more
+ depth. Work related to improving human interaction with computer
+ algebra systems is the main focus of the paper. However, the paper
+ includes additional materials on some closely related issues such as
+ structured document editing, graphics, and communication protocols.",
+ paper = "Kajl98.pdf"
+}
+
@misc{West95,
author = "Wester, Michael J.",
title = "A Review of CAS Mathematical Capabilities",
@@ 18899,6 +19293,52 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Blai70a,
+ author = "Blair, Fred W. and Griesmer, James H. and Jenks, Richard D.",
+ title = "An interactive facility for symbolic mathematics",
+ journal = "ACM SIGSAM",
+ volume = "14",
+ year = "1970",
+ pages = "1718",
+ abstract =
+ "This paper describes a system designed to provide an interactive
+ symbolic computational facility for the mathematician user. To carry
+ out this objective, an experimental LISP system has been implemented
+ for IBM System/360 computers. Using this LISP system as a base,
+ portions of several systems have been combined and augmented to
+ provide the following facilities to a user:(1) rational function
+ manipulation and simplification; symbolic differentiation (Anthony
+ Hearn's REDUCE)(2) symbolic integration (Joel Moses' SIN)(3)
+ polynomial factorization, solution of linear differential equations,
+ direct and inverse symbolic Laplace transforms (Carl Engelman's
+ MATHLAB, including Knut Korsvold's simplification system)(4) unlimited
+ precision integer arithmetic(5) manipulation of arrays containing
+ symbolic entries(6) twodimensional output on IBM 2741 terminals or
+ IBM 2250 displays (William Martin's Symbolic Mathematical Laboratory,
+ and Jonathan Millen's CHARYBDIS program from MATHLAB)(7)
+ selfextending language facility (META/LISP).The user language created
+ for the system incorporates a subset of ``customary'' mathematical
+ notation. Data objects include sequences (both finite and infinite)
+ and arrays of arbitrary rank. Assignment statements are the
+ fundamental commands in the user language; they may contain
+ ``for''clauses which restrict the domain for which the assignment is
+ valid and permit ``piecewise'' and recursive definition of new operators
+ and functions. The user may also enter syntax definition statements in
+ order to introduce new notations into the system.Expressions appearing
+ in assignment statements may include ``where''clauses which allow user
+ control over the ``environment'' used in evaluation. Otherwise,
+ evaluation of expressions occurs in the current environment created by
+ the successive user commands, with certain operations such as
+ integration, differentiation, and simplification performed
+ automatically.Translators for the user language and for a resident
+ higherlevel procedural language facility are written in META/LISP, a
+ new selfcompiling translatorwriting system. As a result, all input
+ language facilities as well as the underlying manipulation routines
+ may be interactively extended by an experienced user.",
+ paper = "Blai70a.pdf",
+ keywords = "axiomref"
+}
+
@InProceedings{Bosm94,
author = "Bosma, Wieb and Cannon, John and Matthews, Graham",
title = "Programming with algebraic structures: Design of the Magma
@@ 20341,6 +20781,7 @@ paper = "Brea89.pdf"
institution = "Numerical Algorithms Group, Oxford, U.K.",
number = "TR5/92",
year = "1992",
+ paper = "Dave92a.pdf",
keywords = "axiomref"
}
@@ 29453,6 +29894,14 @@ paper = "Brea89.pdf"
paper = "Beez15.pdf"
}
+@misc{Bern85,
+ author = "Berndt, B.C.",
+ title = "Ramanujan's Notebooks, Part I",
+ publisher = "SpringerVerlag",
+ year = "1985",
+ pages = "2543"
+}
+
@book{Bern91,
author = "Bernays, Paul",
title = "Axiomatic Set Theory",
@@ 29655,7 +30104,7 @@ paper = "Brea89.pdf"
@article{Brui94,
author = "de Bruijn, N.G.",
 title = "A Survey on the project Automath",
+ title = "A Survey of the project Automath",
journal = "Studies in Logic and the Foundations of Mathematics",
volume = "133",
year = "1994",
@@ 29701,6 +30150,14 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@book{Buch81,
+ author = "Buchberger, B. and Lichtenberger, F.",
+ title = "Mathematics for Computer Science I  The Method of Mathematics",
+ publisher = "Springer",
+ year = "1981",
+ comment = "German"
+}
+
@book{Buch96,
author = "Buchberger, B.",
title = "Symbolic Computation: Computer Algebra and Logic",
@@ 31591,6 +32048,14 @@ paper = "Brea89.pdf"
paper = "Stee90.pdf"
}
+@book{Stur93,
+ author = "Sturmfels, Bernd.",
+ title = "Algorithms in Invariant Theory",
+ year = "1993",
+ publisher = "Springer",
+ paper = "Stur93.pdf"
+}
+
@misc{Stic93,
author = "Stichtenoth, H.",
title = "Algebraic function fields and codes",
@@ 31598,6 +32063,25 @@ paper = "Brea89.pdf"
year = "1993"
}
+@article{Supp89,
+ author = "Suppes, Patrick and Takahashi, Shuzo",
+ title = "An Interactive Calculus TheoremProver for Continuity Properties",
+ journal = "J. Symbolic Computation",
+ volume = "7",
+ number = "6",
+ pages = "573590",
+ year = "1989",
+ abstract =
+ "The work reported concerns the development of an interactive
+ theoremprover for the foundationsof the differential and integral
+ calculus. The main tools are a resolution theoremprover VERIFY,
+ previously developed for interactive proofs in set theory, and the
+ symbolic computation program REDUCE. The use of REDUCE in a
+ theoremproving context is described in detail. Sample proofs are
+ given with data on computation time per step on an IBM4381.",
+ paper = "Supp89.pdf"
+}
+
@techreport{Swee86,
author = "Sweedler, Moss E.",
title = "Typing in Scratchpad II",
@@ 31788,6 +32272,14 @@ paper = "Brea89.pdf"
link = "\url{https://en.wikipedia.org/wiki/Levenshtein\_distance}"
}
+@book{Wuxx94,
+ author = "Wu, Wentsun",
+ title = "Mechanical Theorem Proving in Geometries",
+ isbn = "9783709166390",
+ publisher = "Springer",
+ year = "1994"
+}
+
@article{Wulf76,
author = "Wulf, William A. and London, Ralph L. and Shaw, Mary",
title = "An Introduction to the Construction and Verification of
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 8eef500..5af1772 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 2962,6 +2962,16 @@ paper = "Brea89.pdf"
\subsection{Q} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{chunk}{axiom.bib}
+@misc{QED94,
+ author = "Anonymous",
+ title = "The QED Manifesto",
+ link = "\url{}",
+ paper = "QED94.txt"
+}
+
+\end{chunk}
+
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Rector, D. L.}
@@ 9504,6 +9514,21 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
+\index{Archer, M.}
+\index{Fink, G.}
+\index{Yang, L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Arch93,
+ author = "Archer, M. and Fink, G. and Yang, L.",
+ title = "Linking Other Theorem Provers to HOL Using PM: Proof Manager",
+ booktitle = "Int Workshop on the HOL Theorem Proving System and its
+ Applications",
+ publisher = "NorthHolland",
+ year = "1993"
+}
+
+\end{chunk}
+
\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
@article{Avig12a,
@@ 9570,6 +9595,19 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\subsection{B} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Backus, John}
+\begin{chunk}{axiom.bib}
+@techreport{Back73,
+ author = "Backus, John",
+ title = "Programming Language Semantics and Closed Applicative Language",
+ type = "technical report",
+ institution = "IBM",
+ number = "RJ 1245",
+ year = "1973"
+}
+
+\end{chunk}
+
\index{Ballarin, Clemens}
\index{Homann, Karsten}
\index{Calmet, Jacques}
@@ 10163,6 +10201,32 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
+
+\index{Boyer, Bob}
+\index{Kaufmann, Matt}
+\index{Moore, J}
+\begin{chunk}{axiom.bib}
+@misc{Boye81,
+ author = "Boyer, Bob and Kaufmann, Matt and Moore, J",
+ title = "Metafunctions in Nqthm and Acl2",
+ link = "\url{https://www.cs.utexas.edu/users/boyer/metanqthmacl2.text}",
+ year = "1981"
+}
+
+\end{chunk}
+
+\index{Boyer, R.S.}
+\index{Moore, J.S.}
+\begin{chunk}{axiom.bib}
+@book{Boye88,
+ author = "Boyer, R.S. and Moore, J.S.",
+ title = "A Computational Logic Handbook",
+ publisher = "Academic Press",
+ year = "1988"
+}
+
+\end{chunk}
+
\index{Bradley, Aaron R.}
\index{Manna, Zohar}
\begin{chunk}{axiom.bib}
@@ 10352,6 +10416,24 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
\index{Bundy, Alan}
+\index{van Harmelen, Frank}
+\index{Horn, Christian}
+\index{Smaill, Alan}
+\begin{chunk}{axiom.bib}
+@article{Bund90,
+ author = "Bundy, Alan and van Harmelen, Frank and Horn, Christian and
+ Smaill, Alan",
+ title = "The OysterClam System",
+ journal = "Lecture Notes in Artificial Intelligence",
+ volume = "449",
+ year = "1990",
+ pages = "647648",
+ paper = "Bund90.pdf"
+}
+
+\end{chunk}
+
+\index{Bundy, Alan}
\index{Stevens, Andrew}
\index{van Hemelen, Frank}
\index{Ireland, Andrew}
@@ 10376,7 +10458,8 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
which embodies these extensions as special cases. We prove that
generalised rippling always terminates, and we discuss the
implementation of the tactic and its relation with other inductive
 proof search heuristics."
+ proof search heuristics.",
+ paper = "Bund93b.pdf"
}
\end{chunk}
@@ 10394,6 +10477,18 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\subsection{C} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Cannon, John}
+\index{Bosma, Wieb}
+\begin{chunk}{axiom.bib}
+@book{Cann05,
+ author = "Cannon, John and Bosma, Wieb",
+ title = "Handbook of Magma Functions",
+ year = "2005",
+ publisher = "University of Sydney, School of Math and Statistics"
+}
+
+\end{chunk}
+
\index{Casteran, Pierre}
\index{Sozeau, Mattieu}
\begin{chunk}{axiom.bib}
@@ 10525,6 +10620,41 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
+\index{Clarke, Edmund}
+\index{Zhao, Xudong}
+\begin{chunk}{axiom.bib}
+@article{Clar93,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Analytica  A Theorem Prover for Mathematica",
+ journal = "The Mathematica Journal",
+ volume = "3",
+ number = "1",
+ year = "1993",
+ pages = "761765",
+ abstract =
+ "Analytica is an automatic theorem prover for theorems in
+ elementary analysis. The prover is written in 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 guarantee the
+ correctness of certain steps that are made by the symbolic
+ computation system and therefore prevent common errors like
+ division by a symbolic expression that could be zero. In this
+ paper we describe the structure of Analytica and explain the main
+ techniques that it uses to construct proofs. We have tried to make
+ the paper as selfcontained as possible so that it will be
+ accessible to a wide audience of potential users. We illustrate
+ the power of our theorem prover by several nontrivial examples
+ including the basic properties of the stereographic projection and
+ a series of three lemmas that lead to a proof of Weierstrass's
+ example of a continuous nowhere differentiable function. Each of
+ the lemmas in the latter example is proved completely
+ automatically."
+}
+
+\end{chunk}
+
\index{Comon, H.}
\index{Lugiez, D.}
\index{Schnoebelen, P.H.}
@@ 10554,6 +10684,29 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
+\index{Constable, R.L.}
+\index{Allen, S.F.}
+\index{Bromley, H.M.}
+\index{Cremer, J.F.}
+\index{Harper, R.W.}
+\index{Howe, D.J.}
+\index{Knoblock, T.B.}
+\index{Mendler, N.P.}
+\index{Panagaden, P.}
+\index{Tsaaki, J.T.}
+\index{Smith, S.F.}
+\begin{chunk}{axiom.bib}
+@book{Cons85,
+ author = "Constable, R.L. and Allen, S.F. and Bromley, H.M. and Cremer, J.F.
+ and Harper, R.W. and Howe, D.J. and Knoblock, T.B. and
+ Mendler, N.P. and Panagaden, P. and Tsaaki, J.T. and Smith, S.F.",
+ title = "Implementing Mathematics with The Nuprl Proof Development System",
+ publisher = "PrenticeHall",
+ year = "1985"
+}
+
+\end{chunk}
+
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
@@ 10898,6 +11051,21 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Dolzmann, A.}
+\index{Seidl, A.}
+\index{Sturm, T.}
+\begin{chunk}{axiom.bib}
+@misc{Dolz04a,
+ author = "Dolzmann, A. and Seidl, A. and Sturm, T.",
+ title = "Redlog User Manual",
+ year = "2004",
+ comment = "Edition 3.0",
+ link = "\url{http://www.reducealgebra.com/reduce38docs/redlog.pdf}",
+ paper = "Dolz04a.pdf"
+}
+
+\end{chunk}
+
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@inproceedings{Dybj90,
@@ 11216,6 +11384,17 @@ England, Matthew; Wilson, David
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Geddes, D.}
+\begin{chunk}{axiom.bib}
+@book{Gedd94,
+ author = "Geddes, D.",
+ title = "The DTP Manual",
+ publisher = "Stanford University",
+ year = "1994"
+}
+
+\end{chunk}
+
\index{Gentzen, Gerhard}
\begin{chunk}{axiom.bib}
@misc{Gent35,
@@ 11377,18 +11556,6 @@ England, Matthew; Wilson, David
\end{chunk}
\index{Gordon, Mike}
\begin{chunk}{axiom.bib}
@misc{Gord96,
 author = "Gordon, Mike",
 title = "From LCF to HOL: a short history",
 year = "1996",
 link = "\url{http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf}",
 paper = "Gord96.pdf"
}

\end{chunk}

\index{Goguen, Healfdene}
\index{McBride, Conor}
\index{McKinna, James}
@@ 11415,6 +11582,33 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Gordon, Mike}
+\begin{chunk}{axiom.bib}
+@misc{Gord96,
+ author = "Gordon, Mike",
+ title = "From LCF to HOL: a short history",
+ year = "1996",
+ link = "\url{http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf}",
+ paper = "Gord96.pdf"
+}
+
+\end{chunk}
+
+\index{Gordon, Mike J.C.}
+\index{Melham, T.F.}
+\begin{chunk}{axiom.bib}
+@book{Gord93,
+ author = "Gordon, Mike J.C. and Melham, T.F.",
+ title = "Introduction to HOL: A Theorem Proving Environment for Higher
+ Order Logic",
+ link = "\url{http://www.cs.ox.ac.uk/tom.melham/pub/Gordon1993ITH.html}",
+ publisher = "Cambridge University Press",
+ year = "1993",
+ isbn = "0521441897"
+}
+
+\end{chunk}
+
\index{Gottlieben, Hanne}
\index{Kelsey, Tom}
\index{Martin, Ursula}
@@ 11504,6 +11698,17 @@ England, Matthew; Wilson, David
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Van Hamelen, Frank}
+\begin{chunk}{axiom.bib}
+@misc{Hame89,
+ author = "Van Hamelen, Frank",
+ title = "The CLAM Proof Planner",
+ year = "1989",
+ publisher = "Dept. of AI, Univ. of Edinburgh"
+}
+
+\end{chunk}
+
\index{Hardin, David S.}
\index{McClurg, Jedidiah R.}
\index{Davis, Jennifer A.}
@@ 11687,6 +11892,34 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Howe, Douglas J.}
+\begin{chunk}{axiom.bib}
+@article{Howe88,
+ author = "Howe, Douglas J.",
+ title = "Computational Metatheory in Nuprl",
+ journal = "LNCS",
+ volume = "310",
+ pages = "238257",
+ year = "1988",
+ publisher = "SpringerVerlag",
+ abstract =
+ "This paper describes an implementation within Nuprl of mechanisms
+ that support the use of Nuprl's type theory as a language for
+ constructing theoremprovind procedures. The main componenet of the
+ implementation is a large library of definitions, theorems and
+ proofs. This library may be regarded as the beginning of a book of
+ formal mathematics; it contains the formal development and explanation
+ of a useful subset of Nuprl's metatheory, and of a mechanism for
+ translating results established about this embedded metatheory to the
+ object level. Nuprl's rich type theory, besides permitting the
+ internal development of this partial reflection mechanism, allows us
+ to make abstractions that drastically reduce the burden of
+ establishing the correctness of new theoremproving procedures. Our
+ library includes a formally verified termrewriting system"
+}
+
+\end{chunk}
+
\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
@inproceedings{Huet87,
@@ 12161,6 +12394,73 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Kumar, Ramayya}
+\index{Kropf, Thomas}
+\index{Schneider, Klaus}
+\begin{chunk}{axiom.bib}
+@inproceeding{Kuma91,
+ author = "Kumar, Ramayya and Kropf, Thomas and Schneider, Klaus",
+ title = "Integrating a FirstOrder Automatic Prover in the HOL Environment",
+ booktitle = "Int. Workshop on the HOL Theorem Prover System and its
+ Applications",
+ publisher = "IEEE Computer Society Press",
+ year = "1991",
+ abstract =
+ "The HOL system is a powerful tool for proving higher order formulae.
+ However, proofs have to be performed interactively and only little
+ automation using tactics is possible. Even though interaction is
+ desirable to guide major and creative backward proof steps of complex
+ proofs, a deluge of simple subgoals may evolve which all have to be
+ proven manually in order to accomplish the proof. Although these
+ subgoals are often simple formulae, their proof has not yet been
+ automated in HOL.
+
+ In this paper it is shown how it is possible to
+ automate these tasks by integrating a firstorder automated theorem
+ proving tool, called FAUST, into HOL. It is based on an efficient
+ variant of the wellknown sequent calculus. In order to maintain the
+ high confdence in HOLgenerated proofs, FAUST is able to generate HOL
+ tactics which may be used to postjustifr the theorem derived by FAUST
+ in HOL. The underlying calculus of FAUST, the tactic generation, as
+ well as experimental results are presented.",
+ paper = "Kuma91.pdf"
+}
+
+\end{chunk}
+
+\index{Kutzler, B.}
+\index{Stifter, S.}
+\begin{chunk}{axiom.bib}
+@article{Kutz86,
+ author = "Kutzler, B. and Stifter, S.",
+ title = "On the application of Buchberger's algorithm to automated
+ geometry theorem proving",
+ journal = "J. Symbolic Computation",
+ volume = "2",
+ number = "4",
+ year = "1986",
+ pages = "389397",
+ abstract =
+ "In this paper we present a new approach to automated geometry theorem
+ proving that is based on Buchberger's Gröbner bases method. The goal
+ is to automatically prove geometry theorems whose hypotheses and
+ conjecture can be expressed algebraically, i.e. by polynomial
+ equations. After shortly reviewing the problem considered and
+ discussing some new aspects of confirming theorems, we present two
+ different methods for applying Buehberger's algorithm to geometry
+ theorem proving, each of them being more efficient than the other on a
+ certain class of problems. The second method requires a new notion of
+ reduction, which we call pseudoreduction. This pseudoreduction yields
+ results on polynomials over some rational function field by
+ computations that are done merely over the rationals and, therefore,
+ is of general interest also. Finally, computing time statistics on 70
+ nontrivial examples are given, based on an implementation of the
+ methods in the computer algebra system SAC2 on an IBM 4341.",
+ paper = "Kutz86.pdf"
+}
+
+\end{chunk}p
+
\subsection{L} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Lamport, Leslie}
@@ 12242,6 +12542,41 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{London, Ralph L.}
+\index{Musser, David R.}
+\begin{chunk}{axiom.bib}
+@misc{Lond74,
+ author = "London, Ralph L. and Musser, David R.",
+ title = "The Application of a Symbolic Mathematical System to Program
+ Verification",
+ publisher = "USC Information Sciences Institute",
+ year = "1974",
+ abstract =
+ "Program verification is a relatively new application area for
+ symbolic mathematical systems. We report on an interactive
+ program verification system, based on the inductive assertion method,
+ which system is implemented using an existing symbolic mathematical
+ language and supporting system, Reduce. Reduce has been augmented
+ with a number of capabilities which are important to program
+ verification, particularly transformations on relational and Boolean
+ expressions. We believe these capabilities would be valuable in other
+ contexts and should be incorporated more widely into symbolic
+ mathematical systems for general use. The program verification
+ application can serve as a guide to an appropriate definition of
+ such capabilities, particularly with regard to the need to distinguish
+ between undefined program variables and polynomial indeterminates.
+ Additional capabilities which would benefit the program verification
+ application include representation of userdefined functions by
+ internal forms which directly incorporate properties such as
+ commutativity and associativity (as is commonly done with plus and
+ times), and a comprehensive facility for defining conditionally
+ applicable transformations.",
+ paper = "Lond74.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\subsection{M} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Mahboubi, Assia}
@@ 12865,6 +13200,36 @@ England, Matthew; Wilson, David
\subsection{N} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Naumowicz, Adam}
+\begin{chunk}{axiom.bib}
+@article{Naum06,
+ author = "Naumowicz, Adam",
+ title = "An Example of Formalizing Recent Mathematical Results in Mizar",
+ journal = "Journal of Applied Logic",
+ volume = "4",
+ number = "4",
+ year = "2006",
+ pages = "396413",
+ abstract =
+ "This paper describes an example of the successful formalization of
+ quite advanced and new mathematics using the Mizar system. It shows
+ that although much effort is required to formalize nontrivial facts in
+ a formal computer deduction system, still it is possible to obtain the
+ level of full logical correctness of all inference steps. We also
+ discuss some problems encountered during the formalization, and try to
+ point out some of the features of the Mizar system responsible for
+ that. The formalization described in this paper allows also for
+ contrasting the linguistic capability of the Mizar language and some
+ of the phrases commonly used in “informal” mathematical papers that
+ the Mizar system lacks, and consequently presents the methods of how
+ to cope with it during the formalization. Yet, apart from the
+ problems, this paper shows some definite benefits from using a formal
+ computer system in the work of a mathematician.",
+ paper = "Naum06.pdf"
+}
+
+\end{chunk}
+
\index{Neuper, Walther}
\begin{chunk}{axiom.bib}
@misc{Neup13,
@@ 13149,6 +13514,29 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@book{Paul94,
+ author = "Paulson, Lawrence C.",
+ title = "ISABELLE: A Generic Theorem Prover",
+ year = "1994",
+ publisher = "Springer",
+ isbn = "9783540582441",
+}
+
+\end{chunk}
+
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@misc{Paul98,
+ author = "Paulson, Lawrence C.",
+ title = "Introduction to Isabelle",
+ publisher = "Computer Laboratory, Univ. of Cambridge",
+ year = "1998"
+}
+
+\end{chunk}
+
\index{Pelayo, Alvaro}
\index{Warren, Michael A.}
\begin{chunk}{axiom.bib}
@@ 13194,6 +13582,20 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Pelletier, Francis Jeffry}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pell91,
+ author = "Pelletier, Francis Jeffry",
+ title = "The Philosophy of Automated Theorem Proving",
+ booktitle = "Proc 12th IJCAI",
+ pages = "538543",
+ year = "1991",
+ publisher = "Morgan Kaufmann",
+ paper = "Pell91.pdf"
+}
+
+\end{chunk}
+
\index{Pfenning, Frank}
\index{PaulinMohring, Christine}
\begin{chunk}{axiom.bib}
@@ 13603,6 +14005,37 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Seger, C.}
+\index{Joyce, J.J.}
+\begin{chunk}{axiom.bib}
+@techreport{Sege91,
+ author = "Seger, C. and Joyce, J.J.",
+ title = "A Twolevel Formal Verification Methodology using HOL and COSMOS",
+ type = "technical report",
+ year = "1991",
+ number = "9110",
+ institution = "Dept. of Comp. Sci. Univ. of British Columbia",
+ abstract =
+ "Theoremproving and symbolic simulation are both described as methods
+ for the formal verification of hardware. They are both used to achieve
+ a common goal  correctly designed hardware  and both are intended
+ to be an alternative to conventional methods based on nonexhaustive
+ simulation. However, they have different strengths and weaknesses. The
+ main significance of this paper  and its most original contribution
+  is the suggestion that symbolic simulation and theoremproving can
+ be combined in a complementary manner. We also outline our plans for
+ the development of a mathematical interface between the two approaches
+  in particular, a semantic link between the formulation of
+ higherorder logic used in the Cambridge HOL system and the
+ specification language used in the COSMOS system. We believe that this
+ combination offers great potential as a practical formal verification
+ methodology which combines the ability to accurately model circuit
+ level behavior with the ability to reason about digital hardware at
+ higher levels of abstraction"
+}
+
+\end{chunk}
+
\index{Selinger, Peter}
\begin{chunk}{axiom.bib}
@misc{Seli13,
@@ 13637,6 +14070,18 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Smith, Brian Cantwell}
+\begin{chunk}{axiom.bib}
+@misc{Smit60,
+ author = "Smith, Brian Cantwell",
+ title = "The Limits of Correctness",
+ year = "1960",
+ link = "\url{http://eliza.newhaven.edu/ethics/Resources/14.ReliabilityResponsibility/LimitsOfCorrectness.pdf}",
+ paper = "Smit60.pdf"
+}
+
+\end{chunk}
+
\index{Sozeau, Mattieu}
\index{Oury, Nicolas}
\begin{chunk}{axiom.bib}
@@ 13854,6 +14299,45 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Walsh, Toby}
+\index{Nunes, Alex}
+\index{Bundy, Alan}
+\begin{chunk}{axiom.bib}
+@misc{Wals92,
+ author = "Walsh, Toby and Nunes, Alex and Bundy, Alan",
+ title = "The Use of Proof Plans to Sum Series",
+ booktitle = "Proc. of 11th Int. Conf. on Automated Deduction",
+ year = "1992",
+ abstract =
+ "We describe a program for finding closed form solutions to finite
+ sums. The program was built to test the applicability of the proof
+ planning search control technique in a domain of mathematics outwith
+ induction. This experiment was successful. The series summing program
+ extends previous work in this area and was built in a short time just
+ by providing new series summing methods to our existing inductive
+ theorem proving system CLAM.
+
+ One surprising discovery was the
+ usefulness of the ripple tactic in summing series. Rippling is the key
+ tactic for controlling inductive proofs, and was previously thought to
+ be specialised to such proofs. However, it turns out to be the key
+ subtactic used by all the main tactics for summing series. The only
+ change required was that it had to be supplemented by a difference
+ matching algorithm to set up some initial metalevel annotations to
+ guide the rippling process. In inductive proofs these annotations are
+ provided by the application of mathematical induction. This evidence
+ suggests that rippling, supplemented by difference matching, will find
+ wide application in controlling mathematical proofs. The research
+ reported in this paper was supported by SERC grant GR/F/71799, a SERC
+ PostDoctoral Fellowship to the first author and a SERC Senior
+ Fellowship to the third author. We would like to thank the other
+ members of the mathematical reasoning group for their feedback on this
+ project.",
+ paper = "Wals92.pdf"
+}
+
+\end{chunk}
+
\index{Warner, Evan}
\begin{chunk}{axiom.bib}
@misc{Warn17,
@@ 13877,6 +14361,25 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Wiedijk, Freek}
+\begin{chunk}{axiom.bib}
+@misc{Wied07,
+ author = "Wiedijk, Freek",
+ title = "The Seventeen Provers of the World",
+ link = "\url{http://www.cs.kun.nl/~freek/comparison/comparison.pdf}",
+ year = "2007",
+ abstract =
+ "We compare the styles of several proof assistants for mathematics.
+ We present Pythagoras' proof of the irrationality of $\sqrt{2}$ both
+ informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq,
+ (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX,
+ (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl,
+ (15) $\Omega$mega, (16) B method, (17) Minlog",
+ paper = "Wied07.pdf"
+}
+
+\end{chunk}
+
\index{Wijngarrden, A. van}
\index{Mailloux, B.J.}
\index{Peck, J.E.L.}
@@ 20831,7 +21334,7 @@ Proc ISSAC 97 pp172175 (1997)
measures on both the projection sets and the entire computation, which
turn out to be highly correlated. The statistical data also shows that
the orders generated by our algorithm are significantly close to optimal.",
 paper = "Doze04.pdf"
+ paper = "Dolz04.pdf"
}
\end{chunk}
@@ 22271,6 +22774,32 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\index{Kajler, Norbert}
+\index{Soiffer, Neil}
+\begin{chunk}{axiom.bib}
+@article{Kajl98,
+ author = "Kajler, Norbert and Soiffer, Neil",
+ title = "A Survey of User Interfaces for Computer Algebra Systems",
+ journal = "J. Symbolic Computation",
+ volume = "25",
+ pages = "127159",
+ year = "1998",
+ abstract =
+ "This paper surveys work within the Computer Algebra community (and
+ elsewhere) directed towards improving user interfaces for scientific
+ computation during the period 19631994. It is intended to be useful
+ to two groups of people: those who wish to know what work has been
+ done and those who would like to do work in the field. It contains an
+ extensive bibliography to assist readers in exploring the field in more
+ depth. Work related to improving human interaction with computer
+ algebra systems is the main focus of the paper. However, the paper
+ includes additional materials on some closely related issues such as
+ structured document editing, graphics, and communication protocols.",
+ paper = "Kajl98.pdf"
+}
+
+\end{chunk}
+
\index{Wester, Michael J.}
\begin{chunk}{axiom.bib}
@misc{West95,
@@ 26447,6 +26976,58 @@ American Mathematical Society (1994)
\end{chunk}
\index{Blair, Fred W.}
+\index{Griesmer, James H.}
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Blai70a,
+ author = "Blair, Fred W. and Griesmer, James H. and Jenks, Richard D.",
+ title = "An interactive facility for symbolic mathematics",
+ journal = "ACM SIGSAM",
+ volume = "14",
+ year = "1970",
+ pages = "1718",
+ abstract =
+ "This paper describes a system designed to provide an interactive
+ symbolic computational facility for the mathematician user. To carry
+ out this objective, an experimental LISP system has been implemented
+ for IBM System/360 computers. Using this LISP system as a base,
+ portions of several systems have been combined and augmented to
+ provide the following facilities to a user:(1) rational function
+ manipulation and simplification; symbolic differentiation (Anthony
+ Hearn's REDUCE)(2) symbolic integration (Joel Moses' SIN)(3)
+ polynomial factorization, solution of linear differential equations,
+ direct and inverse symbolic Laplace transforms (Carl Engelman's
+ MATHLAB, including Knut Korsvold's simplification system)(4) unlimited
+ precision integer arithmetic(5) manipulation of arrays containing
+ symbolic entries(6) twodimensional output on IBM 2741 terminals or
+ IBM 2250 displays (William Martin's Symbolic Mathematical Laboratory,
+ and Jonathan Millen's CHARYBDIS program from MATHLAB)(7)
+ selfextending language facility (META/LISP).The user language created
+ for the system incorporates a subset of ``customary'' mathematical
+ notation. Data objects include sequences (both finite and infinite)
+ and arrays of arbitrary rank. Assignment statements are the
+ fundamental commands in the user language; they may contain
+ ``for''clauses which restrict the domain for which the assignment is
+ valid and permit ``piecewise'' and recursive definition of new operators
+ and functions. The user may also enter syntax definition statements in
+ order to introduce new notations into the system.Expressions appearing
+ in assignment statements may include ``where''clauses which allow user
+ control over the ``environment'' used in evaluation. Otherwise,
+ evaluation of expressions occurs in the current environment created by
+ the successive user commands, with certain operations such as
+ integration, differentiation, and simplification performed
+ automatically.Translators for the user language and for a resident
+ higherlevel procedural language facility are written in META/LISP, a
+ new selfcompiling translatorwriting system. As a result, all input
+ language facilities as well as the underlying manipulation routines
+ may be interactively extended by an experienced user.",
+ paper = "Blai70a.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Blair, Fred W.}
\index{Jenks, Richard D.}
\begin{chunk}{ignore}
\bibitem[Blair 70a]{BJ70}
@@ 29015,6 +29596,7 @@ April 89, 2013 Portland Oregon
institution = "Numerical Algorithms Group, Oxford, U.K.",
number = "TR5/92",
year = "1992",
+ paper = "Dave92a.pdf",
keywords = "axiomref"
}
@@ 44172,6 +44754,18 @@ J. Symbolic Computation (1993) 15, 393413
\end{chunk}
+\index{Berndt, B.C.}
+\begin{chunk}{axiom.bib}
+@misc{Bern85,
+ author = "Berndt, B.C.",
+ title = "Ramanujan's Notebooks, Part I",
+ publisher = "SpringerVerlag",
+ year = "1985",
+ pages = "2543"
+}
+
+\end{chunk}
+
\index{Bernays, Paul}
\begin{chunk}{axiom.bib}
@book{Bern91,
@@ 44543,7 +45137,7 @@ ISBN 3764359013 (1998)
\begin{chunk}{axiom.bib}
@article{Brui94,
author = "de Bruijn, N.G.",
 title = "A Survey on the project Automath",
+ title = "A Survey of the project Automath",
journal = "Studies in Logic and the Foundations of Mathematics",
volume = "133",
year = "1994",
@@ 44599,6 +45193,19 @@ ISBN 3764359013 (1998)
\end{chunk}
\index{Buchberger, B.}
+\index{Lichtenberger, F.}
+\begin{chunk}{axiom.bib}
+@book{Buch81,
+ author = "Buchberger, B. and Lichtenberger, F.",
+ title = "Mathematics for Computer Science I  The Method of Mathematics",
+ publisher = "Springer",
+ year = "1981",
+ comment = "German"
+}
+
+\end{chunk}
+b
+\index{Buchberger, B.}
\begin{chunk}{axiom.bib}
@book{Buch96,
author = "Buchberger, B.",
@@ 49026,6 +49633,18 @@ The University of Chicago Press. 1974
\end{chunk}
+\index{Sturmfels, Bernd.}
+\begin{chunk}{axiom.bib}
+@book{Stur93,
+ author = "Sturmfels, Bernd.",
+ title = "Algorithms in Invariant Theory",
+ year = "1993",
+ publisher = "Springer",
+ paper = "Stur93.pdf"
+}
+
+\end{chunk}
+
\index{Stichtenoth, H.}
\begin{chunk}{axiom.bib}
@misc{Stic93,
@@ 49054,6 +49673,30 @@ PrenticeHall 1971
\end{chunk}
+\index{Suppes, Patrick}
+\index{Takahashi, Shuzo}
+\begin{chunk}{axiom.bib}
+@article{Supp89,
+ author = "Suppes, Patrick and Takahashi, Shuzo",
+ title = "An Interactive Calculus TheoremProver for Continuity Properties",
+ journal = "J. Symbolic Computation",
+ volume = "7",
+ number = "6",
+ pages = "573590",
+ year = "1989",
+ abstract =
+ "The work reported concerns the development of an interactive
+ theoremprover for the foundationsof the differential and integral
+ calculus. The main tools are a resolution theoremprover VERIFY,
+ previously developed for interactive proofs in set theory, and the
+ symbolic computation program REDUCE. The use of REDUCE in a
+ theoremproving context is described in detail. Sample proofs are
+ given with data on computation time per step on an IBM4381.",
+ paper = "Supp89.pdf"
+}
+
+\end{chunk}
+
\index{Swarztrauber, P. N.}
\index{Sweet, R. A.}
\begin{chunk}{ignore}
@@ 49551,6 +50194,18 @@ Van Nostrand. (1967)
\end{chunk}
+\index{Wu, Wentsun}
+\begin{chunk}{axiom.bib}
+@book{Wuxx94,
+ author = "Wu, Wentsun",
+ title = "Mechanical Theorem Proving in Geometries",
+ isbn = "9783709166390",
+ publisher = "Springer",
+ year = "1994"
+}
+
+\end{chunk}
+
\index{Wu, W.T.}
\begin{chunk}{ignore}
\bibitem[Wu 87]{WU87} Wu, W.T.
diff git a/changelog b/changelog
index a63b5a7..576da38 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171016 tpd src/axiomwebsite/patches.html 20171016.01.tpd.patch
+20171016 tpd books/bookvolbib Proving Axiom Correct references
20171011 tpd src/axiomwebsite/patches.html 20171011.01.tpd.patch
20171011 tpd books/bookvolbib Proving Axiom Correct references
20171010 tpd src/axiomwebsite/patches.html 20171010.01.tpd.patch
diff git a/patch b/patch
index d2a7035..2126375 100644
 a/patch
+++ b/patch
@@ 2,141 +2,529 @@ books/bookvolbib Proving Axiom Correct references
Goal: Proving Axiom Correct
\index{de Bruijn, N.G.}
+\index{Berndt, B.C.}
\begin{chunk}{axiom.bib}
\article{Brui68,
 author = "de Bruijn, N.G."
 title = "The Mathematical Language Automath, its Usage, and Some of
 its Extensions",
 journal = "Lecture Notes in Mathematics",
 publisher = "Springer",
 year = "1994",
 volume = "125",
 paper = "Brui68.pdf",
 keywords = "CASProof"
+@misc{Bern85,
+ author = "Berndt, B.C.",
+ title = "Ramanujan's Notebooks, Part I",
+ publisher = "SpringerVerlag",
+ year = "1985",
+ pages = "2543"
}
\end{chunk}
\index{Jones, C.}
+\index{London, Ralph L.}
+\index{Musser, David R.}
\begin{chunk}{axiom.bib}
@book{Jone93,
 author = "Jones, C.",
 title = Completing the Rationals and Metric Spaces in LEGO",
 booktitle = "Logical Frameworks",
 pages = "209222",
 year = "1993",
 publisher = "Cambridge University Press"
}
+@misc{Lond74,
+ author = "London, Ralph L. and Musser, David R.",
+ title = "The Application of a Symbolic Mathematical System to Program
+ Verification",
+ publisher = "USC Information Sciences Institute",
+ year = "1974",
+ abstract =
+ "Program verification is a relatively new application area for
+ symbolic mathematical systems. We report on an interactive
+ program verification system, based on the inductive assertion method,
+ which system is implemented using an existing symbolic mathematical
+ language and supporting system, Reduce. Reduce has been augmented
+ with a number of capabilities which are important to program
+ verification, particularly transformations on relational and Boolean
+ expressions. We believe these capabilities would be valuable in other
+ contexts and should be incorporated more widely into symbolic
+ mathematical systems for general use. The program verification
+ application can serve as a guide to an appropriate definition of
+ such capabilities, particularly with regard to the need to distinguish
+ between undefined program variables and polynomial indeterminates.
+ Additional capabilities which would benefit the program verification
+ application include representation of userdefined functions by
+ internal forms which directly incorporate properties such as
+ commutativity and associativity (as is commonly done with plus and
+ times), and a comprehensive facility for defining conditionally
+ applicable transformations.",
+ paper = "Lond74.pdf",
+ keywords = "axiomref"
+}
\end{chunk}
+\index{Suppes, Patrick}
+\index{Takahashi, Shuzo}
\begin{chunk}{axiom.bib}
@misc{JARx96,
 author = "various",
 title = "Journal of Automated Reasoning",
 publisher = "Springer",
 year = "1996",
 volume = "16",
 number = "1/2",
 comment = "Special Issue on Inductive Proof"
+@article{Supp89,
+ author = "Suppes, Patrick and Takahashi, Shuzo",
+ title = "An Interactive Calculus TheoremProver for Continuity Properties",
+ journal = "J. Symbolic Computation",
+ volume = "7",
+ number = "6",
+ pages = "573590",
+ year = "1989",
+ abstract =
+ "The work reported concerns the development of an interactive
+ theoremprover for the foundationsof the differential and integral
+ calculus. The main tools are a resolution theoremprover VERIFY,
+ previously developed for interactive proofs in set theory, and the
+ symbolic computation program REDUCE. The use of REDUCE in a
+ theoremproving context is described in detail. Sample proofs are
+ given with data on computation time per step on an IBM4381.",
+ paper = "Supp89.pdf"
}
\end{chunk}
+\index{Walsh, Toby}
+\index{Nunes, Alex}
\index{Bundy, Alan}
\index{Stevens, Andrew}
\index{van Hemelen, Frank}
\index{Ireland, Andrew}
\index{Smaill, Alan}
\begin{chunk}{axiom.bib}
@article{Bund93b,
 author = "Bundy, Alan and Stevens, Andrew and van Hemelen, Frank and
 Ireland, Andrew and Smaill, Alan",
 title = "Rippling: A heuristic for guiding inductive proofs",
 journal = "Artifical Intelligence",
 volume = "62",
 number = "2",
 year = "1993",
 pages = "185253",
+\begin{chunk}{axiom.bib}
+@misc{Wals92,
+ author = "Walsh, Toby and Nunes, Alex and Bundy, Alan",
+ title = "The Use of Proof Plans to Sum Series",
+ booktitle = "Proc. of 11th Int. Conf. on Automated Deduction",
+ year = "1992",
abstract =
 "We describe rippling: a tactic for the heuristic control of the key
 part of proofs by mathematical induction. This tactic significantly
 reduces the search for a proof of a wide variety of inductive
 theorems. We first present a basic version of rippling, followed by
 various extensions which are necessary to capture larger classes of
 inductive proofs. Finally, we present a generalised form of rippling
 which embodies these extensions as special cases. We prove that
 generalised rippling always terminates, and we discuss the
 implementation of the tactic and its relation with other inductive
 proof search heuristics."
+ "We describe a program for finding closed form solutions to finite
+ sums. The program was built to test the applicability of the proof
+ planning search control technique in a domain of mathematics outwith
+ induction. This experiment was successful. The series summing program
+ extends previous work in this area and was built in a short time just
+ by providing new series summing methods to our existing inductive
+ theorem proving system CLAM.
+
+ One surprising discovery was the
+ usefulness of the ripple tactic in summing series. Rippling is the key
+ tactic for controlling inductive proofs, and was previously thought to
+ be specialised to such proofs. However, it turns out to be the key
+ subtactic used by all the main tactics for summing series. The only
+ change required was that it had to be supplemented by a difference
+ matching algorithm to set up some initial metalevel annotations to
+ guide the rippling process. In inductive proofs these annotations are
+ provided by the application of mathematical induction. This evidence
+ suggests that rippling, supplemented by difference matching, will find
+ wide application in controlling mathematical proofs. The research
+ reported in this paper was supported by SERC grant GR/F/71799, a SERC
+ PostDoctoral Fellowship to the first author and a SERC Senior
+ Fellowship to the third author. We would like to thank the other
+ members of the mathematical reasoning group for their feedback on this
+ project.",
+ paper = "Wals92.pdf"
}
\end{chunk}
\index{Bundy, Alan}
+\index{Blair, Fred W.}
+\index{Griesmer, James H.}
+\index{Jenks, Richard D.}
\begin{chunk}{axiom.bib}
@article{Bund88,
 author = "Bundy, Alan",
 title = "The Use of Explicit Plans to Guide Inductive Proofs",
 journal = "LNCS 310",
 volume = "310",
 pages = "111120",
 year = "1998",
+@article{Blai70a,
+ author = "Blair, Fred W. and Griesmer, James H. and Jenks, Richard D.",
+ title = "An interactive facility for symbolic mathematics",
+ journal = "ACM SIGSAM",
+ volume = "14",
+ year = "1970",
+ pages = "1718",
abstract =
 "We propose the use of explicit proof plans to guide the search for a
 proof in automatic theorem proving. By representing proof plans as the
 specifications of LCFlike tactics and by recording these
 specifications in a sorted metalogic, we are able to reason about the
 conjectures to be proved and the methods available to prove them. In
 this way we can build proof plans of wide generality, formally account
 for and predict their successes and failures, apply them flexibly,
 recover from their failures, and learn them from example proofs.

 We illustrate this technique by building a proof plan based on a
 simple subset of the implicit proof plan embedded in the BoyerMoore
 theorem prover.",
 paper = "Bund88.pdf"
+ "This paper describes a system designed to provide an interactive
+ symbolic computational facility for the mathematician user. To carry
+ out this objective, an experimental LISP system has been implemented
+ for IBM System/360 computers. Using this LISP system as a base,
+ portions of several systems have been combined and augmented to
+ provide the following facilities to a user:(1) rational function
+ manipulation and simplification; symbolic differentiation (Anthony
+ Hearn's REDUCE)(2) symbolic integration (Joel Moses' SIN)(3)
+ polynomial factorization, solution of linear differential equations,
+ direct and inverse symbolic Laplace transforms (Carl Engelman's
+ MATHLAB, including Knut Korsvold's simplification system)(4) unlimited
+ precision integer arithmetic(5) manipulation of arrays containing
+ symbolic entries(6) twodimensional output on IBM 2741 terminals or
+ IBM 2250 displays (William Martin's Symbolic Mathematical Laboratory,
+ and Jonathan Millen's CHARYBDIS program from MATHLAB)(7)
+ selfextending language facility (META/LISP).The user language created
+ for the system incorporates a subset of "customary" mathematical
+ notation. Data objects include sequences (both finite and infinite)
+ and arrays of arbitrary rank. Assignment statements are the
+ fundamental commands in the user language; they may contain
+ "for"clauses which restrict the domain for which the assignment is
+ valid and permit "piecewise" and recursive definition of new operators
+ and functions. The user may also enter syntax definition statements in
+ order to introduce new notations into the system.Expressions appearing
+ in assignment statements may include "where"clauses which allow user
+ control over the "environment" used in evaluation. Otherwise,
+ evaluation of expressions occurs in the current environment created by
+ the successive user commands, with certain operations such as
+ integration, differentiation, and simplification performed
+ automatically.Translators for the user language and for a resident
+ higherlevel procedural language facility are written in META/LISP, a
+ new selfcompiling translatorwriting system. As a result, all input
+ language facilities as well as the underlying manipulation routines
+ may be interactively extended by an experienced user.",
+ paper = "Blai70a.pdf",
+ keywords = "axiomref"
}
\end{chunk}
\index{Guttag, John V.}
\index{Horning, James J.}
+\index{Sturmfels, B.}
\begin{chunk}{axiom.bib}
@book{Gutt93,
 author = "Guttag, John V. and Horning, James J.",
 title = "LARCH: Languages and TOols for Formal Specifications",
 publisher = "SpringerVerlag",
+@book{Stur93,
+ author = "Sturmfels, B.",
+ title = "Algorithms in Invariant Theory",
year = "1993",
 isbn = "3540940065"
+ publisher = "Springer"
}
\end{chunk}
\index{McCune, William W.}
+\index{Wu, Wentsun}
\begin{chunk}{axiom.bib}
@article{Mccu93,
 author = "McCune, William W.",
 title = "Single Axioms for Groups and Abelian Groups with Various
 Operations",
 journal = "J. Automated Reasoning",
 volume = "10",
+@book{Wuxx94,
+ author = "Wu, Wentsun",
+ title = "Mechanical Theorem Proving in Geometries",
+ isbn = "9783709166390",
+ publisher = "Springer",
+ year = "1994"
+}
+
+\end{chunk}
+
+\index{Buchberger, B.}
+\index{Lichtenberger, F.}
+\begin{chunk}{axiom.bib}
+@book{Buch81,
+ author = "Buchberger, B. and Lichtenberger, F.",
+ title = "Mathematics for Computer Science I  The Method of Mathematics",
+ publisher = "Springer",
+ year = "1981",
+ comment = "German"
+}
+
+\end{chunk}
+
+\index{Clarke, Edmund}
+\index{Zhao, Xudong}
+\begin{chunk}{axiom.bib}
+@article{Clar93,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Analytica  A Theorem Prover for Mathematica",
+ journal = "The Mathematica Journal",
+ volume = "3",
number = "1",
year = "1993",
+ pages = "761765",
+ abstract =
+ "Analytica is an automatic theorem prover for theorems in
+ elementary analysis. The prover is written in 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 guarantee the
+ correctness of certain steps that are made by the symbolic
+ computation system and therefore prevent common errors like
+ division by a symbolic expression that could be zero. In this
+ paper we describe the structure of Analytica and explain the main
+ techniques that it uses to construct proofs. We have tried to make
+ the paper as selfcontained as possible so that it will be
+ accessible to a wide audience of potential users. We illustrate
+ the power of our theorem prover by several nontrivial examples
+ including the basic properties of the stereographic projection and
+ a series of three lemmas that lead to a proof of Weierstrass's
+ example of a continuous nowhere differentiable function. Each of
+ the lemmas in the latter example is proved completely
+ automatically."
+}
+
+\end{chunk}
+
+\index{Dolzmann, A.}
+\index{Seidl, A.}
+\index{Sturm, T.}
+\begin{chunk}{axiom.bib}
+@misc{Dolz04,
+ author = "Dolzmann, A. and Seidl, A. and Sturm, T.",
+ title = "Redlog User Manual",
+ year = "2004",
+ comment = "Edition 3.0",
+ link = "\url{http://www.reducealgebra.com/reduce38docs/redlog.pdf}",
+ paper = "Dolz04.pdf"
+}
+
+\end{chunk}
+
+\index{Van Hamelen, Frank}
+\begin{chunk}{axiom.bib}
+@misc{Hame89,
+ author = "Van Hamelen, Frank",
+ title = "The CLAM Proof Planner",
+ year = "1989",
+ publisher = "Dept. of AI, Univ. of Edinburgh"
+}
+
+\end{chunk}
+
+\index{Gordon, Mike J.C.}
+\index{Melham, T.F.}
+\begin{chunk}{axiom.bib}
+@book{Gord93,
+ author = "Gordon, Mike J.C. and Melham, T.F.",
+ title = "Introduction to HOL: A Theorem Proving Environment for Higher
+ Order Logic",
+ link = "\url{http://www.cs.ox.ac.uk/tom.melham/pub/Gordon1993ITH.html}",
+ publisher = "Cambridge University Press",
+ year = "1993",
+ isbn = "0521441897"
+}
+
+\end{chunk}
+
+\index{Constable, R.L.}
+\index{Allen, S.F.}
+\index{Bromley, H.M.}
+\index{Cremer, J.F.}
+\index{Harper, R.W.}
+\index{Howe, D.J.}
+\index{Knoblock, T.B.}
+\index{Mendler, N.P.}
+\index{Panagaden, P.}
+\index{Tsaaki, J.T.}
+\index{Smith, S.F.}
+\begin{chunk}{axiom.bib}
+@book{Cons85,
+ author = "Constable, R.L. and Allen, S.F. and Bromley, H.M. and Cremer, J.F.
+ and Harper, R.W. and Howe, D.J. and Knoblock, T.B. and
+ Mendler, N.P. and Panagaden, P. and Tsaaki, J.T. and Smith, S.F.",
+ title = "Implementing Mathematics with The Nuprl Proof Development System",
+ publisher = "PrenticeHall",
+ year = "1985"
+}
+
+\end{chunk}
+
+\index{Boyer, R.S.}
+\index{Moore, J.S.}
+\begin{chunk}{axiom.bib}
+@book{Boye88,
+ author = "Boyer, R.S. and Moore, J.S.",
+ title = "A Computational Logic Handbook",
+ publisher = "Academic Press",
+ year = "1988"
+}
+
+\end{chunk}
+
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@misc{Paul98,
+ author = "Paulson, Lawrence C.",
+ title = "Introduction to Isabelle",
+ publisher = "Computer Laboratory, Univ. of Cambridge",
+ year = "1998"
+}
+
+\end{chunk}
+
+\index{Seger, C.}
+\incdex{Joyce, J.J.}
+\begin{chunk}{axiom.bib}
+@techreport{Sege91,
+ author = "Seger, C. and Joyce, J.J.",
+ title = "A Twolevel Formal Verification Methodology using HOL and COSMOS",
+ type = "technical report",
+ year = "1991",
+ number = "9110",
+ institution = "Dept. of Comp. Sci. Univ. of British Columbia",
+ abstract =
+ "Theoremproving and symbolic simulation are both described as methods
+ for the formal verification of hardware. They are both used to achieve
+ a common goal  correctly designed hardware  and both are intended
+ to be an alternative to conventional methods based on nonexhaustive
+ simulation. However, they have different strengths and weaknesses. The
+ main significance of this paper  and its most original contribution
+  is the suggestion that symbolic simulation and theoremproving can
+ be combined in a complementary manner. We also outline our plans for
+ the development of a mathematical interface between the two approaches
+  in particular, a semantic link between the formulation of
+ higherorder logic used in the Cambridge HOL system and the
+ specification language used in the COSMOS system. We believe that this
+ combination offers great potential as a practical formal verification
+ methodology which combines the ability to accurately model circuit
+ level behavior with the ability to reason about digital hardware at
+ higher levels of abstraction"
+}
+
+\end{chunk}
+
+\index{Backus, John}
+\begin{chunk}{axiom.bib}
+@techreport{Back73,
+ author = "Backus, John",
+ title = "Programming Language Semantics and Closed Applicative Language",
+ type = "technical report",
+ institution = "IBM",
+ number = "RJ 1245",
+ year = "1973"
+}
+
+\end{chunk}
+
+\index{Howe, Douglas J.}
+\begin{chunk}{axiom.bib}
+@article{Howe88,
+ author = "Howe, Douglas J.",
+ title = "Computational Metatheory in Nuprl",
+ journal = "LNCS",
+ volume = "310",
+ pages = "238257",
+ year = "1988",
+ publisher = "SpringerVerlag",
+ abstract =
+ "This paper describes an implementation within Nuprl of mechanisms
+ that support the use of Nuprl's type theory as a language for
+ constructing theoremprovind procedures. The main componenet of the
+ implementation is a large library of definitions, theorems and
+ proofs. This library may be regarded as the beginning of a book of
+ formal mathematics; it contains the formal development and explanation
+ of a useful subset of Nuprl's metatheory, and of a mechanism for
+ translating results established about this embedded metatheory to the
+ object level. Nuprl's rich type theory, besides permitting the
+ internal development of this partial reflection mechanism, allows us
+ to make abstractions that drastically reduce the burden of
+ establishing the correctness of new theoremproving procedures. Our
+ library includes a formally verified termrewriting system"
+}
+
+\end{chunk}
+
+\index{Pelletier, Francis Jeffry}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pell91,
+ author = "Pelletier, Francis Jeffry",
+ title = "The Philosophy of Automated Theorem Proving",
+ booktitle = "Proc 12th IJCAI",
+ pages = "538543",
+ year = "1991",
+ publisher = "Morgan Kaufmann",
+ paper = "Pell91.pdf"
+}
+
+\end{chunk}
+
+\index{Smith, Brian Cantwell}
+\begin{chunk}{axiom.bib}
+@misc{Smit60,
+ author = "Smith, Brian Cantwell",
+ title = "The Limits of Correctness",
+ year = "1960",
+ link = "\url{http://eliza.newhaven.edu/ethics/Resources/14.ReliabilityResponsibility/LimitsOfCorrectness.pdf}",
+ paper = "Smit60.pdf"
+}
+
+\end{chunk}
+
+\index{Naumowicz, Adam}
+\begin{chunk}{axiom.bib}
+@article{Naum06,
+ author = "Naumowicz, Adam",
+ title = "An Example of Formalizing Recent Mathematical Results in Mizar",
+ journal = "Journal of Applied Logic",
+ volume = "4",
+ number = "4",
+ year = "2006",
+ pages = "396413",
+ abstract =
+ "This paper describes an example of the successful formalization of
+ quite advanced and new mathematics using the Mizar system. It shows
+ that although much effort is required to formalize nontrivial facts in
+ a formal computer deduction system, still it is possible to obtain the
+ level of full logical correctness of all inference steps. We also
+ discuss some problems encountered during the formalization, and try to
+ point out some of the features of the Mizar system responsible for
+ that. The formalization described in this paper allows also for
+ contrasting the linguistic capability of the Mizar language and some
+ of the phrases commonly used in “informal” mathematical papers that
+ the Mizar system lacks, and consequently presents the methods of how
+ to cope with it during the formalization. Yet, apart from the
+ problems, this paper shows some definite benefits from using a formal
+ computer system in the work of a mathematician.",
+ paper = "Naum06.pdf"
+}
+
+\end{chunk}
+
+\index{Wiedijk, Freek}
+\begin{chunk}{axiom.bib}
+@misc{Wied07,
+ author = "Wiedijk, Freek",
+ title = "The Seventeen Provers of the World",
+ link = "\url{http://www.cs.kun.nl/~freek/comparison/comparison.pdf}",
+ year = "2007",
+ abstract =
+ "We compare the styles of several proof assistants for mathematics.
+ We present Pythagoras' proof of the irrationality of $\sqrt{2}$ both
+ informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq,
+ (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX,
+ (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl,
+ (15) $\Omega$mega, (16) B method, (17) Minlog",
+ paper = "Wied07.pdf"
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@misc{QED94,
+ author = "Anonymous",
+ title = "The QED Manifesto",
+ link = "\url{}",
+ paper = "QED94.txt"
+}
+
+\end{chunk}
+
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@book{Paul94,
+ author = "Paulson, Lawrence C.",
+ title = "ISABELLE: A Generic Theorem Prover",
+ year = "1994",
+ publisher = "Springer",
+ isbn = "9783540582441",
+}
+
+\end{chunk}
+
+\index{Cannon, John}
+\index{Bosma, Wieb}
+\begin{chunk}{axiom.bib}
+@book{Cann05,
+ author = "Cannon, John and Bosma, Wieb",
+ title = "Handbook of Magma Functions",
+ year = "2005",
+ publisher = "University of Sydney, School of Math and Statistics"
+}
+
+\end{chunk}
+
+\index{Kajler, Norbert}
+\index{Soiffer, Neil}
+\begin{chunk}{axiom.bib}
+@article{Kajl98,
+ author = "Kajler, Norbert and Soiffer, Neil",
+ title = "A Survey of User Interfaces for Computer Algebra Systems",
+ journal = "J. Symbolic Computation",
+ volume = "25",
+ pages = "127159",
+ year = "1998",
abstract =
 "This paper summarizes the results of an investigation into single
 axioms for groups, both ordinary and Abelian, with each of following
 six sets of operations: \{product, inverse\}, \{division\}, \{double
 division, identity\}, \{double division, inverse\}, \{division,
 identity\} , and \{division, inverse\}. In all but two of the twelve
 corresponding theories, we present either the rst single axioms known
 to us or single axioms shorter than those previously known to us. The
 automated theoremproving program Otter was used extensively to
 construct sets of candidate axioms and to search for and nd proofs
 that given candidate axioms are in fact single axioms.",
 paper = "Mccu93.pdf"
+ "This paper surveys work within the Computer Algebra community (and
+ elsewhere) directed towards improving user interfaces for scientific
+ computation during the period 19631994. It is intended to be useful
+ to two groups of people: those who wish to know what work has been
+ done and those who would like to do work in the field. It contains an
+ extensive bibliography to assist readers in exploring the field in more
+ depth. Work related to improving human interaction with computer
+ algebra systems is the main focus of the paper. However, the paper
+ includes additional materials on some closely related issues such as
+ structured document editing, graphics, and communication protocols.",
+ paper = "Kajl98.pdf"
}
\end{chunk}

diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 51c9f2d..315f5af 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5838,6 +5838,8 @@ books/Makefile temp fix for signature sorting
books/*.pamphlet eliminate redundant index in toc
20171011.01.tpd.patch
books/bookvolbib Proving Axiom Correct references
+20171016.01.tpd.patch
+books/bookvolbib Proving Axiom Correct references

1.9.1