Details:
Title  Quantifier elimination for a class of exponential polynomial formulas  Author(s)  Zhuojun Liu, Ming Xu, Lu Yang  Type  Article in Journal  Abstract  Abstract Quantifier elimination is a foundational issue in the field of algebraic and logic computation. In firstorder logic, every formula is well composed of atomic formulas by negation, conjunction, disjunction, and introducing quantifiers. It is often made quite complicated by the occurrences of quantifiers and nonlinear functions in atomic formulas. In this paper, we study a class of quantified exponential polynomial formulas extending polynomial ones, which allows the exponential to appear in the first variable. We then design a quantifier elimination procedure for these formulas. It adopts the scheme of cylindrical decomposition that consists of four phases—projection, isolation, lifting, and solution formula construction. For the nonalgebraic representation, the triangular systems are introduced to define transcendental coordinates of sample points. Based on that, our cylindrical decomposition produces projections for input variables only. Hence the procedure is direct and effective.  Keywords  Exponential polynomials, Cylindrical algebraic decomposition, Quantifier elimination, Decision procedures, Interval arithmetic  ISSN  07477171 
URL 
http://www.sciencedirect.com/science/article/pii/S0747717114000832 
Language  English  Journal  Journal of Symbolic Computation  Volume  68, Part 1  Number  0  Pages  146  168  Year  2015  Edition  0  Translation 
No  Refereed 
No 
