From cbc68433cc8168d66592937e9a7cc20e3e181124 Mon Sep 17 00:00:00 2001
From: Tim Daly <daly@axiom-developer.org>
Date: Thu, 24 Mar 2016 09:20:49 -0400
Subject: [PATCH] books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+

Goal: Axiom Algebra

@misc{TLA16,
  author = "Lamport, Leslie",
  title = "TLA+ Proof System",
  year = "2016",
  url = "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html",
  abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
}
---
 books/bookvolbib.pamphlet      |   13 ++++++++++-
 changelog                      |    2 +
 patch                          |   46 ++++++---------------------------------
 src/axiom-website/patches.html |    2 +
 4 files changed, 23 insertions(+), 40 deletions(-)

diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 22fa31f..2450594 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2853,6 +2853,18 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
 
 \end{chunk}
 
+\index{Lamport, Leslie}
+\begin{chunk}{axiom.bib}
+@misc{TLA16,
+  author = "Lamport, Leslie",
+  title = "TLA+ Proof System",
+  year = "2016",
+  url = "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html",
+  abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
+}
+
+\end{chunk}
+
 \index{Mahboubi, Assia}
 \begin{chunk}{axiom.bib}
 @article{Mahb06,
@@ -6819,7 +6831,6 @@ Proc ISSAC 97 pp172-175 (1997)
     method nor our improvement of it have been implemented in QEPCAD. The
     design of the system would make implementing such a feature quite
     difficult."
-
 }
 
 \end{chunk}
diff --git a/changelog b/changelog
index 8ddfd0d..3059404 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20160324 tpd src/axiom-website/patches.html 20160324.01.tpd.patch
+20160324 tpd books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+
 20160320 tpd src/axiom-website/patches.html 20160320.04.tpd.patch
 20160320 tpd books/bookvolbib Add Brow01, the McCallum CAD projection
 20160320 tpd src/axiom-website/patches.html 20160320.03.tpd.patch
diff --git a/patch b/patch
index 0e4da59..1e14b2b 100644
--- a/patch
+++ b/patch
@@ -1,43 +1,11 @@
-books/bookvolbib Add Brow01, the McCallum CAD projection
+books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+
 
 Goal: Axiom Algebra
 
-@article{Brow01,
-  author="Brown, Christopher W.",
-  title="The McCallum projection, lifting, and order-invariance",
-  year="2001",
-  url="http://www.usna.edu/Users/cs/wcbrown/research/MOTS2001.1.ps.gz",
-  paper = "Brow01.pdf",
-  abstract = 
-    "The McCallum Projection for Cylindrical Algebraic Decomposition (CAD)
-    produces a smaller projection factor set than previous projections,
-    however it does not always produce a sign-invariant CAD for the set of
-    input polynomials. Problems may arise when a ($k+1$)-level projection
-    factor vanishes identically over a k-level cell. According to
-    McCallum's paper, when this happens (and $k+1$ is not the highest
-    level in the CAD) we do not know whether the projection is valid,
-    i.e. whether or not a sign-invariant CAD for the set of input
-    polynomials will be produced when lifting is performed in the usual
-    way. When the $k$-level cell in question has dimension 0, McCallum
-    suggests a modification of the lifting method that will ensure the
-    validity of his projection, although to my knowledge this has never
-    been implemented.
-
-    In this paper we give easily computable criteria that often allow us
-    to conclude that McCallum's projection is valid even though a
-    projection factor vanishes identically over a cell. We also improve on
-    McCallum's modified lifting method.
-
-    We've incorporated the ideas contained in the paper into QEPCAD, the
-    most complete implementation of CAD. When McCallum's projection is
-    invalid because of a projection factor not being order-invariant over a
-    region on which it vanishes identically, at least a warning message
-    ought to be issued. Currently, QEPCAD may print warning messages that
-    are not needed, and may fail to print warning messages when they are
-    needed. Our implementation in QEPCAD ensures that warning messages are
-    printed when needed, and reduces the number of times warning messages
-    are printed when not needed. Neither McCallum's modified lifting
-    method nor our improvement of it have been implemented in QEPCAD. The
-    design of the system would make implementing such a feature quite
-    difficult."
+@misc{TLA16,
+  author = "Lamport, Leslie",
+  title = "TLA+ Proof System",
+  year = "2016",
+  url = "https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html",
+  abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
 }
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index bff2cd6..47bc446 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5244,6 +5244,8 @@ books/bookvolbib Add Demm88 Computing Small Singular Values<br/>
 books/bookvolbib Add Fern92 Accurate Singular Values<br/>
 <a href="patches/20160320.04.tpd.patch">20160320.04.tpd.patch</a>
 books/bookvolbib Add Brow01, the McCallum CAD projection<br/>
+<a href="patches/20160324.01.tpd.patch">20160324.01.tpd.patch</a>
+books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+<br/>
  </body>
 </html>
 
-- 
1.7.5.4

