China
Africa
Explore chapters and articles related to this topic
Two Decades of Multidimensional Systems Research and Future Trends
Published in Krzysztof Gałkowski, Jeff David Wood, Multidimensional Signals, Circuits and Systems, 2001
in (Lazard 1988) is problem-specific and is unsuitable for generalization to the higher-degree and multivariate eases. Л systematic scheme that leads to a set of inequalities involving the free variables, whose satisfaction will be necessary and sufficient for global posilivity or nonnegativity of any specified polynomial with literal coefficients, has been developed, recently (Bose & Charoenlarpnopparut 1998b). In particular, a procedure was advanced to determine a set of necessary and sufficient conditions lor an univariate polynomial of arbitrary but fixed degree to be globally nonnegative in terms of the literal coefficients of the polynomial based on the theory of quantifier elimination by the method of resultant and subrcsultants (Bose & Charoenlarpnopparut 1998b). That effort continued the resurgence of research in the further development of quantifier elimination procedures (Bose 1997) by cylindrical algebraic decomposition of the multidimensional Euclidean space into semi-algebraic cells such that the value of any multivariate polynomial in a set of such polynomials has constant sign (positive, negative, or zero). For lower degree polynomials the result in (Bose & Charoenlarpnopparut 1998b) is explicit in terms of the literal coefficients and provides a direct independent verification of the result in (Lazard 1988) for the fourth degree case. However, in general the conditions arrived at arc expressible as inequalities involving polynomial functions of the coefficients.
Context-dependent Reachability Analysis for Hybrid Systems
Published in Stuart H Rubin, Lydia Bouzar-Benlabiod, Reuse in Intelligent Systems, 2020
Stefan Schupp, Justin Winkens, Erika Ábrahám
Using quantifier elimination techniques, e.g., Fourier-Motzkin variable elimination, we can eliminate quantifiers in order to simplify the formulas. For the above example quantifier elimination shows that by letting time progress, x can take all values larger or equal 1: ∃t.∃xpre.t≥0∧1≤xpre∧xpre≤3∧t+xpre≤x∧x≤2t+xpre.⇔∃t.t≥0∧1≤3∧x−2t≤3∧1≤x−t∧x−2t≤x−t⇔1≤x∧−1≤x⇔1≤x
Conic optimization-based algorithms for nonnegative matrix factorization
Published in Optimization Methods and Software, 2023
Valentin Leplat, Yurii Nesterov, Nicolas Gillis, François Glineur
The argument is based on quantifier elimination theory, using the seminal result by Basu, Pollack and Roy [3]. Unfortunately, this approach cannot be used in practice, even for small size matrices, because of its high computational cost: although the term is a polynomial in F and N for K fixed, it grows extremely fast (and the hidden constants are usually very large). Let us illustrate with a 4-by-4 matrix with K = 3, we have a complexity of order and for a 5-by-5 matrix with K = 4, the complexity raises up to . Therefore developing an effective computational technique for exact NMF of small matrices is an important direction of research. Some heuristics have been recently developed that allow solving exact NMF for matrices up to a few dozen rows and columns [29].
Atom-canonicity in varieties of cylindric algebras with applications to omitting types in multi-modal logic
Published in Journal of Applied Non-Classical Logics, 2020
Let T be as given in a signature L having n variables. Let , and . Then is a non-principal ultrafilter; maximality follows from the completeness of types considered. By completeness of T, is simple. Since T admits elimination of quantifiers, then . Indeed, let be the theory in the same signature L but using ω many variables. Let be the Tarski–Lindenbaum quotient cylindric algebra. Then (because we have ω many variables); in fact , and the map Φ defined from to via is injective and bijective, that is to say, Φ having domain and codomain is in fact onto due to quantifier elimination. An application of Theorem 5.13 finishes the proof.