Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleQuantifier elimination for a class of exponential polynomial formulas
Author(s) Zhuojun Liu, Ming Xu, Lu Yang
TypeArticle in Journal
AbstractAbstract Quantifier elimination is a foundational issue in the field of algebraic and logic computation. In first-order 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 non-algebraic 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.
KeywordsExponential polynomials, Cylindrical algebraic decomposition, Quantifier elimination, Decision procedures, Interval arithmetic
URL http://www.sciencedirect.com/science/article/pii/S0747717114000832
JournalJournal of Symbolic Computation
Volume68, Part 1
Pages146 - 168
Translation No
Refereed No