English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In this paper, we give a new algorithm for quantifier elimination in the first order theory of real closed fields that improves the complexity of the best known algorithm for this problem till now. Unlike previously known algorithms [Basu et al. 1996; Renegar 1992; Heintz et al. 1990], the combinatorial part of the complexity (the part depending on the number of polynomials in the input) of this new algorithm is independent of the number of free variables. Moreover, under the assumption that each polynomial in the input depends only on a constant number of the free variables, the algebraic part of the complexity(the part depending on the degrees of the input polynomials) can also be made independent of the number of free variables. This new feature of our algorithm allow us to obtain a new algorithm for a variant of the quantifier elimination problem. We give an almost optimal algorithm for this new problem, which we call the uniform quantifier elimination problem.Using tthe uniform quantifier elimination algorithm, we give an algorithm for solving a problem arising in the field of constraint databases with real polynomial constraints. We give an algorithm for converting a query with natural domain semantics to an equivalent one with active domain semantics. A nonconstructive version of this result was proved in Benedikt et al. [1998]. Very recently, a constructive proof was also given independently in Benedikt and Libkin [1997]. However, complexity issues were not considered and no algorithm with a reasonable complexity bound was known for this latter problem till now.We also point out interesting logical consequences of this algorithmic result, concerning the expressive power of a constraint query language over the reals. This leads to simpler and constructive proofs for these inexpressibility results than the ones known before.Moreover, our improved algorithm for performing quantifier elimination immediately leads to improved algorithms for several problems for which quantifier elimination is a basic step, for example, the problem of computing the closure of a given semi-algebraic set.

New results on quantifier elimination over real closed fields and applications to constraint databases