From 0c2e59c6fd5f8d7e8d299c527e019416a4ea4492 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 17 Oct 2017 07:39:29 0400
Subject: [PATCH] books/bookvol13 add Homann database reference
Goal: Proving Axiom Correct

books/bookvol13.pamphlet  13 +
changelog  2 +
patch  528 +
src/axiomwebsite/patches.html  2 +
4 files changed, 18 insertions(+), 527 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index ef8dd4a..8f83678 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 2971,6 +2971,19 @@ Aczel\cite{Acze13} Homotopy Type Theory
Santas\cite{Sant95} A Type System for Computer Algebra
+Homann\cite{Homa94} algorithm schemata
+
+Name: gcd(?a,?b)=?g\\
+Signature: ?A $\times$ ?A $\rightarrow$ ?A\\
+Constraints: (?A, EuclideanRing)\\
+Definition: $(?g \vert ?a)\land(?g \vert ?b) \land
+(\forall c \in ?A: (c \vert ?a) \land
+(c \vert ?b)\Rightarrow (c\vert ?g))$\\
+Theorems:\\
+gcd(u,v) = gcd(v,u)\\
+gcd(u,v) = gcd(v, u mod v)\\
+gcd(u,0) = u
+
\appendix
\chapter{The Global Environment}
diff git a/changelog b/changelog
index 576da38..8cefb26 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171017 tpd src/axiomwebsite/patches.html 20171017.01.tpd.patch
+20171017 tpd books/bookvol13 add Homann database reference
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
diff git a/patch b/patch
index 2126375..7e43a8b 100644
 a/patch
+++ b/patch
@@ 1,530 +1,4 @@
books/bookvolbib Proving Axiom Correct references
+books/bookvol13 add Homann database reference
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}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 315f5af..c948616 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5840,6 +5840,8 @@ books/*.pamphlet eliminate redundant index in toc
books/bookvolbib Proving Axiom Correct references
20171016.01.tpd.patch
books/bookvolbib Proving Axiom Correct references
+20171017.01.tpd.patch
+books/bookvol13 add Homann database reference

1.9.1