From 19f4a72dbb929be8366c48f249dba0ca7111fcfc Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 9 May 2017 02:17:23 0400
Subject: [PATCH] bookvolbib: Cylindrical Algebraic Decomposition references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Brown, Christopher W.}
\begin{chunk}{axiom.bib}
@article{Brow12,
author = "Brown, Christopher W.",
title = "Fast simplifications for Tarski formulas based on monomial
inequalities",
year = "2012",
journal = "Journal of Symbolic Computation",
volume = "47",
pages = "859882",
abstract =
"We define the ‘‘combinatorial part’’ of a Tarski formula in which
equalities and inequalities are in factored or partially factored
form. The combinatorial part of a formula contains only
‘‘monomial inequalities’’,which are sign conditions on monomials. We
give efficient algorithms for answering some basic questions about
conjunctions of monomial inequalities and prove the
NPCompleteness/Hardness of some others. By simplifying the
combinatorial part of a Tarski formula, and mapping the simplified
combinatorial part back to a Tarski formula, we obtain nontrivial
simplifications without algebraic operations.",
paper = "Brow12.pdf"
}
\end{chunk}
\index{Arno, D.S.}
\index{Mignotte, M.}
\begin{chunk}{axiom.bib}
@article{Arno88,
author = "Arno, D.S. and Mignotte, M.",
title = "On Mechanical Quantifier Elimination for Elementary Algebra
and Geometry",
journal = "J. Symbolic Computation",
volume = "5",
pages = "237259",
year = "1988",
link = "\url{http://http://www.sciencedirect.com/science/article/pii/S0747717188800142/pdf?md5=62052077d84e6078cc024bc8e29c23c1&pid=1s2.0S0747717188800142main.pdf}",
abstract = "
We give solutions to two problems of elementary algebra and geometry:
(1) find conditions on real numbers $p$, $q$, and $r$ so that the
polynomial function $f(x)=x^4+px^2+qx+r$ is nonnegative for all real
$x$ and (2) find conditions on real numbers $a$, $b$, and $c$ so that
the ellipse $\frac{(xe)^2}{q^2}+\frac{y^2}{b^2}1=0$ lies inside the
unit circle $y^2+x^21=0$. Our solutions are obtained by following the
basic outline of the method of quantifier elimination by cylindrical
algebraic decomposition (Collins, 1975), but we have developed, and
have been considerably aided by, modified versions of certain of its
steps. We have found three equally simple but not obviously equivalent
solutions for the first problem, illustrating the difficulty of
obtaining unique ``simplest'' solutions to quantifier elimination
problems of elementary algebra and geometry.",
paper = "Arno88.pdf"
}
\end{chunk}
\index{Collins, George E.}
\begin{chunk}{axiom.bib}
@article{Coll75,
author = "Collins, George E.",
title = "Quantifier Elimination for Real Closed Fields by
Cylindrical Algebraic Decomposition",
year = "1975",
journal = "Lecture Notes in Computer Science",
volume = "33",
pages = "134183",
abstract =
"I. Introduction. Tarski in 1948, published a quantifier
elimination method for the elementary theory of real closed fields
(which he had discoverd in 1930). As noted by Tarski, any quantifier
elimination method for this theory also provides a decision method,
which enables one to decide whether any sentence of the theory is
true or false. Since many important and difficult mathematical
problems can be expressed in this theory, any computationally
feasible quantifier elimination algorithm would be of utmost
significance.
However, it became apparent that Tarski's method required too much
computation to be practical except for quite trivial problems.
Seidenberg in 1954, described another method which he thought
would be more efficient. A third method was published by Cohen in
1969. Some significant improvements of Tarski's method have been
made by W. Boge, which are described in a thesis by Holthusen
This paper describes a completely new method which I discoverd in
February 1973. This method was presented in a seminar at Stanford
University in March 1973 and in abstract form at a symposium at
CarnegieMellon University in May 1973. In August 1974 a full
presentation of the method was delivered at the EUROSAM 74 Conference
in Stockholm, and a preliminary version of the present paper was
published in the proceedings of that conference.",
paper = "Coll75.pdf"
}
\end{chunk}
\index{Arnon, Dennis S.}
\index{Collins, George E.}
\index{McCallum, Scott}
\begin{chunk}{axiom.bib}
@techreport{Arno82,
author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
title = "Cylindrical Algebraic Decomposition I: The Basic Algorithm",
year = "1982",
institution = "Purdue University",
type = "Technical Report",
number = "82427A",
link = "\url{https://pdfs.semanticscholar.org/7643/4b54250f05ebf0dcc27c33b7dc250419fb94.pdf}",
abstract =
"Given a set of rvariate integral polynomials, a {\sl cylindrical
algebraic decomposition (cad)} of euclidean rspace $E^r$ into connected
subsets compatible with the zeros of the polynomials. Collins gave a
cad construction algorithm in 1975, as part of a quantifier elimination
procedure for real closed fields. The algorithm has subsequently found
diverse applications (optimization, curve display); new applications
have been proposed (term rewriting systems, motion planning). In the
present twopart paper, we give an algorithm for determining the pairs
of adjacent cells in a cad of $E^2$. This capability is often needed
in applications. In Part I we describe the essential features of the
rspace cad algorithm, to provide a framework for the adjacency algorithm
in Part II.",
paper = "Arno82.pdf"
}
\end{chunk}
\index{Arnon, Dennis S.}
\index{Collins, George E.}
\index{McCallum, Scott}
\begin{chunk}{axiom.bib}
@article{Arno84,
author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
title = "Cylindrical Algebraic Decomposition II: An Adjacency Algorithm
for the Plane",
year = "1984",
journal = "SIAM J. Comput.",
volume = "13",
number = "4",
pages = "878889",
abstract =
"Given a set of rvariate integral polynomials, a {\sl cylindrical
algebraic decomposition (cad)} of euclidean rspace $E^r$ partitions
$E^r$ into connected subsets compaitible with the zeros of the
polynomials. Each subset is a {\sl cell}. Informally, two cells of
a cad are {\sl adjacent} if they touch each other; formally, they are
adjacent if their union is connected. In applications of cad's one
often wishes to know the adjacent pairs of cells. Previous algorithms
for cad construction (such as that given in Part I of this paper) have
not actually determined them. We give here in Part II an algorithm
which determines the pairs of adjacent cells as it constructs a cad
of $E^2$.",
paper = "Arno84.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  143 ++++++++++++++++++++++++++++
changelog  4 +
patch  196 +++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 287 insertions(+), 58 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index b236d45..b9ab4c2 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 6159,6 +6159,32 @@ Martin, U.
\end{chunk}
+\index{Brown, Christopher W.}
+\begin{chunk}{axiom.bib}
+@article{Brow12,
+ author = "Brown, Christopher W.",
+ title = "Fast simplifications for Tarski formulas based on monomial
+ inequalities",
+ year = "2012",
+ journal = "Journal of Symbolic Computation",
+ volume = "47",
+ pages = "859882",
+ abstract =
+ "We define the ‘‘combinatorial part’’ of a Tarski formula in which
+ equalities and inequalities are in factored or partially factored
+ form. The combinatorial part of a formula contains only
+ ‘‘monomial inequalities’’,which are sign conditions on monomials. We
+ give efficient algorithms for answering some basic questions about
+ conjunctions of monomial inequalities and prove the
+ NPCompleteness/Hardness of some others. By simplifying the
+ combinatorial part of a Tarski formula, and mapping the simplified
+ combinatorial part back to a Tarski formula, we obtain nontrivial
+ simplifications without algebraic operations.",
+ paper = "Brow12.pdf"
+}
+
+\end{chunk}
+
\index{Buchberger, Bruno}
\begin{chunk}{axiom.bib}
@article{Buch97,
@@ 13928,12 +13954,77 @@ Proc ISSAC 97 pp172175 (1997)
\section{Cylindrical Algebraic Decomposition} %%%%%%%%%%%%%%%%%%%%%%
\index{Arno, D.S.}
+\index{Arnon, Dennis S.}
+\index{Collins, George E.}
+\index{McCallum, Scott}
+\begin{chunk}{axiom.bib}
+@techreport{Arno82,
+ author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
+ title = "Cylindrical Algebraic Decomposition I: The Basic Algorithm",
+ year = "1982",
+ institution = "Purdue University",
+ type = "Technical Report",
+ number = "82427A",
+ link = "\url{https://pdfs.semanticscholar.org/7643/4b54250f05ebf0dcc27c33b7dc250419fb94.pdf}",
+ abstract =
+ "Given a set of rvariate integral polynomials, a {\sl cylindrical
+ algebraic decomposition (cad)} of euclidean rspace $E^r$ into connected
+ subsets compatible with the zeros of the polynomials. Collins gave a
+ cad construction algorithm in 1975, as part of a quantifier elimination
+ procedure for real closed fields. The algorithm has subsequently found
+ diverse applications (optimization, curve display); new applications
+ have been proposed (term rewriting systems, motion planning). In the
+ present twopart paper, we give an algorithm for determining the pairs
+ of adjacent cells in a cad of $E^2$. This capability is often needed
+ in applications. In Part I we describe the essential features of the
+ rspace cad algorithm, to provide a framework for the adjacency algorithm
+ in Part II.",
+ paper = "Arno82.pdf"
+}
+
+\end{chunk}
+
+\index{Arnon, Dennis S.}
+\index{Collins, George E.}
+\index{McCallum, Scott}
+\begin{chunk}{axiom.bib}
+@article{Arno84,
+ author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
+ title = "Cylindrical Algebraic Decomposition II: An Adjacency Algorithm
+ for the Plane",
+ year = "1984",
+ journal = "SIAM J. Comput.",
+ volume = "13",
+ number = "4",
+ pages = "878889",
+ abstract =
+ "Given a set of rvariate integral polynomials, a {\sl cylindrical
+ algebraic decomposition (cad)} of euclidean rspace $E^r$ partitions
+ $E^r$ into connected subsets compaitible with the zeros of the
+ polynomials. Each subset is a {\sl cell}. Informally, two cells of
+ a cad are {\sl adjacent} if they touch each other; formally, they are
+ adjacent if their union is connected. In applications of cad's one
+ often wishes to know the adjacent pairs of cells. Previous algorithms
+ for cad construction (such as that given in Part I of this paper) have
+ not actually determined them. We give here in Part II an algorithm
+ which determines the pairs of adjacent cells as it constructs a cad
+ of $E^2$.",
+ paper = "Arno84.pdf"
+}
+
+\end{chunk}
+
+\index{Arnon, D.S.}
\index{Mignotte, M.}
\begin{chunk}{ignore}
\bibitem[Arnon 88]{Arno88} Arno, D.S.; Mignotte, M.
 title = "On Mechanical Quantifier Elimination for Elementary Algebra and Geometry",
