
We consider systems of strict multivariate polynomial inequalities over the
reals. All polynomial coefficients are parameters ranging over the reals, where
for each coefficient we prescribe its sign. We are interested in the existence
of positive real solutions of our system for all choices of coefficients
subject to our sign conditions. We give a decision procedure for the existence
of such solutions. In the positive case our procedure yields a parametric
positive solution as a rational function in the coefficients. Our framework
allows to reformulate heuristic subtropical approaches for nonparametric
systems of polynomial inequalities that have been recently used in qualitative
biological network analysis and, independently, in satisfiability modulo theory
solving. We apply our results to characterize the incompleteness of those
methods.

Quantifierfree nonlinear arithmetic (QF_NRA) appears in many applications of
satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning
for corresponding constraints in SMT theory solvers is highly relevant. We
propose a new incomplete but efficient and terminating method to identify
satisfiable instances. The method is derived from the subtropical method
recently introduced in the context of symbolic computation for computing real
zeros of single very large multivariate polynomials. Our method takes as input
conjunctions of strict polynomial inequalities, which represent more than 40%
of the QF_NRA section of the SMTLIB library of benchmarks. The method takes an
abstraction of polynomials as exponent vectors over the natural numbers tagged
with the signs of the corresponding coefficients. It then uses, in turn, SMT to
solve linear problems over the reals to heuristically find suitable points that
translate back to satisfying points for the original problem. Systematic
experiments on the SMTLIB demonstrate that our method is not a sufficiently
strong decision procedure by itself but a valuable heuristic to use within a
portfolio of techniques.

We investigate models of the mitogenactivated protein kinases (MAPK) network,
with the aim of determining where in parameter space there exist multiple
positive steady states. We build on recent progress which combines various
symbolic computation methods for mixed systems of equalities and inequalities.
We demonstrate that those techniques benefit tremendously from a newly
implemented graph theoretical symbolic preprocessing method. We compare
computation times and quality of results of numerical continuation methods with
our symbolic approach before and after the application of our preprocessing.

We consider the problem of determining multiple steady states for positive
real values in models of biological networks. Investigating the potential for
these in models of the mitogenactivated protein kinases (MAPK) network has
consumed considerable effort using special insights into the structure of
corresponding models. Here we apply combinations of symbolic computation
methods for mixed equality/inequality systems, specifically virtual
substitution, lazy real triangularization and cylindrical algebraic
decomposition. We determine multistationarity of an 11dimensional MAPK network
when numeric values are known for all but potentially one parameter. More
precisely, our considered model has 11 equations in 11 variables and 19
parameters, 3 of which are of interest for symbolic treatment, and furthermore
positivity conditions on all variables and parameters.

We introduce a new decidable fragment of firstorder logic with equality,
which strictly generalizes two already wellknown ones  the
BernaysSch\"onfinkelRamsey (BSR) Fragment and the Monadic Fragment. The
defining principle is the syntactic separation of universally quantified
variables from existentially quantified ones at the level of atoms. Thus, our
classification neither rests on restrictions on quantifier prefixes (as in the
BSR case) nor on restrictions on the arity of predicate symbols (as in the
monadic case). We demonstrate that the new fragment exhibits the finite model
property and derive a nonelementary upper bound on the computing time required
for deciding satisfiability in the new fragment. For the subfragment of prenex
sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the
satisfiability problem is shown to be complete for NEXPTIME. Finally, we
discuss how automated reasoning procedures can take advantage of our results.

We consider feasibility of linear integer programs in the context of
verification systems such as SMT solvers or theorem provers. Although
satisfiability of linear integer programs is decidable, many stateoftheart
solvers neglect termination in favor of efficiency. It is challenging to design
a solver that is both terminating and practically efficient. Recent work by
Jovanovic and de Moura constitutes an important step into this direction. Their
algorithm CUTSAT is sound, but does not terminate, in general. In this paper we
extend their CUTSAT algorithm by refined inference rules, a new type of
conflicting core, and a dedicated rule application strategy. This leads to our
algorithm CUTSAT++, which guarantees termination.

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.

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 postprocessing 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.

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.