From 87e74f2a35a0d3a6a0738c27f6eb117c5ac3daaf Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 27 Nov 2017 20:45:49 0500
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Hamlet, Dick}
\begin{chunk}{axiom.bib}
@inproceedings{Haml02,
author = "Hamlet, Dick",
title = {{Continuity in Software Systems}},
booktitle = "ISSTA 2002 Int. Symp. on Software Testing and Analysis",
pages = "196200",
year = "2002",
}
\end{chunk}
\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
@inproceedings{Fate90a,
author = "Fateman, Richard J.",
title = {{Advances and Trends in the Design of Algebraic
Manipulation Systems}},
booktitle = "Proc. ISSAC'90",
pages = "6067",
year = "1990"
}
\end{chunk}
\index{Beeson, M.}
\begin{chunk}{axiom.bib}
@article{Bees92,
author = "Beeson, M.",
title = {{Mathpert: Computer support for learning algebra, trig, and
calculus}},
journal = "LNCS",
volume = "624",
pages = "454456",
year = "1992",
abstract =
"Mathpert is a computerized environment for learning algebra, trig,
and onevariable calculus. It permits students to direct the
stepbystep solution of problems, and is capable of helping them
by solving the problems itself if necessary.",
paper = "Bees92.pdf"
}
\end{chunk}
\index{Dijkstra, Edsger}
\begin{chunk}{axiom.bib}
@misc{Dijk72,
author = "Dijkstra, Edsger",
title = {{The Humble Programmer}},
year = "1972",
number = "EWD340",
comment = "ACM Turing Lecture 1972",
paper = "Dijk72.txt"
}
\end{chunk}
\index{Suppes, Patrick}
\index{Smith, Robert}
\index{Beard, Marian}
\begin{chunk}{axiom.bib}
@article{Supp77,
author = "Suppes, Patrick and Smith, Robert and Beard, Marian",
title = {{UniversityLevel ComputerAssisted Instruction at Stanford: 1975}},
journal = "Instructional Science",
volume = "6",
year = "1977",
pages = "151185",
abstract =
"This article provides an overview of current work on universitylevel
computer assisted instruction at Stanford University. Brief
descriptions are given of the main areas of current interest. The
main emphasis is on the courses now being used: Introduction to Logic,
Axiomatic Set Theory, Old Church Slavonic, History of the Russian
Literary Language, Introduction to Bulgarian, Introduction to BASIC,
Introduction to LISP, and various courses in music.",
paper = "Supp77.pdf"
}
\end{chunk}
\index{Char, B.W.}
\index{Geddes, K.O.}
\index{Gonnet, G.H.}
\index{Leong, B.L.}
\index{Monagan, M.B.}
\index{Watt, S.M.}
\begin{chunk}{axiom.bib}
@book{Char92,
author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
and Monagan, M.B. and Watt, S.M.",
title = {{A Tutorial Introduction to Maple V}},
year = "1992",
publisher = "SpringerVerlag"
}
\end{chunk}
\index{Harrison, John}
\begin{chunk}{axiom.bib}
@article{Harr94a,
author = "Harrison, John",
title = {{Constructing the Real Numbers in HOL}},
journal = "Formal Methods in Systems Design",
volume = "5",
pages = "3539",
year = "1994",
abstract =
"This paper describes a construction of the real numbers in the HOL
theoremprover by strictly definitional means using a version of
Dedekind's method. It also outlines the theory of mathematical
analysis that has been built on top of it and discusses current and
potential applications in verification and computer algebra.",
paper = "Harr94a.pdf"
}
\end{chunk}
\index{Gordon, M.}
\index{Melham, T.}
\begin{chunk}{axiom.bib}
@book{Gord93,
author = "Gordon, M. and Melham, T.",
title = {{Introduction to HOL}},
publisher = "Cambridge University Press",
year = "1993"
}
\end{chunk}
\index{Igarashi, Shigeru}
\index{London, Ralph L.}
\index{Luckham, David C.}
\begin{chunk}{axiom.bib}
@article{Igar75,
author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
titile = {{Automatic Program Verification I: A Logical Basis and Its
Implementation}},
journal = "Acta Informatica",
volume = "4",
number = "2",
pages = "145182",
year = "1975",
abstract =
"Defining the semantics of programming languages by axioms and rules
of inference yields a deduction system within which proofs may be
given that programs satisfy specifications. The deduction system
herein is shown to be consistent and also deduction complete with
respect to Hoare's system. A subgoaler for the deduction system is
described whose input is a significant subset of Pascal programs plus
inductive assertions. The output is a set of verification conditions
or lemmas to be proved. Several nontrivial arithmetic and sorting
programs have been shown to satisfy specifications by using an
interactive theorem prover to automatically generate proofs of the
verification conditions. Additional components for a more powerful
verification system are under construction.",
paper = "Igar75.pdf"
}
\end{chunk}
\index{Deutsch, L. Peter}
\begin{chunk}{axiom.bib}
@phdthesis{Deut73,
author = "Deutsch, L. Peter",
title = {{An Interactive Program Verifer}},
institution = "University of California, Berkeley",
year = "1973",
paper = "Deut73.pdf"
}
\end{chunk}
\index{King, James Cornelius}
\begin{chunk}{axiom.bib}
@phdthesis{King70,
author = "King, James Cornelius",
title = {{A Program Verifier}},
institution = "Carnegie Mellon University",
year = "1970"
}
\end{chunk}
\index{Good, Donald I.}
\index{London, Ralph L.}
\index{Bledsoe, W.W.}
\begin{chunk}{axiom.bib}
@article{Good75,
author = "Good, Donald I. and London, Ralph L. and Bledsoe, W.W.",
title = {{An Interactive Program Verification System}},
journal = "SIGPLAN Notices",
volume = "10",
number = "6",
pages = "482492",
year = "1975",
abstract =
"This paper is an initial progress report on the development of an
interactive system for verifying that computer programs meet given
formal specifications. The system is based on the conventional
inductive assertion method: given a program and its specifications,
the object is to generate the verification conditions, simplify them,
and prove what remains. The important feature of the system is that
the human user has the opportunity and obligation to help actively in
the simplifying and proving. The user, for example, is the primary
source of problem domain facts and properties needed in the proofs. A
general description is given of the overall design philosophy,
structure, and functional components of the system, and a simple
sorting program is used to illustrate both the behavior of major
system components and the type of user interaction the system provides.",
paper = "Good75.pdf"
}
\end{chunk}
\index{Bledsoe, W.W.}
\index{Bruell, Peter}
\begin{chunk}{axiom.bib}
@article{Bled74,
author = "Bledsoe, W.W. and Bruell, Peter",
title = {{A ManMachine TheoremProving System}},
journal = "Artificial Intelligence",
volume = "5",
number = "1",
pages = "5172",
year = "1974",
abstract =
"This paper describes a manmachine theoremproving system at the
University of Texas at Austin which has been used to prove a few
theorems in general topology. The theorem (or subgoal) being proved is
presented on the scope in its natural form so that the user can easily
comprehend it and, by a series of interactive commands, can help with
the proof when he desires. A feature called DETAIL is employed which
allows the human to interact only when needed and only to the extent
necessary for the proof.
The program is built around a modified form of IMPLY, a
naturaldeductionlike theorem proving technique which has been
described earlier.",
paper = "Bled74.pdf"
}
\end{chunk}

