ﻻ يوجد ملخص باللغة العربية
Quantifier elimination over the reals is a central problem in computational real algebraic geometry, polynomial system solving and symbolic computation. Given a semi-algebraic formula (whose atoms are polynomial constraints) with quantifiers on some variables, it consists in computing a logically equivalent formula involving only unquantified variables. When there is no alternation of quantifiers, one has a one block quantifier elimination problem. This paper studies a variant of the one block quantifier elimination in which we compute an almost equivalent formula of the input. We design a new probabilistic efficient algorithm for solving this variant when the input is a system of polynomial equations satisfying some regularity assumptions. When the input is generic, involves $s$ polynomials of degree bounded by $D$ with $n$ quantified variables and $t$ unquantified ones, we prove that this algorithm outputs semi-algebraic formulas of degree bounded by $mathcal{D}$ using $O {widetilde{~}}left ((n-s+1) 8^{t} mathcal{D}^{3t+2} binom{t+mathcal{D}}{t} right )$ arithmetic operations in the ground field where $mathcal{D} = 2(n+s) D^s(D-1)^{n-s+1} binom{n}{s}$. In practice, it allows us to solve quantifier elimination problems which are out of reach of the state-of-the-art (up to $8$ variables).
Given a straight-line program whose output is a polynomial function of the inputs, we present a new algorithm to compute a concise representation of that unknown function. Our algorithm can handle any case where the unknown function is a multivariate
In this paper we report on an application of computer algebra in which mathematical puzzles are generated of a type that had been widely used in mathematics contests by a large number of participants worldwide. The algorithmic aspect of our work pr
The only C*-algebras that admit elimination of quantifiers in continuous logic are $mathbb{C}, mathbb{C}^2$, $C($Cantor space$)$ and $M_2(mathbb{C})$. We also prove that the theory of C*-algebras does not have model companion and show that the theory
This paper is devoted to the study of the analytic properties of Mahler systems at 0. We give an effective characterisation of Mahler systems that are regular singular at 0, that is, systems which are equivalent to constant ones. Similar characterisa
The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, sets of polynomial constraints, is of particular importance. One of the