Thumbnail
Access Restriction
Subscribed

Author Basu, Saugata ♦ Pollack, Richard ♦ Roy, Marie-Franoise
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1996
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Tarski-Seidenberg principle ♦ Quantifier elimination ♦ Real closed fields
Abstract In this paper, a new algorithm for performing quantifier elimination from first order formulas over real closed fields in given. This algorithm improves the complexity of the asymptotically fastest algorithm for this problem, known to this data. A new feature of this algorithm is that the role of the algebraic part (the dependence on the degrees of the imput polynomials) and the combinatorial part (the dependence on the number of polynomials) are sparated. 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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1996-11-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 43
Issue Number 6
Page Count 44
Starting Page 1002
Ending Page 1045


Open content in new tab

   Open content in new tab
Source: ACM Digital Library