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.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
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