J. Symbolic Computation 5, 237259 (1988)
+\begin{chunk}{axiom.bib}
+@article{Arno88,
+ author = "Arnon, D.S. and Mignotte, M.",
+ title = "On Mechanical Quantifier Elimination for Elementary Algebra
+ and Geometry",
+ journal = "J. Symbolic Computation",
+ volume = "5",
+ pages = "237259",
+ year = "1988",
link = "\url{http://http://www.sciencedirect.com/science/article/pii/S0747717188800142/pdf?md5=62052077d84e6078cc024bc8e29c23c1&pid=1s2.0S0747717188800142main.pdf}",
abstract = "
We give solutions to two problems of elementary algebra and geometry:
@@ 13951,6 +14042,8 @@ J. Symbolic Computation 5, 237259 (1988)
problems of elementary algebra and geometry.",
paper = "Arno88.pdf"
+}
+
\end{chunk}
\index{Beaumont, James}
@@ 14225,6 +14318,46 @@ J. Symbolic Computation 5, 237259 (1988)
\end{chunk}
+\index{Collins, George E.}
+\begin{chunk}{axiom.bib}
+@article{Coll75,
+ author = "Collins, George E.",
+ title = "Quantifier Elimination for Real Closed Fields by
+ Cylindrical Algebraic Decomposition",
+ year = "1975",
+ journal = "Lecture Notes in Computer Science",
+ volume = "33",
+ pages = "134183",
+ abstract =
+ "I. Introduction. Tarski in 1948, published a quantifier
+ elimination method for the elementary theory of real closed fields
+ (which he had discoverd in 1930). As noted by Tarski, any quantifier
+ elimination method for this theory also provides a decision method,
+ which enables one to decide whether any sentence of the theory is
+ true or false. Since many important and difficult mathematical
+ problems can be expressed in this theory, any computationally
+ feasible quantifier elimination algorithm would be of utmost
+ significance.
+
+ However, it became apparent that Tarski's method required too much
+ computation to be practical except for quite trivial problems.
+ Seidenberg in 1954, described another method which he thought
+ would be more efficient. A third method was published by Cohen in
+ 1969. Some significant improvements of Tarski's method have been
+ made by W. Boge, which are described in a thesis by Holthusen
+
+ This paper describes a completely new method which I discoverd in
+ February 1973. This method was presented in a seminar at Stanford
+ University in March 1973 and in abstract form at a symposium at
+ CarnegieMellon University in May 1973. In August 1974 a full
+ presentation of the method was delivered at the EUROSAM 74 Conference
+ in Stockholm, and a preliminary version of the present paper was
+ published in the proceedings of that conference.",
+ paper = "Coll75.pdf"
+}
+
+\end{chunk}
+
\index{RealClosure}
\index{Emiris, Ioannis Z.}
\index{Tsigaridas, Elias P.}
diff git a/changelog b/changelog
index 4566442..6d7e29c 100644
 a/changelog