books/axiom.bib  173 ++++++++++
books/bookvolbib.pamphlet  233 +++++++++++++
changelog  4 +
patch  738 ++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 587 insertions(+), 563 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 45a0383..25177fa 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 7493,6 +7493,22 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Bees92,
+ author = "Beeson, M.",
+ title = {{Mathpert: Computer support for learning algebra, trig, and
+ calculus}},
+ journal = "LNCS",
+ volume = "624",
+ pages = "454456",
+ year = "1992",
+ abstract =
+ "Mathpert is a computerized environment for learning algebra, trig,
+ and onevariable calculus. It permits students to direct the
+ stepbystep solution of problems, and is capable of helping them
+ by solving the problems itself if necessary.",
+ paper = "Bees92.pdf"
+}
+
@misc{Beesxx,
author = "Beeson, Michael",
title = {{Automatic Generation of EpsilonDelta Proofs of Continuity}},
@@ 7617,6 +7633,30 @@ paper = "Brea89.pdf"
}
+@article{Bled74,
+ author = "Bledsoe, W.W. and Bruell, Peter",
+ title = {{A ManMachine TheoremProving System}},
+ journal = "Artificial Intelligence",
+ volume = "5",
+ number = "1",
+ pages = "5172",
+ year = "1974",
+ abstract =
+ "This paper describes a manmachine theoremproving system at the
+ University of Texas at Austin which has been used to prove a few
+ theorems in general topology. The theorem (or subgoal) being proved is
+ presented on the scope in its natural form so that the user can easily
+ comprehend it and, by a series of interactive commands, can help with
+ the proof when he desires. A feature called DETAIL is employed which
+ allows the human to interact only when needed and only to the extent
+ necessary for the proof.
+
+ The program is built around a modified form of IMPLY, a
+ naturaldeductionlike theorem proving technique which has been
+ described earlier.",
+ paper = "Bled74.pdf"
+}
+
@techreport{Bled79,
author = "Bledsoe, W.W. and Bruell, P. and Shostak, R.",
title = {{A Prover for General Inequalities}},
@@ 8812,6 +8852,15 @@ paper = "Brea89.pdf"
isbn = "9780387904412"
}
+@misc{Dijk72,
+ author = "Dijkstra, Edsger",
+ title = {{The Humble Programmer}},
+ year = "1972",
+ number = "EWD340",
+ comment = "ACM Turing Lecture 1972",
+ paper = "Dijk72.txt"
+}
+
@book{Dijk76,
author = "Dijkstra, Edsger",
title = {{A Discipline of Programming}},
@@ 9403,6 +9452,31 @@ paper = "Brea89.pdf"
paper = "Gogu06.pdf"
}
+@article{Good75,
+ author = "Good, Donald I. and London, Ralph L. and Bledsoe, W.W.",
+ title = {{An Interactive Program Verification System}},
+ journal = "SIGPLAN Notices",
+ volume = "10",
+ number = "6",
+ pages = "482492",
+ year = "1975",
+ abstract =
+ "This paper is an initial progress report on the development of an
+ interactive system for verifying that computer programs meet given
+ formal specifications. The system is based on the conventional
+ inductive assertion method: given a program and its specifications,
+ the object is to generate the verification conditions, simplify them,
+ and prove what remains. The important feature of the system is that
+ the human user has the opportunity and obligation to help actively in
+ the simplifying and proving. The user, for example, is the primary
+ source of problem domain facts and properties needed in the proofs. A
+ general description is given of the overall design philosophy,
+ structure, and functional components of the system, and a simple
+ sorting program is used to illustrate both the behavior of major
+ system components and the type of user interaction the system provides.",
+ paper = "Good75.pdf"
+}
+
@misc{Gord96,
author = "Gordon, Mike",
title = {{From LCF to HOL: a short history}},
@@ 9569,6 +9643,22 @@ paper = "Brea89.pdf"
paper = "Harr93.pdf"
}
+@article{Harr94a,
+ author = "Harrison, John",
+ title = {{Constructing the Real Numbers in HOL}},
+ journal = "Formal Methods in Systems Design",
+ volume = "5",
+ pages = "3539",
+ year = "1994",
+ abstract =
+ "This paper describes a construction of the real numbers in the HOL
+ theoremprover by strictly definitional means using a version of
+ Dedekind's method. It also outlines the theory of mathematical
+ analysis that has been built on top of it and discusses current and
+ potential applications in verification and computer algebra.",
+ paper = "Harr94a.pdf"
+}
+
@inproceedings{Harr94,
author = "Harrison, John and Thery, Laurent",
title = {{Extending the HOL Thoerem Prover with a Computer Algebra System
@@ 23218,6 +23308,14 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@phdthesis{Deut73,
+ author = "Deutsch, L. Peter",
+ title = {{An Interactive Program Verifer}},
+ institution = "University of California, Berkeley",
+ year = "1973",
+ paper = "Deut73.pdf"
+}
+
@InProceedings{Dewa92,
author = "Dewar, Michael C.",
title = {{Using Computer Algebra to Select Numerical Algorithms}},
@@ 25936,6 +26034,31 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Igar75,
+ author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
+ titile = {{Automatic Program Verification I: A Logical Basis and Its
+ Implementation}},
+ journal = "Acta Informatica",
+ volume = "4",
+ number = "2",
+ pages = "145182",
+ year = "1975",
+ abstract =
+ "Defining the semantics of programming languages by axioms and rules
+ of inference yields a deduction system within which proofs may be
+ given that programs satisfy specifications. The deduction system
+ herein is shown to be consistent and also deduction complete with
+ respect to Hoare's system. A subgoaler for the deduction system is
+ described whose input is a significant subset of Pascal programs plus
+ inductive assertions. The output is a set of verification conditions
+ or lemmas to be proved. Several nontrivial arithmetic and sorting
+ programs have been shown to satisfy specifications by using an
+ interactive theorem prover to automatically generate proofs of the
+ verification conditions. Additional components for a more powerful
+ verification system are under construction.",
+ paper = "Igar75.pdf"
+}
+
@article{Jacq97,
author = "Jacquemard, Alain and KhechichineMourtada, F.Z. and Mourtada, A.",
title = {{Formal algorithms applied to the study of the cyclicity of a
@@ 26941,6 +27064,13 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
+@phdthesis{King70,
+ author = "King, James Cornelius",
+ title = {{A Program Verifier}},
+ institution = "Carnegie Mellon University",
+ year = "1970"
+}
+
@article{Kocb96,
author = "Kocbach, Ladislav and Liska, Richard",
title = {{Generation and Verification of Algorithms for Symbolic\_Numeric
@@ 32334,6 +32464,14 @@ paper = "Brea89.pdf"
pages = "95101",
}
+@book{Char92,
+ author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
+ and Monagan, M.B. and Watt, S.M.",
+ title = {{A Tutorial Introduction to Maple V}},
+ year = "1992",
+ publisher = "SpringerVerlag"
+}
+
@article{Cher80,
author = "Cherlin, Gregory",
title = {{Rings of Continuous Functions: Decision Problems}},
@@ 32861,6 +32999,15 @@ paper = "Brea89.pdf"
paper = "Eras11.pdf"
}
+@inproceedings{Fate90a,
+ author = "Fateman, Richard J.",
+ title = {{Advances and Trends in the Design of Algebraic
+ Manipulation Systems}},
+ booktitle = "Proc. ISSAC'90",
+ pages = "6067",
+ year = "1990"
+}
+
@misc{Fate08,
author = "Fateman, Richard J.",
title = {{Revisiting numeric/symbolic indefinite integration of rational
@@ 33183,6 +33330,14 @@ paper = "Brea89.pdf"
month = "Septembre"
}
+@inproceedings{Haml02,
+ author = "Hamlet, Dick",
+ title = {{Continuity in Software Systems}},
+ booktitle = "ISSTA 2002 Int. Symp. on Software Testing and Analysis",
+ pages = "196200",
+ year = "2002",
+}
+
@inproceedings{Harr07,
author = "Harrison, John",
title = {{A Short Survey of Automated Reasoning}},
@@ 35194,6 +35349,24 @@ paper = "Brea89.pdf"
year = "1993"
}
+@article{Supp77,
+ author = "Suppes, Patrick and Smith, Robert and Beard, Marian",
+ title = {{UniversityLevel ComputerAssisted Instruction at Stanford: 1975}},
+ journal = "Instructional Science",
+ volume = "6",
+ year = "1977",
+ pages = "151185",
+ abstract =
+ "This article provides an overview of current work on universitylevel
+ computer assisted instruction at Stanford University. Brief
+ descriptions are given of the main areas of current interest. The
+ main emphasis is on the courses now being used: Introduction to Logic,
+ Axiomatic Set Theory, Old Church Slavonic, History of the Russian
+ Literary Language, Introduction to Bulgarian, Introduction to BASIC,
+ Introduction to LISP, and various courses in music.",
+ paper = "Supp77.pdf"
+}
+
@article{Supp89,
author = "Suppes, P. and Takahashi, S.",
title = {{An Interactive Calculus Theoremprover for Continuity
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index ee0dca5..6585628 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 10183,6 +10183,26 @@ when shown in factored form.
\end{chunk}
+\index{Beeson, M.}
+\begin{chunk}{axiom.bib}
+@article{Bees92,
+ author = "Beeson, M.",
+ title = {{Mathpert: Computer support for learning algebra, trig, and
+ calculus}},
+ journal = "LNCS",
+ volume = "624",
+ pages = "454456",
+ year = "1992",
+ abstract =
+ "Mathpert is a computerized environment for learning algebra, trig,
+ and onevariable calculus. It permits students to direct the
+ stepbystep solution of problems, and is capable of helping them
+ by solving the problems itself if necessary.",
+ paper = "Bees92.pdf"
+}
+
+\end{chunk}
+
\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@misc{Beesxx,
@@ 10338,6 +10358,35 @@ when shown in factored form.
\end{chunk}
\index{Bledsoe, W.W.}
+\index{Bruell, Peter}
+\begin{chunk}{axiom.bib}
+@article{Bled74,
+ author = "Bledsoe, W.W. and Bruell, Peter",
+ title = {{A ManMachine TheoremProving System}},
+ journal = "Artificial Intelligence",
+ volume = "5",
+ number = "1",
+ pages = "5172",
+ year = "1974",
+ abstract =
+ "This paper describes a manmachine theoremproving system at the
+ University of Texas at Austin which has been used to prove a few
+ theorems in general topology. The theorem (or subgoal) being proved is
+ presented on the scope in its natural form so that the user can easily
+ comprehend it and, by a series of interactive commands, can help with
+ the proof when he desires. A feature called DETAIL is employed which
+ allows the human to interact only when needed and only to the extent
+ necessary for the proof.
+
+ The program is built around a modified form of IMPLY, a
+ naturaldeductionlike theorem proving technique which has been
+ described earlier.",
+ paper = "Bled74.pdf"
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
\index{Bruell, P.}
\index{Shostak, R.}
\begin{chunk}{axiom.bib}
@@ 11934,6 +11983,19 @@ when shown in factored form.
\index{Dijkstra, Edsger}
\begin{chunk}{axiom.bib}
+@misc{Dijk72,
+ author = "Dijkstra, Edsger",
+ title = {{The Humble Programmer}},
+ year = "1972",
+ number = "EWD340",
+ comment = "ACM Turing Lecture 1972",
+ paper = "Dijk72.txt"
+}
+
+\end{chunk}
+
+\index{Dijkstra, Edsger}
+\begin{chunk}{axiom.bib}
@book{Dijk76,
author = "Dijkstra, Edsger",
title = {{A Discipline of Programming}},
@@ 12700,6 +12762,37 @@ when shown in factored form.
\end{chunk}
+\index{Good, Donald I.}
+\index{London, Ralph L.}
+\index{Bledsoe, W.W.}
+\begin{chunk}{axiom.bib}
+@article{Good75,
+ author = "Good, Donald I. and London, Ralph L. and Bledsoe, W.W.",
+ title = {{An Interactive Program Verification System}},
+ journal = "SIGPLAN Notices",
+ volume = "10",
+ number = "6",
+ pages = "482492",
+ year = "1975",
+ abstract =
+ "This paper is an initial progress report on the development of an
+ interactive system for verifying that computer programs meet given
+ formal specifications. The system is based on the conventional
+ inductive assertion method: given a program and its specifications,
+ the object is to generate the verification conditions, simplify them,
+ and prove what remains. The important feature of the system is that
+ the human user has the opportunity and obligation to help actively in
+ the simplifying and proving. The user, for example, is the primary
+ source of problem domain facts and properties needed in the proofs. A
+ general description is given of the overall design philosophy,
+ structure, and functional components of the system, and a simple
+ sorting program is used to illustrate both the behavior of major
+ system components and the type of user interaction the system provides.",
+ paper = "Good75.pdf"
+}
+
+\end{chunk}
+
\index{Gordon, Mike}
\begin{chunk}{axiom.bib}
@misc{Gord96,
@@ 12931,6 +13024,26 @@ when shown in factored form.
\end{chunk}
\index{Harrison, John}
+\begin{chunk}{axiom.bib}
+@article{Harr94a,
+ author = "Harrison, John",
+ title = {{Constructing the Real Numbers in HOL}},
+ journal = "Formal Methods in Systems Design",
+ volume = "5",
+ pages = "3539",
+ year = "1994",
+ abstract =
+ "This paper describes a construction of the real numbers in the HOL
+ theoremprover by strictly definitional means using a version of
+ Dedekind's method. It also outlines the theory of mathematical
+ analysis that has been built on top of it and discusses current and
+ potential applications in verification and computer algebra.",
+ paper = "Harr94a.pdf"
+}
+
+\end{chunk}
+
+\index{Harrison, John}
\index{Th\'ery, Laurent}
\begin{chunk}{axiom.bib}
@inproceedings{Harr94,
@@ 32725,6 +32838,18 @@ May 1984
\end{chunk}
+\index{Deutsch, L. Peter}
+\begin{chunk}{axiom.bib}
+@phdthesis{Deut73,
+ author = "Deutsch, L. Peter",
+ title = {{An Interactive Program Verifer}},
+ institution = "University of California, Berkeley",
+ year = "1973",
+ paper = "Deut73.pdf"
+}
+
+\end{chunk}
+
\index{d01ajfAnnaType}
\index{d01akfAnnaType}
\index{d01alfAnnaType}
@@ 36932,6 +37057,37 @@ SpringerVerlag, Berlin, Germany / Heildelberg, Germany / London, UK / etc.,
\subsection{I} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Igarashi, Shigeru}
+\index{London, Ralph L.}
+\index{Luckham, David C.}
+\begin{chunk}{axiom.bib}
+@article{Igar75,
+ author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
+ titile = {{Automatic Program Verification I: A Logical Basis and Its
+ Implementation}},
+ journal = "Acta Informatica",
+ volume = "4",
+ number = "2",
+ pages = "145182",
+ year = "1975",
+ abstract =
+ "Defining the semantics of programming languages by axioms and rules
+ of inference yields a deduction system within which proofs may be
+ given that programs satisfy specifications. The deduction system
+ herein is shown to be consistent and also deduction complete with
+ respect to Hoare's system. A subgoaler for the deduction system is
+ described whose input is a significant subset of Pascal programs plus
+ inductive assertions. The output is a set of verification conditions
+ or lemmas to be proved. Several nontrivial arithmetic and sorting
+ programs have been shown to satisfy specifications by using an
+ interactive theorem prover to automatically generate proofs of the
+ verification conditions. Additional components for a more powerful
+ verification system are under construction.",
+ paper = "Igar75.pdf"
+}
+
+\end{chunk}
+
\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Jacob, G.}
@@ 38593,6 +38749,17 @@ SIGSAM Communications in Computer Algebra, 157 2006
\end{chunk}
+\index{King, James Cornelius}
+\begin{chunk}{axiom.bib}
+@phdthesis{King70,
+ author = "King, James Cornelius",
+ title = {{A Program Verifier}},
+ institution = "Carnegie Mellon University",
+ year = "1970"
+}
+
+\end{chunk}
+
\index{Kocbach, Ladislav}
\index{Liska, Richard}
\begin{chunk}{axiom.bib}
@@ 47686,6 +47853,23 @@ GauthierVillars, Paris, 1891).
\end{chunk}
+\index{Char, B.W.}
+\index{Geddes, K.O.}
+\index{Gonnet, G.H.}
+\index{Leong, B.L.}
+\index{Monagan, M.B.}
+\index{Watt, S.M.}
+\begin{chunk}{axiom.bib}
+@book{Char92,
+ author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
+ and Monagan, M.B. and Watt, S.M.",
+ title = {{A Tutorial Introduction to Maple V}},
+ year = "1992",
+ publisher = "SpringerVerlag"
+}
+
+\end{chunk}
+
\index{Cherlin, Gregory}
\begin{chunk}{axiom.bib}
@article{Cher80,
@@ 48797,6 +48981,19 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
+@inproceedings{Fate90a,
+ author = "Fateman, Richard J.",
+ title = {{Advances and Trends in the Design of Algebraic
+ Manipulation Systems}},
+ booktitle = "Proc. ISSAC'90",
+ pages = "6067",
+ year = "1990"
+}
+
+\end{chunk}
+
+\index{Fateman, Richard J.}
+\begin{chunk}{axiom.bib}
@misc{Fate08,
author = "Fateman, Richard J.",
title = {{Revisiting numeric/symbolic indefinite integration of rational
@@ 49681,6 +49878,18 @@ Methuen. (1967)
\end{chunk}
+\index{Hamlet, Dick}
+\begin{chunk}{axiom.bib}
+@inproceedings{Haml02,
+ author = "Hamlet, Dick",
+ title = {{Continuity in Software Systems}},
+ booktitle = "ISSTA 2002 Int. Symp. on Software Testing and Analysis",
+ pages = "196200",
+ year = "2002",
+}
+
+\end{chunk}
+
\index{Harrison, John}
\begin{chunk}{axiom.bib}
@inproceedings{Harr07,
@@ 53337,6 +53546,30 @@ PrenticeHall 1971
\end{chunk}
+\index{Suppes, Patrick}
+\index{Smith, Robert}
+\index{Beard, Marian}
+\begin{chunk}{axiom.bib}
+@article{Supp77,
+ author = "Suppes, Patrick and Smith, Robert and Beard, Marian",
+ title = {{UniversityLevel ComputerAssisted Instruction at Stanford: 1975}},
+ journal = "Instructional Science",
+ volume = "6",
+ year = "1977",
+ pages = "151185",
+ abstract =
+ "This article provides an overview of current work on universitylevel
+ computer assisted instruction at Stanford University. Brief
+ descriptions are given of the main areas of current interest. The
+ main emphasis is on the courses now being used: Introduction to Logic,
+ Axiomatic Set Theory, Old Church Slavonic, History of the Russian
+ Literary Language, Introduction to Bulgarian, Introduction to BASIC,
+ Introduction to LISP, and various courses in music.",
+ paper = "Supp77.pdf"
+}
+
+\end{chunk}
+
\index{Suppes, P.}
\index{Takahashi, S.}
\begin{chunk}{axiom.bib}
diff git a/changelog b/changelog
index 73dd774..9aac25e 100644
 a/changelog
+++ b/changelog
@@ 1,5 +1,7 @@
+20171127 tpd src/axiomwebsite/patches.html 20171127.01.tpd.patch
+20171127 tpd books/bookvolbib add references
20171115 tpd src/axiomwebsite/patches.html 20171115.01.tpd.patch
20171113 tpd books/bookvolbib add references
+20171115 tpd books/bookvolbib add references
20171113 tpd src/axiomwebsite/patches.html 20171113.01.tpd.patch
20171113 tpd books/bookvolbib add references
20171109 tpd src/axiomwebsite/patches.html 20171109.01.tpd.patch
diff git a/patch b/patch
index 0024a85..66b8e8a 100644
 a/patch
+++ b/patch
@@ 2,633 +2,247 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Brown, W.S.}
+\index{Hamlet, Dick}
\begin{chunk}{axiom.bib}
@article{Brow69,
 author = "Brown, W.S.",
 title = {{Rational Exponential Expressions and a Conjecture Concerning
 $\pi$ and $e$}},
 journal = "The American Mathematical Monthly",
 volume = "76",
 number = "1",
 year = "1969",
 pages = "2834",
 abstract =
 "One of the most controversial and least well defined of mathematical
 problems is the problem of simplification. The recent upsurge
 of interest in mechanized mathematics has lent new urgency to this
 problem, but so far very little has been accomplished. This paper
 attempts to shed light on the situation by introducing the class of
 rational exponential expressions, defining simplification within
 this class, and showing constructively how to achieve it. It is shown
 that the only simplified rational exponential expression equivalent to
 0 is 0 itself, provided that an easily stated conjecture is true.
 However the conjecture, if true, will surely be difficult to prove,
 since it asserts as a special case that $\pi$ and $e$ are algebraically
 independent, and no one has yet been able to prove even the much
 weaker conjecture that $\pi+e$ is irrational.",
 paper = "Brow69.pdf"
}

\end{chunk}

\index{Bogen, Richard}
\begin{chunk}{axiom.bib}
@book{Boge77,
 author = "Bogen, Richard",
 title = {{MACSYMA Reference Manual, Version 9}},
 publisher = "MIT",
 year = "1977",
 link = "\url{http://bitsavers.informatik.unistuttgart.de/pdf/mit/macsyma/MACSYMA_RefMan_V9_Dec77.pdf}",
 paper = "Boge77.pdf"
}

\end{chunk}

\index{Schelter, William F.}
\begin{chunk}{axiom.bib}
@book{Sche01,
 author = "Schelter, William F.",
 title = {{Maxima Manual Version 5.41.0}},
 year = "2001",
 publisher = "Sourceforge",
 paper = "Sche01.pdf"
}

\end{chunk}

\index{Farmer, William M.}
\index{Guttman, J.D.}
\index{Thayer, F.J.}
\begin{chunk}{axiom.bib}
@article{Farm95,
 author = "Farmer, William M. and Guttman, J.D. and Thayer, F.J.",
 title = {{Contexts in Mathematical Reasoning and Computation}},
 journal = "J. of Symbolic Computation",
 volume = "19",
 pages = "201216",
 year = "1995",
 abstract =
 "Contexts are sets of formulas used to manage the assumptions that
 arise in the course of a mathematical deduction or
 calculation. Although contextdependent reasoning is commonplace in
 informal mathematics, most contemporary symbolic computation systems
 do not utilize contexts in sophisticated ways. This paper describes
 some contextbased techniques for symbolic computation, including
 techniques for reasoning about definedness, simplifying abstract
 algebraic expressions, and computing with theorems. All of these
 techniques are implemented in the IMPS Interactive Mathematical Proof
 System. The paper also proposes a general mathematics laboratory that
 combines the functionality of current symbolic computation systems
 with the facilities of a theorem proving system like IMPS.",
 paper = "Farm95.pdf"
+@inproceedings{Haml02,
+ author = "Hamlet, Dick",
+ title = {{Continuity in Software Systems}},
+ booktitle = "ISSTA 2002 Int. Symp. on Software Testing and Analysis",
+ pages = "196200",
+ year = "2002",
}
\end{chunk}
\index{Farmer, William M.}
+\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
@article{Farm93b,
 author = "Farmer, William M.",
 title = {{A simple type theory with partial functions and subtypes}},
 journal = "Annals of Pure and Applied Logic",
 volume = "64",
 pages = "211240",
 year = "1993",
 abstract =
 "Simple type theory is a higherorder predicate logic for reasoning
 about truth values, individuals, and simply typed total functions. We
 present in this paper a version of simple type theory, called PF*, in
 which functions may be partial and types may have subtypes. We define
 both a Henkinstyle general models semantics and an axiomatic system
 for PF*, and we prove that the axiomatic system is complete with
 respect to the general models semantics. We also define a notion of
 an interpretation of one PF* theory in another. PF* is intended as a
 foundation for mechanized mathematics. It is the basis for the logic
 of IMPS, an Interactive Mathematical Proof System developed at The
 MITRE Corporation.",
 paper = "Farm93b.pdf"
+@inproceedings{Fate90a,
+ author = "Fateman, Richard J.",
+ title = {{Advances and Trends in the Design of Algebraic
+ Manipulation Systems}},
+ booktitle = "Proc. ISSAC'90",
+ pages = "6067",
+ year = "1990"
}
\end{chunk}
\index{Farmer, William H.}
+\index{Beeson, M.}
\begin{chunk}{axiom.bib}
@article{Farm92,
 author = "Farmer, William H.",
 title = {{Little Theories}},
+@article{Bees92,
+ author = "Beeson, M.",
+ title = {{Mathpert: Computer support for learning algebra, trig, and
+ calculus}},
journal = "LNCS",
 volume = "607",
 year = "1992",
 pages = "567581",
 abstract =
 "In the ``little theories'' version of the axiomatic method, different
 portions of mathematics are developed in various different formal
 axiomatic theories. Axiomatic theories may be related by inclusion or
 by theory interpretation. We argue that the little theories approach
 is a desirable way to formalize mathematics, and we describe how IMPS,
 an Interactive Mathematical Proof System, supports it.",
 paper = "Farm92.pdf"
}

\end{chunk}

\index{Owre, S.}
\index{Rushby, J.M.}
\index{Shankar, N.}
\begin{chunk}{axiom.bib}
@article{Owre92,
 author = "Owre, S. and Rushby, J.M. and Shankar, N.",
 title = {{PVS: A Prototype Verification System}},
 journal = "Lecture Notes in Computer Science",
 volume = "687",
 pages = "748752",
+ volume = "624",
+ pages = "454456",
year = "1992",
abstract =
 "This brief paper introduces the main ideas of PVS",
 paper = "Owre92.pdf"
}

\end{chunk}

\index{Farmer, William H.}
\begin{chunk}{axiom.bib}
@article{Farm92a,
 author = "Farmer, William H.",
 title = {{IMPS: System Description}},
 journal = "Lecture Notes in Computer Science",
 volume = "607",
 pages = "701705",
 year = "1992",
 paper = "Farm92a.pdf"
}

\end{chunk}

\index{Wos, Larry}
\begin{chunk}{axiom.bib}
@article{Wosx92,
 author = "Wos, Larry",
 title = {{The Impossibility of the Automation of Logical Reasoning}},
 journal = "Lecture Notes in Computer Science",
 volume = "607",
 year = "1992",
 pages = "13",
 paper = "Wosx92.pdf"
+ "Mathpert is a computerized environment for learning algebra, trig,
+ and onevariable calculus. It permits students to direct the
+ stepbystep solution of problems, and is capable of helping them
+ by solving the problems itself if necessary.",
+ paper = "Bees92.pdf"
}
\end{chunk}
\index{Craigen, Dan}
\index{Kromodimoeljo, Sentot}
\index{Meisels, Irwin}
\index{Pase, Bill}
\index{Saaltink, Mark}
+\index{Dijkstra, Edsger}
\begin{chunk}{axiom.bib}
@article{Crai92,
 author = "Craigen, Dan and Kromodimoeljo, Sentot and Meisels, Irwin
 and Pase, Bill",
 title = {{Eves System Description}},
 journal = "Lecture Notes in Computer Science",
 volume = "607"
 pages = "771775",
 year = "1992",
 paper = "Crai92.pdf"
+@misc{Dijk72,
+ author = "Dijkstra, Edsger",
+ title = {{The Humble Programmer}},
+ year = "1972",
+ number = "EWD340",
+ comment = "ACM Turing Lecture 1972",
+ paper = "Dijk72.txt"
}
\end{chunk}
\index{Pfenning, Frank}
\index{Rohwedder, Ekkehard}
+\index{Suppes, Patrick}
+\index{Smith, Robert}
+\index{Beard, Marian}
\begin{chunk}{axiom.bib}
@article{Pfen92b,
 author = "Pfenning, Frank and Rohwedder, Ekkehard",
 title = {{Implementing the MetaTheory of Deductive Systems}},
 journal = "Lecture Notes in Computer Science",
 volume = "607"
 pages = "771775",
 year = "1992",
+@article{Supp77,
+ author = "Suppes, Patrick and Smith, Robert and Beard, Marian",
+ title = {{UniversityLevel ComputerAssisted Instruction at Stanford: 1975}},
+ journal = "Instructional Science",
+ volume = "6",
+ year = "1977",
+ pages = "151185",
abstract =
 "We exhibit a methodology for formulating and verifying meta theorems
 about deductive systems in the Elf language, an implementation of the
 LF Logical Framework with an operational semantics in the spirit of
 logic programming. It is based on the mechanical verification of
 properties of transformations between deductions, which relies on type
 reconstruction and schemachecking. The latter is justified by
 induction principles for closed LF objects, which can be constructed
 over a given signature. We illustrate our technique through several
 examples, the most extensive of which is an interpre tation of
 classical logic in minimal logic through a continuationpassingstyle
 transformation on proofs.",
 paper = "Pfen92b.pdf"
}

\end{chunk}

\index{Guttman, J.D.}
\begin{chunk}{axiom.bib}
@techreport{Gutt91,
 author = "Guttman, J.D.",
 title = {{A Propoed Interface Logic for Verification Environments}},
 type = "technical report",
 number = "M9119",
 institution = "The MITRE Corporation",
 year = "1991"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Open11,
 author = "Dos Reis, G.",
 title = {{OpenAxiom}},
 link = "\url{http://www.openaxiom.org}",
 year = "2011"
+ "This article provides an overview of current work on universitylevel
+ computer assisted instruction at Stanford University. Brief
+ descriptions are given of the main areas of current interest. The
+ main emphasis is on the courses now being used: Introduction to Logic,
+ Axiomatic Set Theory, Old Church Slavonic, History of the Russian
+ Literary Language, Introduction to Bulgarian, Introduction to BASIC,
+ Introduction to LISP, and various courses in music.",
+ paper = "Supp77.pdf"
}
\end{chunk}
\index{Matthews, David C.J.}
\index{Wenzel, Makarius}
+\index{Char, B.W.}
+\index{Geddes, K.O.}
+\index{Gonnet, G.H.}
+\index{Leong, B.L.}
+\index{Monagan, M.B.}
+\index{Watt, S.M.}
\begin{chunk}{axiom.bib}
@inproceedings{Matt10,
 author = "Matthews, David C.J. and Wenzel, Makarius",
 title = {{Efficient Parallel Programming in Poly/ML and Isabelle/ML}},
 booktitle = "Proc. 5th ACM SIGPLAN workshop on Declarative aspects of
 multicore programming",
 pages = "5362",
 year = "2010",
 publisher = "ACM",
 isbn = "9781605588599",
 abstract =
 "The ML family of languages and LCFstyle interactive theorem proving
 have been closely related from their beginnings about 30 years
 ago. Here we report on a recent project to adapt both the Poly/ML
 compiler and the Isabelle theorem prover to current multicore
 hardware. Checking theories and proofs in typical Isabelle application
 takes minutes or hours, and users expect to make efficient use of
 ``home machines'' with 28 cores, or more.

 Poly/ML and Isabelle are big and complex software systems that have
 evolved over more than two decades. Faced with the requirement to
 deliver a stable and efficient parallel programming environment, many
 infrastructure layers had to be reworked: from lowlevel system
 threads to highlevel principles of valueoriented programming. At
 each stage we carefully selected from the many existing concepts for
 parallelism, and integrated them in a way that fits smoothly into the
 idea of purely functional ML with the addition of synchronous
 exceptions and asynchronous interrupts.

 From the Isabelle/ML perspective, the main concept to manage parallel
 evaluation is that of ``future values''. Scheduling is implicit, but it
 is also possible to specify dependencies and priorities. In addition,
 blockstructured groups of futures with propagation of exceptions
 allow for alternative functional evaluation (such as parallel search),
 without requiring user code to tackle concurrency. Our library also
 provides the usual parallel combinators for functions on lists, and
 analogous versions on prover tactics.

 Despite substantial reorganization in the background, only minimal
 changes are occasionally required in user ML code, and none at the
 Isabelle application level (where parallel theory and proof processing
 is fully implicit). The present implementation is able to address more
 than 8 cores effectively, while the earlier version of the official
 Isabelle2009 release works best for 24 cores. Scalability beyond 16
 cores still poses some extra challenges, and will require further
 improvements of the Poly/ML runtime system (heap management and
 garbage collection), and additional parallelization of Isabelle
 application logic.",
 paper = "Matt10.pdf"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Poly11a,
 author = "Unknown",
 title = {{Poly/ML}},
 link = "\url{http://www.polyml.org}",
 year = "2011"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Isab11,
 author = "Unknown",
 title = {{Isabell}},
 link = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html}",
 year = "2011"
+@book{Char92,
+ author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
+ and Monagan, M.B. and Watt, S.M.",
+ title = {{A Tutorial Introduction to Maple V}},
+ year = "1992",
+ publisher = "SpringerVerlag"
}
\end{chunk}
\index{Boulm\'e, Sylvain}
+\index{Harrison, John}
\begin{chunk}{axiom.bib}
@techreport{Boul00a,
 author = "Boulme. Sylvain",
 title = {{Specifying in Coq inheritance used in Computer Algebra
 Libraries}},
 year = "2000",
 institution = "LIP6, Paris",
 number = "2000.013",
+@article{Harr94a,
+ author = "Harrison, John",
+ title = {{Constructing the Real Numbers in HOL}},
+ journal = "Formal Methods in Systems Design",
+ volume = "5",
+ pages = "3539",
+ year = "1994",
abstract =
 "This paper is part of FOC[3], a project for developing Computer
 Algebra libraries, certified in Coq[2]. FOC has developed a
 methodology for programming Computer Algebra libraries, using modules
 and objects in Ocaml. In order to specify modularity features used by
 FOC in Ocaml, we are coding in Coq a theory for extensible records
 with dependent fields. This theory intends to express especially the
 kind of inheritance with method redefinition and late binding, that
 FOC uses in its Ocaml programs.

 The unit of FOC are coded as records. As we want to encode sematic
 information on units, the fields of our records may be proofs. Thus,
 our fields may depend on each others. We call the
 {\sl Drecords}. Then, we introduce a new datatype, called
 {\sl mixDrec}, to represent FOC classes. Actually, mixDrecs are useful
 for describing a hierarchy of Drecords in an incremental way. In
 mixDrecs, fields can be only declared or they can be
 redefined. MixDrecs can be extended by inheritance.",
 paper = "Boul00a.pdf"
+ "This paper describes a construction of the real numbers in the HOL
+ theoremprover by strictly definitional means using a version of
+ Dedekind's method. It also outlines the theory of mathematical
+ analysis that has been built on top of it and discusses current and
+ potential applications in verification and computer algebra.",
+ paper = "Harr94a.pdf"
}
\end{chunk}
\index{Dennis, Louise A.}
\index{Collins, Graham}
\index{Norrish, Michael}
\index{Boulton, Richard}
\index{Slind, Konrad}
\index{Robinson, Graham}
\index{Gordon, Mike}
\index{Melham, Tom}
+\index{Gordon, M.}
+\index{Melham, T.}
\begin{chunk}{axiom.bib}
@article{Denn00,
 author = "Dennis, Louise A. and Collins, Graham and Norrish, Michael
 and Boulton, Richard and Slind, Konrad and
 Robinson, Graham and Gordon, Mike and Melham, Tom",
 title = {{The PROSPER Toolkit}},
 journal = "LNCS",
 volume = "1785",
 publisher = "SpringerVerlag",
 pages = "7892",
 year = "2000",
 link =
 "\url{https://link.springer.com/content/pdf/10.1007/3540464190_7.pdf}",
 abstract =
 "The PROSPER (Proof and Specification Assisted Design Environments)
 project advocates the use of toolkits which allow existing
 verification tools to be adapted to a more flexible format so that
 they may be treated as components. A system incorporating such tools
 becomes another component that can be embedded in an application. This
 paper describes the PROSPER Toolkit which enables this. The nature of
 communication between components is specified in a
 languageindependent way. It is implemented in several common
 programming languages to allow a wide variety of tools to have access
 to the toolkit.",
 paper = "Denn00.pdf"
+@book{Gord93,
+ author = "Gordon, M. and Melham, T.",
+ title = {{Introduction to HOL}},
+ publisher = "Cambridge University Press",
+ year = "1993"
}
\end{chunk}
\index{Dewar, Mike}
+\index{Igarashi, Shigeru}
+\index{London, Ralph L.}
+\index{Luckham, David C.}
\begin{chunk}{axiom.bib}
@misc{Dewa00,
 author = "Dewar, Mike",
 title = {{Special Issue on OPENMATH}},
 publisher = "ACM SIGPLAN Bulletin",
 volume = "34",
+@article{Igar75,
+ author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
+ titile = {{Automatic Program Verification I: A Logical Basis and Its
+ Implementation}},
+ journal = "Acta Informatica",
+ volume = "4",
number = "2",
 year = "2000"
}

\end{chunk}

\index{Gray, Simon}
\index{Kajler, Norbert}
\index{Wang, Paul S.}
\begin{chunk}{axiom.bib}
@article{Gray98,
 author = "Gray, Simon and Kajler, Norbert and Wang, Paul S.",
 title = {{Design and Implementation of MP, a Protocol for
 Efficient Exchange of Mathematical Expressions}},
 journal = "J. Symboic Computation",
 volume = "25",
 pages = "213237",
 year = "1998",
+ pages = "145182",
+ year = "1975",
abstract =
 "The Multi Project is an ongoing research e ort at Kent State
 University aimed at providing an environment for distributed scientific
 computing. An integral part of this environment is the Multi
 Protocol (MP) which is designed to support ecientific communication of
 mathematical data between scientificallyoriented software tools. MP
 exchanges data in the form of linearized annotated syntax
 trees. Syntax trees provide a simple, flexible and toolindependent
 way to represent and exchange data, and annotations provide a powerful
 and generic expressive facility for transmitting additional
 information. At a level above the data exchange protocol,
 dictionaries provide definitions for operators and constants, providing
 shared semantics across heterogeneous packages. A clear distinction
 between MPdefined and userdefined entities is enforced. Binary
 encodings are used for efficiency. Commonly used values and blocks of
 homogeneous data are further optimized. The protocol is independent of
 the underlying communication paradigm and can support parallel
 computation, distributed problemsolving environments, and the
 coupling of tools for speci c applications.",
 paper = "Gray98.pdf"
+ "Defining the semantics of programming languages by axioms and rules
+ of inference yields a deduction system within which proofs may be
+ given that programs satisfy specifications. The deduction system
+ herein is shown to be consistent and also deduction complete with
+ respect to Hoare's system. A subgoaler for the deduction system is
+ described whose input is a significant subset of Pascal programs plus
+ inductive assertions. The output is a set of verification conditions
+ or lemmas to be proved. Several nontrivial arithmetic and sorting
+ programs have been shown to satisfy specifications by using an
+ interactive theorem prover to automatically generate proofs of the
+ verification conditions. Additional components for a more powerful
+ verification system are under construction.",
+ paper = "Igar75.pdf"
}
\end{chunk}
\index{Harrison, John}
\index{Th\'ery, Laurent}
+\index{Deutsch, L. Peter}
\begin{chunk}{axiom.bib}
@incollection{Harr93,
 author = "Harrison, John and Thery, Laurent",
 title = {{Reasoning about the Reals: The Marriage of HOL and
 Maple}},
 booktitle = "Logic Programming and Automated Reasoning",
 publisher = "SpringerVerlag",
 year = "1993",
 pages = "351353",
 link =
 "\url{https://link.springer.com/content/pdf/10.1007/3540569448_68.pdf}",
 abstract =
 "Computer algebra systems are extremely powerful and flexible, but
 often give results which require careful interpretation or are
 downright incorrect. By contrast, theorem provers are very reliable
 but lack the powerful specialized decision procedures and heuristics
 of computer algebra systems. In this paper we try to get the best of
 both worlds by careful exploitation of a link between a theorem prover
 and a computer algebra system.",
 paper = "Harr93.pdf"
+@phdthesis{Deut73,
+ author = "Deutsch, L. Peter",
+ title = {{An Interactive Program Verifer}},
+ institution = "University of California, Berkeley",
+ year = "1973",
+ paper = "Deut73.pdf"
}
\end{chunk}
\index{Richardson, Daniel}
+\index{King, James Cornelius}
\begin{chunk}{axiom.bib}
@article{Rich69,
 author = "Richardson, Daniel",
 title = {{Some Undecidable Problems involving Elementar Functions of
 a Real Variable}},
 journal = "J. Symbolic Logic",
 volume = "33",
 number = "4",
 year = "1969",
 pages = "514520",
 abstract =
 "Let $E$ be a set of expressions representing real, single valued,
 partially defined functions of one real variable. $E^*$ will be the
 set of functions represented by expressions in $E$. If $A$ is an
 expression in $E$, $A(x)$ is the function denoted by $AA$. It is
 assumed that $D^*$ contains the identity function and the rational
 numbers as constant functions and that $E^*$ is closed under addition,
 subtraction, multiplication, and composition"
+@phdthesis{King70,
+ author = "King, James Cornelius",
+ title = {{A Program Verifier}},
+ institution = "Carnegie Mellon University",
+ year = "1970"
}
\end{chunk}
\index{Rushby, John}
+\index{Good, Donald I.}
+\index{London, Ralph L.}
+\index{Bledsoe, W.W.}
\begin{chunk}{axiom.bib}
@inproceedings{Rush00,
 author = "Rushby, John",
 title = {{Disappearing Formal Methods}},
 booktitle = "High Assurance Systems Engineering, 5th Int. Symp.",
 pages = "9596",
 year = "2000",
 publisher = "ACM",
 paper = "Rush00.pdf"
}

\end{chunk}

\index{Buchberger, B.}
\index{Dupre, C.}
\index{Jebelean, T.}
\index{Kriftner, F.}
\index{Nakagawa, K.}
\index{Vasaru, D.}
\index{Windsteiger, W.}
\begin{chunk}{axiom.bib}
@misc{Buch00,
 author = "Buchberger, B. and Dupre, C. and Jebelean, T. and Kriftner, F.
 and Nakagawa, K. and Vasaru, D. and Windsteiger, W.",
 title = {{The Theorema Project: A Progress Report}},
 year = "2000",
+@article{Good75,
+ author = "Good, Donald I. and London, Ralph L. and Bledsoe, W.W.",
+ title = {{An Interactive Program Verification System}},
+ journal = "SIGPLAN Notices",
+ volume = "10",
+ number = "6",
+ pages = "482492",
+ year = "1975",
abstract =
 "The THEOREMA project aims at supporting, within one consistent logic
 and one coherent software system, the entire mathematical exploration
 cycle including the phase of proving. In this paper we report on some
 of the new features of THEOREMA that have been designed and
 implemented since the first expository version of THEOREMA in
 1997. These features are:  the THEOREMA formal text language  the
 THEOREMA computational sessions  the ProveComputeSolve (PCS) prover
 of THEOREMA  the THEOREMA set theory prover  special provers within
 THEOREMA  the cascademetastrategy for THEOREMA provers  proof
 simplification in THEOREMA. In the conclusion, we formulate design
 goals for the next version of THEOREMA",
 paper = "Buch00.pdf"
}

\end{chunk}

\index{Boyer, Robert S.}
\index{Moore, J Strother}
\begin{chunk}{axiom.bib}
@techreport{Boye85,
 author = "Boyer, Robert S. and Moore, J Strother",
 title = {{Integrating Decision Procedures into Heuristic Theorem Provers}},
 type = "technical report",
 institution = "Inst. for Comp. Sci. University of Texas at Austin",
 number = "ICSCACMP44",
 year = "1985",
+ "This paper is an initial progress report on the development of an
+ interactive system for verifying that computer programs meet given
+ formal specifications. The system is based on the conventional
+ inductive assertion method: given a program and its specifications,
+ the object is to generate the verification conditions, simplify them,
+ and prove what remains. The important feature of the system is that
+ the human user has the opportunity and obligation to help actively in
+ the simplifying and proving. The user, for example, is the primary
+ source of problem domain facts and properties needed in the proofs. A
+ general description is given of the overall design philosophy,
+ structure, and functional components of the system, and a simple
+ sorting program is used to illustrate both the behavior of major
+ system components and the type of user interaction the system provides.",
+ paper = "Good75.pdf"
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
+\index{Bruell, Peter}
+\begin{chunk}{axiom.bib}
+@article{Bled74,
+ author = "Bledsoe, W.W. and Bruell, Peter",
+ title = {{A ManMachine TheoremProving System}},
+ journal = "Artificial Intelligence",
+ volume = "5",
+ number = "1",
+ pages = "5172",
+ year = "1974",
abstract =
 "We discuss the problem of incorporating into a heuristic theorem
 prover a decision procedure for a fragment of the logic. An obvious
 goal when incorporating such a procedure is to reduce the search space
 explored by the heuristic component of the system, as would be
 achieved by eliminating from the systemâ€™s data base some explicitly
 stated axioms. For example, if a decision procedure for linear
 inequalities is added, one would hope to eliminate the explicit
 consideration of the transitivity axioms. However, the decision
 procedure must then be used in all the ways the eliminated axioms
 might have been. The difficulty of achieving this degree of
 integration is more dependent upon the complexity of the heuristic
 component than upon that of the decision procedure. The view of the
 decision procedure as a ``black box'' is frequently destroyed by the
 need pass large amounts of search strategic information back and forth
 between the two components. Finally, the efficiency of the decision
 procedure may be virtually irrelevant; the efficiency of the final
 system may depend most heavily on how easy it is to communicate
 between the two components. This paper is a case study of how we
 integrated a linear arithmetic procedure into a heuristic theorem
 prover. By linear arithmetic here we mean the decidable subset of
 number theory dealing with universally quantified formulas composed of
 the logical connectives, the identity relation, the Peano ``less than''
 relation, the Peano addition and subtraction functions, Peano
 constants, and variables taking on natural values. We describe our
 system as it originally stood, and then describe chronologically the
 evolution of our linear arithmetic procedure and its interface to the
 heuristic theorem prover. We also provide a detailed description of
 our final linear arithmetic procedure and the use we make of it. This
 description graphically illustrates the difference between a
 standalone decision procedure and one that is of use to a more
 powerful theorem prover.",
 paper = "Boye85.pdf"
}

\end{chunk}

\index{Farmer, William M.}
\index{Guttman, Joshua D.}
\index{Fabrega, F. Javier Thayer}
\begin{chunk}{axiom.bib}
@article{Farm96,
 author = "Farmer, William M. and Guttman, Joshua D. and
 Fabrega, F. Javier Thayer",
 title = {{IMPS: An Updated System Description}},
 journal = "LNCS",
 volume = "1104",
 pages = "298302",
 year = "1996",
 paper = "Farm96.pdf"
}

\end{chunk}

\index{Gordon, M.}
\index{Milner, R.}
\index{Wadsworth, C.P.}
\begin{chunk}{axiom.bib}
@book{Gord79,
 author = "Gordon, M. and Milner, R. and Wadsworth, C.P.",
 title = {{Edinburgh LCF: A Mechanised Logic of Computation}},
 comment = "Lecture Notes in Computer Science Volume 78",
 publisher = "SpringerVerlag",
 year = "1979"
}

\end{chunk}

\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen17,
 author = "Pfenning, Frank",
 title = {{Logical Frameworks}},
 link = "\url{http://www.cs.cmu.edu/afs/cs.cmu.edu/user/fp/www/lfs.html}",
 year = "2017"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Theo17,
 author = "Unknown",
 title = {{Theorema Project}},
 link = "\url{http://www.theorema.org}",
 year = "2017"
+ "This paper describes a manmachine theoremproving system at the
+ University of Texas at Austin which has been used to prove a few
+ theorems in general topology. The theorem (or subgoal) being proved is
+ presented on the scope in its natural form so that the user can easily
+ comprehend it and, by a series of interactive commands, can help with
+ the proof when he desires. A feature called DETAIL is employed which
+ allows the human to interact only when needed and only to the extent
+ necessary for the proof.
+
+ The program is built around a modified form of IMPLY, a
+ naturaldeductionlike theorem proving technique which has been
+ described earlier.",
+ paper = "Bled74.pdf"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 7afd180..d4c92ec 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5858,6 +5858,8 @@ books/bookvolbib add references
books/bookvolbib add references
20171115.01.tpd.patch
books/bookvolbib add references
+20171127.01.tpd.patch
+books/bookvolbib add references

1.9.1