From db878f7b47f63fb882305b03de8b56dfc5410f35 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 11 Oct 2017 21:30:16 -0400
Subject: [PATCH] books/bookvolbib Proving Axiom Correct references
Goal: Proving Axiom Correct
\index{de Bruijn, N.G.}
\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 = "CAS-Proof"
}
\end{chunk}
\index{Jones, C.}
\begin{chunk}{axiom.bib}
@book{Jone93,
author = "Jones, C.",
title = Completing the Rationals and Metric Spaces in LEGO",
booktitle = "Logical Frameworks",
pages = "209-222",
year = "1993",
publisher = "Cambridge University Press"
}
\end{chunk}
\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"
}
\end{chunk}
\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 = "185-253",
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."
}
\end{chunk}
\index{Bundy, Alan}
\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 = "111-120",
year = "1998",
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 LCF-like tactics and by recording these
specifications in a sorted meta-logic, 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 Boyer-Moore
theorem prover.",
paper = "Bund88.pdf"
}
\end{chunk}
\index{Guttag, John V.}
\index{Horning, James J.}
\begin{chunk}{axiom.bib}
@book{Gutt93,
author = "Guttag, John V. and Horning, James J.",
title = "LARCH: Languages and TOols for Formal Specifications",
publisher = "Springer-Verlag",
year = "1993",
isbn = "3-540-94006-5"
}
\end{chunk}
\index{McCune, William W.}
\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",
number = "1",
year = "1993",
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 theorem-proving 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"
}
\end{chunk}
---
books/axiom.bib | 106 ++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet | 138 +++++++++++++++++++++++++++++++++++++++
changelog | 2 +
patch | 142 ++++++++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
5 files changed, 388 insertions(+), 2 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index d954b86..1e977b3 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -7468,6 +7468,18 @@ paper = "Brea89.pdf"
paper = "Broy88.pdf"
}
+\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 = "CAS-Proof"
+}
+
@article{Buch97,
author = "Buchberger, Bruno",
title = "Mathematica: doing mathematics by computer?",
@@ -7516,6 +7528,51 @@ paper = "Brea89.pdf"
paper = "Bulo10.pdf"
}
+@article{Bund88,
+ author = "Bundy, Alan",
+ title = "The Use of Explicit Plans to Guide Inductive Proofs",
+ journal = "LNCS 310",
+ volume = "310",
+ pages = "111-120",
+ year = "1998",
+ 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 LCF-like tactics and by recording these
+ specifications in a sorted meta-logic, 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 Boyer-Moore
+ theorem prover.",
+ paper = "Bund88.pdf"
+}
+
+@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 = "185-253",
+ 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."
+}
+
@misc{Byrd17,
author = "Byrd, William",
title = "The Most Beautiful Program Ever Written",
@@ -8312,6 +8369,14 @@ paper = "Brea89.pdf"
isbn = "0-387-90641-X"
}
+@book{Gutt93,
+ author = "Guttag, John V. and Horning, James J.",
+ title = "LARCH: Languages and TOols for Formal Specifications",
+ publisher = "Springer-Verlag",
+ year = "1993",
+ isbn = "3-540-94006-5"
+}
+
@misc{Hard13,
author = "Hardin, David S. and McClurg, Jedidiah R. and Davis, Jennifer A.",
title = "Creating Formally Verified Components for Layered Assurance
@@ -8570,6 +8635,25 @@ paper = "Brea89.pdf"
keyword = "axiomref, CAS-Proof"
}
+@book{Jone93,
+ author = "Jones, C.",
+ title = "Completing the Rationals and Metric Spaces in LEGO",
+ booktitle = "Logical Frameworks",
+ pages = "209-222",
+ year = "1993",
+ publisher = "Cambridge University Press"
+}
+
+@misc{JARx96,
+ author = "various",
+ title = "Journal of Automated Reasoning",
+ publisher = "Springer",
+ year = "1996",
+ volume = "16",
+ number = "1/2",
+ comment = "Special Issue on Inductive Proof"
+}
+
@misc{Juds16,
author = "Judson, Thomas W.",
title = "Abstract Algebra: Theory and Applications",
@@ -9055,6 +9139,28 @@ paper = "Brea89.pdf"
paper = "Mcca78.pdf"
}
+@article{Mccu93,
+ author = "McCune, William W.",
+ title = "Single Axioms for Groups and Abelian Groups with Various
+ Operations",
+ journal = "J. Automated Reasoning",
+ volume = "10",
+ number = "1",
+ year = "1993",
+ 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 theorem-proving 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"
+}
+
@article{Medi04,
author = "Medina-Bulo, Inmaculada and Lozano-Palomo, F. and
Alonso-Jimenez, J.A. and Ruiz-Reina, J.L.",
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 9d17e40..8eef500 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -10242,6 +10242,22 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\end{chunk}
+\index{de Bruijn, N.G.}
+\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 = "CAS-Proof"
+}
+
+\end{chunk}
+
\index{Buchberger, Bruno}
\begin{chunk}{axiom.bib}
@article{Buch97,
@@ -10308,6 +10324,63 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp1215-1231
\end{chunk}
+\index{Bundy, Alan}
+\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 = "111-120",
+ year = "1998",
+ 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 LCF-like tactics and by recording these
+ specifications in a sorted meta-logic, 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 Boyer-Moore
+ theorem prover.",
+ paper = "Bund88.pdf"
+}
+
+\end{chunk}
+
+\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 = "185-253",
+ 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."
+}
+
+\end{chunk}
+
\index{Byrd, William}
\begin{chunk}{axiom.bib}
@misc{Byrd17,
@@ -11416,6 +11489,19 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Guttag, John V.}
+\index{Horning, James J.}
+\begin{chunk}{axiom.bib}
+@book{Gutt93,
+ author = "Guttag, John V. and Horning, James J.",
+ title = "LARCH: Languages and TOols for Formal Specifications",
+ publisher = "Springer-Verlag",
+ year = "1993",
+ isbn = "3-540-94006-5"
+}
+
+\end{chunk}
+
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Hardin, David S.}
@@ -11736,6 +11822,32 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Jones, C.}
+\begin{chunk}{axiom.bib}
+@book{Jone93,
+ author = "Jones, C.",
+ title = "Completing the Rationals and Metric Spaces in LEGO",
+ booktitle = "Logical Frameworks",
+ pages = "209-222",
+ year = "1993",
+ publisher = "Cambridge University Press"
+}
+
+\end{chunk}
+
+\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"
+}
+
+\end{chunk}
+
\index{Judson, Thomas W.}
\begin{chunk}{axiom.bib}
@misc{Juds16,
@@ -12354,6 +12466,32 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{McCune, William W.}
+\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",
+ number = "1",
+ year = "1993",
+ 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 theorem-proving 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"
+}
+
+\end{chunk}
+
\index{Medina-Bulo, Inmaculada}
\index{Lozano-Palomo, F.}
\index{Alonso-Jimenez, J.A.}
diff --git a/changelog b/changelog
index 5571b9a..a63b5a7 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20171011 tpd src/axiom-website/patches.html 20171011.01.tpd.patch
+20171011 tpd books/bookvolbib Proving Axiom Correct references
20171010 tpd src/axiom-website/patches.html 20171010.01.tpd.patch
20171010 tpd books/*.pamphlet eliminate redundant index in toc
20171009 tpd src/axiom-website/patches.html 20171009.04.tpd.patch
diff --git a/patch b/patch
index 327645c..d2a7035 100644
--- a/patch
+++ b/patch
@@ -1,4 +1,142 @@
-books/*.pamphlet eliminate redundant index in toc
+books/bookvolbib Proving Axiom Correct references
-Goal: Axiom Maintenance
+Goal: Proving Axiom Correct
+\index{de Bruijn, N.G.}
+\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 = "CAS-Proof"
+}
+
+\end{chunk}
+
+\index{Jones, C.}
+\begin{chunk}{axiom.bib}
+@book{Jone93,
+ author = "Jones, C.",
+ title = Completing the Rationals and Metric Spaces in LEGO",
+ booktitle = "Logical Frameworks",
+ pages = "209-222",
+ year = "1993",
+ publisher = "Cambridge University Press"
+}
+
+\end{chunk}
+
+\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"
+}
+
+\end{chunk}
+
+\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 = "185-253",
+ 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."
+}
+
+\end{chunk}
+
+\index{Bundy, Alan}
+\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 = "111-120",
+ year = "1998",
+ 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 LCF-like tactics and by recording these
+ specifications in a sorted meta-logic, 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 Boyer-Moore
+ theorem prover.",
+ paper = "Bund88.pdf"
+}
+
+\end{chunk}
+
+\index{Guttag, John V.}
+\index{Horning, James J.}
+\begin{chunk}{axiom.bib}
+@book{Gutt93,
+ author = "Guttag, John V. and Horning, James J.",
+ title = "LARCH: Languages and TOols for Formal Specifications",
+ publisher = "Springer-Verlag",
+ year = "1993",
+ isbn = "3-540-94006-5"
+}
+
+\end{chunk}
+
+\index{McCune, William W.}
+\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",
+ number = "1",
+ year = "1993",
+ 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 theorem-proving 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"
+}
+
+\end{chunk}
+
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 564da63..51c9f2d 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5836,6 +5836,8 @@ books/bookvol5 update credits list

books/Makefile temp fix for signature sorting

20171010.01.tpd.patch
books/*.pamphlet eliminate redundant index in toc

+20171011.01.tpd.patch
+books/bookvolbib Proving Axiom Correct references

--
1.9.1