Search

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. [ABSTRACT FROM AUTHOR]

This paper shows that for any given polynomial ideal the collection of Gröbner cones corresponding to -specific elimination orders forms a star-shaped region which contrary to first intuition in general is not convex. Moreover we show that the corresponding region may contain Gröbner cones intersecting in the boundary of the Gröbner fan in the origin only. This implies that Gröbner walks aiming for the elimination of variables from a polynomial ideal can be terminated earlier than previously known. We provide a slightly improved stopping criterion for a known Gröbner walk algorithm for the elimination of variables. [ABSTRACT FROM AUTHOR]

Abstract: An improved algorithm, together with its implementation, is presented for the automatic computation of the complete root classification of a real parametric polynomial. The algorithm offers improved efficiency and a new test for non-realizable conditions. The improvement lies in the direct use of ‘sign lists’, obtained from the discriminant sequence, rather than ‘revised sign lists’. It is shown that the discriminant sequences, upon which the sign lists are based, are closely related both to Sturm–Habicht sequences and to subresultant sequences. Thus calculations based on any of these quantities are essentially equivalent. One particular application of complete root classifications is the determination of the conditions for the positive definiteness of a polynomial, and here the new algorithm is applied to a class of sparse polynomials. It is seen that the number of conditions for positive definiteness remains surprisingly small in these cases. [Copyright &y& Elsevier]

Abstract: Elimination is a classical subject. The problem is algorithmically solvable by using resultants or by one calculation of Groebner basis with respect to an elimination term order. However, there is no existing method that is both efficient and reliable enough for applicable size problems, say implicitization of bi-cubic Bezier surfaces with degree six in five variables. This basic and useful operation in computer aided geometric design and geometric modeling defies a solution even when approximation using floating-point or modular coefficients is used for Groebner basis computation. An elimination term order can be used to eliminate for any ideal in . However, for most practical problems we are given a fixed ideal, which means that an elimination term order may be too much for our calculation. In this paper, the author proposes a new approach for elimination. Instead of using a classical elimination term order for all problems or ideals as usual, the author proposes to use algebraic structures of the given system of equations for finding more suitable term orders for elimination of the given problem only. Experimental results showed that these ideal-specific term orders are much more efficient for elimination. In particular, when ideal specific term orders for elimination are used with Groebner walk conversion, one can completely avoid all perturbations. This is a significant result because researchers have been struggling with how to perturb basis conversions for a long time. [Copyright &y& Elsevier]

New formulae are given for Chow forms, discriminants and resultants arising from (not necessarily normal) toric varieties of codimension 2. The Newton polygon of the discriminant is determined exactly. [Copyright &y& Elsevier]

We report on our on-going efforts to apply real quantifier elimination to the synthesis of optimal numerical algorithms. In particular, we describe a case study on the square root problem: given a real number x and an error bound ε , find a real interval such that it contains x and its width is less than or equal to ε . A typical numerical algorithm starts with an initial interval and repeatedly updates it by applying a “refinement map” on it until it becomes narrow enough. Thus the synthesis amounts to finding a refinement map that ensures the correctness and optimality of the resulting algorithm. This problem can be formulated as a real quantifier elimination. Hence, in principle, the synthesis can be carried out automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general real quantifier elimination software. We overcame the difficulty by (1) carefully reducing a complicated quantified formula into several simpler ones and (2) automatically eliminating the quantifiers from the resulting ones using the state-of-the-art quantifier elimination software. As the result, we were able to synthesize semi-automatically an optimal quadratically 1 convergent map, which is better than the well known hand-crafted Secant-Newton map. Interestingly, the optimal synthesized map is not contracting as one would naturally expect. [ABSTRACT FROM AUTHOR]

Abstract: Let be a field of characteristic zero, any positive integer and let be the derivation of the polynomial ring in variables over . A Conjecture of Nowicki (Conjecture 6.9.10 in [Nowicki, A. 1994. Polynomial derivations and their rings of constants, Wydawnictwo Uniwersytetu Mikolaja Kopernika, Torun]) states the following in which case we say that is standard. In this paper, we use the elimination theory of Groebner bases to prove that Nowicki’s conjecture holds in the more general case of the derivation , . In [Kojima, H. Miyanishi, M. 1997. On Robert’s counterexample to the fourteenth problem of Hilbert, J. Pure Appl. Algebra 122, 277–292], Kojima and Miyanishi argued that is standard in the case where () for some . Although the result is true, we show in this paper that their proof is not complete. [Copyright &y& Elsevier]

A quantifier elimination algorithm by cylindrical algebraic decomposition based on regular chains is presented. The main idea is to refine a complex cylindrical tree until the signs of polynomials appearing in the tree are sufficient to distinguish the true and false cells. We report an implementation of our algorithm in the RegularChains library in Maple and illustrate its effectiveness by examples. [ABSTRACT FROM AUTHOR]

Given the equations of the first and the second order manifolds in R n , we construct the distance equation , i.e. a univariate algebraic equation one of the zeros of which (generically minimal positive) coincides with the square of the distance between these manifolds. To achieve this goal we employ Elimination Theory methods. In the frame of this approach we also deduce the necessary and sufficient algebraic conditions under which the manifolds intersect and propose an algorithm for finding the coordinates of their nearest points. The case of parameter dependent manifolds is also considered. [ABSTRACT FROM AUTHOR]

Abstract: We revisit in this paper the concept of decoding binary cyclic codes with Gröbner bases. These ideas were first introduced by Cooper, then Chen, Reed, Helleseth and Truong, and eventually by Orsini and Sala. We discuss here another way of putting the decoding problem into equations: the Newton identities. Although these identities have been extensively used for decoding, the work was done manually, to provide formulas for the coefficients of the locator polynomial. This was achieved by Reed, Chen, Truong and others in a long series of papers, for decoding quadratic residue codes, on a case-by-case basis. It is tempting to automate these computations, using elimination theory and Gröbner bases. Thus, we study in this paper the properties of the system defined by the Newton identities, for decoding binary cyclic codes. This is done in two steps, first we prove some facts about the variety associated with this system, then we prove that the ideal itself contains relevant equations for decoding, which lead to formulas. Then we consider the so-called online Gröbner basis decoding, where the work of computing a Gröbner basis is done for each received word. It is much more efficient for practical purposes than preprocessing and substituting into the formulas. Finally, we conclude with some computational results, for codes of interesting length (about one hundred). [Copyright &y& Elsevier]