From cbc68433cc8168d66592937e9a7cc20e3e181124 Mon Sep 17 00:00:00 2001
From: Tim Daly
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.msrinria.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/axiomwebsite/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.msrinria.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 pp172175 (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/axiomwebsite/patches.html 20160324.01.tpd.patch
+20160324 tpd books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+
20160320 tpd src/axiomwebsite/patches.html 20160320.04.tpd.patch
20160320 tpd books/bookvolbib Add Brow01, the McCallum CAD projection
20160320 tpd src/axiomwebsite/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 orderinvariance",
 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 signinvariant CAD for the set of
 input polynomials. Problems may arise when a ($k+1$)level projection
 factor vanishes identically over a klevel 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 signinvariant 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 orderinvariant 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.msrinria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html",
+ abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index bff2cd6..47bc446 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5244,6 +5244,8 @@ books/bookvolbib Add Demm88 Computing Small Singular Values
books/bookvolbib Add Fern92 Accurate Singular Values
20160320.04.tpd.patch
books/bookvolbib Add Brow01, the McCallum CAD projection
+20160324.01.tpd.patch
+books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+

1.7.5.4