arXiv subjects

Thomas Sturm

Publications and source records attributed to Thomas Sturm.

21 records · Page 2Linked to original sources

arXiv2015

A Generalized Framework for Virtual Substitution

We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in elimination sets using roots of parametric univariate polynomials described by Thom codes. Our approach follows an early suggestion by Weispfenning, which has never been carried out explicitly. Inspired by virtual substitution for linear formulas, we show how to systematically construct elimination sets containing only test points representing lower bounds.

cs.SC↗

arXiv2015

Better Answers to Real Questions

We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.

cs.SC↗

arXiv2015

Subtropical Real Root Finding

We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vectors associated with sign information on the coefficients. Then we employ linear programming to heuristically find roots. There is a specialized variant for roots with exclusively positive coordinates, which is of considerable interest for applications in chemistry and systems biology. An implementation of our method combining the computer algebra system Reduce with the linear programming solver Gurobi has been successfully applied to input data originating from established mathematical models used in these areas. We have solved several hundred problems with up to more than 800000 monomials in up to 10 variables with degrees up to 12. Our method has failed due to its incompleteness in less than 8 percent of the cases.

cs.SC↗