Quantifier elimination for a class of exponential polynomial formulas. (May 2015)

• Record Type: Journal Article
• Authors: Xu, Ming; Li, Zhi-Bin; Yang, Lu
• Is Part Of: Journal of symbolic computation. Volume 68:Part 1(2015)
• Page Start: 146
• Page End: 168
• Publication Date: 2015-05
• Subjects: 03C10 -- 14Q15 -- 68W30; Exponential polynomials -- Cylindrical algebraic decomposition -- Quantifier elimination -- Decision procedures -- Interval arithmetic; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2014.09.015
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: 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.