%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "basupr96.ltx",
%%%     date      = "17 December 1996",
%%%     time      = "16:44:13 EST",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "50789 108 447 3696",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 by ACM, Inc.
%%%                  Permission to make digital or hard copies of part
%%%                  or all of this work for personal or classroom use
%%%                  is granted without fee provided that copies are
%%%                  not made or distributed for profit or direct
%%%                  commercial advantage and that copies bear this
%%%                  notice and the full citation on the first page.
%%%                  Copyrights for components of this work owned by
%%%                  others than ACM must be honored. Abstracting with
%%%                  credit is permitted. To copy otherwise, to
%%%                  republish, to post on servers, or to redistribute
%%%                  to lists, requires prior specific permission
%%%                  and/or a fee. Request permissions from
%%%                  Publications Dept, ACM Inc., fax +1 (212)
%%%                  869-0481, or permissions@acm.org.
%%%
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{BasuPR96}

\title{On the Combinatorial and Algebraic Complexity of Quantifier
Elimination}

\author{Saugata Basu \and Richard Pollack \and Marie-Fran{\c{c}}oise
Roy}

\Pages{1002--1045}

\Month{November}

\Year{1996}

\Volume{43}

\Number{6}

\maketitle

\begin{abstract}

In this paper, a new algorithm for performing quantifier elimination
from first order formulas over real closed fields is given. This
algorithm improves the complexity of the asymptotically fastest
algorithm for this problem, known to this date. A new feature of this
algorithm is that the rule of the algebraic part (the dependence on
the degrees of the input polynomials) and the combinatorial part (the
dependence on the number of the polynomials) are separated. Another
new feature is that the degrees of the polynomials in the equivalent
quantifier-free formula that is output, are independent of the number
of input polynomials. As special cases of this algorithm, new and
improved algorithms for deciding a sentence in the first order theory
over real closed fields, and also for solving the existential problem
in the first order theory over real closed fields, are obtained.

\end{abstract}

\begin{categories}

F.4.3 [\textbf{Mathematical Logic and Formal Languages}]: Formal
Languages---\emph{decision problems}

\end{categories}

\begin{terms}

Algorithms, Theory

\end{terms}

\begin{keywords}

Quantifier elimination, real closed fields, Tarski-Seidenberg principle

\end{keywords}

\end{document}