+++ b/changelog
@@ 1,4 +1,6 @@
20170507 bmt src/axiomwebsite/patches.html 20170507.01.tpd.patch
+20170509 tpd src/axiomwebsite/patches.html 20170509.01.tpd.patch
+20170509 tpd bookvolbib Cylindrical Algebraic Decomposition references
+20170507 tpd src/axiomwebsite/patches.html 20170507.01.tpd.patch
20170507 tpd bookvolbib Add references to Axiom in literature
20170417 bmt src/axiomwebsite/patches.html 20170417.04.bmt.patch
20170417 bmt Makefile Build patches for BSD distribution on MAC OSX
diff git a/patch b/patch
index b8dfd96..0834543 100644
 a/patch
+++ b/patch
@@ 1,72 +1,164 @@
bookvolbib: Add references to Axiom in literature
+bookvolbib: Cylindrical Algebraic Decomposition references
Goal: Proving Axiom Correct
\index{Carette, Jacques}
\index{Farmer, William M.}
\index{Jeremic, Filip}
\index{Maccio, Vincent}
\index{O'Connor, Russell}
\index{Tran, Quang M.}
+\index{Brown, Christopher W.}
\begin{chunk}{axiom.bib}
@misc{Care11a,
 author = "Carette, Jacques and Farmer, William M. and Jeremic, Filip and
 Maccio, Vincent and O'Connor, Russell and Tran, Quang M.",
 title = "The MathScheme Library: Some Preliminary Experiments",
 year = "2011",
 link = "\url{https://arxiv.org/pdf/1106.1862.pdf}",
+@article{Brow12,
+ author = "Brown, Christopher W.",
+ title = "Fast simplifications for Tarski formulas based on monomial
+ inequalities",
+ year = "2012",
+ journal = "Journal of Symbolic Computation",
+ volume = "47",
+ pages = "859882",
abstract =
 "We present some of the experiments we have performed to best test our
 design for a library for MathScheme, the mechanized mathematics
 software system we are building. We wish for our library design to use
 and reflect, as much as possible, the mathematical structure present
 in the objects which populate the library.",
 paper = "Care11a.pdf",
 keywords = "axiomref"
+ "We define the ‘‘combinatorial part’’ of a Tarski formula in which
+ equalities and inequalities are in factored or partially factored
+ form. The combinatorial part of a formula contains only
+ ‘‘monomial inequalities’’,which are sign conditions on monomials. We
+ give efficient algorithms for answering some basic questions about
+ conjunctions of monomial inequalities and prove the
+ NPCompleteness/Hardness of some others. By simplifying the
+ combinatorial part of a Tarski formula, and mapping the simplified
+ combinatorial part back to a Tarski formula, we obtain nontrivial
+ simplifications without algebraic operations.",
+ paper = "Brow12.pdf"
}
\end{chunk}
\index{Maza, Marc Moreno}
+\index{Arno, D.S.}
+\index{Mignotte, M.}
\begin{chunk}{axiom.bib}
@misc{Maza06,
 author = "Maza, Marc Moreno",
 title = "Axiom: Generic, open and powerful",
 link = "\url{http://www.csd.uwo.ca/~moreno//Publications/ICMS061.pdf}",
 year = "2006",
 paper = "Maza06.pdf",
 keywords = "axiomref"
+@article{Arno88,
+ author = "Arno, D.S. and Mignotte, M.",
+ title = "On Mechanical Quantifier Elimination for Elementary Algebra
+ and Geometry",
+ journal = "J. Symbolic Computation",
+ volume = "5",
+ pages = "237259",
+ year = "1988",
+ link = "\url{http://http://www.sciencedirect.com/science/article/pii/S0747717188800142/pdf?md5=62052077d84e6078cc024bc8e29c23c1&pid=1s2.0S0747717188800142main.pdf}",
+ abstract = "
+ We give solutions to two problems of elementary algebra and geometry:
+ (1) find conditions on real numbers $p$, $q$, and $r$ so that the
+ polynomial function $f(x)=x^4+px^2+qx+r$ is nonnegative for all real
+ $x$ and (2) find conditions on real numbers $a$, $b$, and $c$ so that
+ the ellipse $\frac{(xe)^2}{q^2}+\frac{y^2}{b^2}1=0$ lies inside the
+ unit circle $y^2+x^21=0$. Our solutions are obtained by following the
+ basic outline of the method of quantifier elimination by cylindrical
+ algebraic decomposition (Collins, 1975), but we have developed, and
+ have been considerably aided by, modified versions of certain of its
+ steps. We have found three equally simple but not obviously equivalent
+ solutions for the first problem, illustrating the difficulty of
+ obtaining unique ``simplest'' solutions to quantifier elimination
+ problems of elementary algebra and geometry.",
+ paper = "Arno88.pdf"
+
}
\end{chunk}
\index{Zippel, Richard}
+\index{Collins, George E.}
\begin{chunk}{axiom.bib}
@book{Zipp92,
 author = "Zippel, Richard",
 title = "Symbolic/Numeric Techniques in Modeling and Simulation",
 link = "\url{http://www.cs.duke.edu/donaldlab/Books/SymbolicNumericalComputation/323346.pdf}",
 year = "1992",
 publisher = "Academic Press Limited",
 isbn = "0122205359",
+@article{Coll75,
+ author = "Collins, George E.",
+ title = "Quantifier Elimination for Real Closed Fields by
+ Cylindrical Algebraic Decomposition",
+ year = "1975",
+ journal = "Lecture Notes in Computer Science",
+ volume = "33",
+ pages = "134183",
abstract =
 "Modeling and simulating collections of physical objects that are
 subject to a wide variety of physical forces and interactions is
 exceedingly difficult. The construction of a single simulator capable
 of dealing with all possible physical processes is completely
 impracti cal and, it seems to us, wrongheaded. Instead, we propose
 to build custom simulators designed for a particular collection of
 physical objects, where a particular set of physical phenomena are
 involved. For such an approach to be practical, an environment must
 be provided that facilitates the quick construction of these
 simulators. In this paper we describe the essential features of such
 an environment and describe in some detail how a general
 implementation of the weighted residual method, one of the more
 general classes of numerical integration techniques, can be used.",
 paper = "Zipp92.pdf",
 keywords = "axiomref"
+ "I. Introduction. Tarski in 1948, published a quantifier
+ elimination method for the elementary theory of real closed fields
+ (which he had discoverd in 1930). As noted by Tarski, any quantifier
+ elimination method for this theory also provides a decision method,
+ which enables one to decide whether any sentence of the theory is
+ true or false. Since many important and difficult mathematical
+ problems can be expressed in this theory, any computationally
+ feasible quantifier elimination algorithm would be of utmost
+ significance.
+
+ However, it became apparent that Tarski's method required too much
+ computation to be practical except for quite trivial problems.
+ Seidenberg in 1954, described another method which he thought
+ would be more efficient. A third method was published by Cohen in
+ 1969. Some significant improvements of Tarski's method have been
+ made by W. Boge, which are described in a thesis by Holthusen
+
+ This paper describes a completely new method which I discoverd in
+ February 1973. This method was presented in a seminar at Stanford
+ University in March 1973 and in abstract form at a symposium at
+ CarnegieMellon University in May 1973. In August 1974 a full
+ presentation of the method was delivered at the EUROSAM 74 Conference
+ in Stockholm, and a preliminary version of the present paper was
+ published in the proceedings of that conference.",
+ paper = "Coll75.pdf"
}

+
+\end{chunk}
+
+\index{Arnon, Dennis S.}
+\index{Collins, George E.}
+\index{McCallum, Scott}
+\begin{chunk}{axiom.bib}
+@techreport{Arno82,
+ author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
+ title = "Cylindrical Algebraic Decomposition I: The Basic Algorithm",
+ year = "1982",
+ institution = "Purdue University",
+ type = "Technical Report",
+ number = "82427A",
+ link = "\url{https://pdfs.semanticscholar.org/7643/4b54250f05ebf0dcc27c33b7dc250419fb94.pdf}",
+ abstract =
+ "Given a set of rvariate integral polynomials, a {\sl cylindrical
+ algebraic decomposition (cad)} of euclidean rspace $E^r$ into connected
+ subsets compatible with the zeros of the polynomials. Collins gave a
+ cad construction algorithm in 1975, as part of a quantifier elimination
+ procedure for real closed fields. The algorithm has subsequently found
+ diverse applications (optimization, curve display); new applications
+ have been proposed (term rewriting systems, motion planning). In the
+ present twopart paper, we give an algorithm for determining the pairs
+ of adjacent cells in a cad of $E^2$. This capability is often needed
+ in applications. In Part I we describe the essential features of the
+ rspace cad algorithm, to provide a framework for the adjacency algorithm
+ in Part II.",
+ paper = "Arno82.pdf"
+}
+
\end{chunk}
+\index{Arnon, Dennis S.}
+\index{Collins, George E.}
+\index{McCallum, Scott}
+\begin{chunk}{axiom.bib}
+@article{Arno84,
+ author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
+ title = "Cylindrical Algebraic Decomposition II: An Adjacency Algorithm
+ for the Plane",
+ year = "1984",
+ journal = "SIAM J. Comput.",
+ volume = "13",
+ number = "4",
+ pages = "878889",
+ abstract =
+ "Given a set of rvariate integral polynomials, a {\sl cylindrical
+ algebraic decomposition (cad)} of euclidean rspace $E^r$ partitions
+ $E^r$ into connected subsets compaitible with the zeros of the
+ polynomials. Each subset is a {\sl cell}. Informally, two cells of
+ a cad are {\sl adjacent} if they touch each other; formally, they are
+ adjacent if their union is connected. In applications of cad's one
+ often wishes to know the adjacent pairs of cells. Previous algorithms
+ for cad construction (such as that given in Part I of this paper) have
+ not actually determined them. We give here in Part II an algorithm
+ which determines the pairs of adjacent cells as it constructs a cad
+ of $E^2$.",
+ paper = "Arno84.pdf"
+}
+
+\end{chunk}
+
+
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index b4db614..cabdafd 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5712,6 +5712,8 @@ src/axiomwebsite/download.html fix typo in BSD binary filename
Makefile Build patches for BSD distribution on MAC OSX
20170507.01.tpd.patch
bookvolbib Add references to Axiom in literature
+20170509.01.tpd.patch
+bookvolbib Cylindrical Algebraic Decomposition references

1.7.5.4