The real type of a finite family of univariate polynomials characterizes the combined sign behavior of the polynomials over the real line. We derive explicit formulas for numbers of real types subject to various degree bounds. For the special case of a single polynomial we present a closed-form expression involving Fibonacci numbers. This allows us to precisely describe the asymptotic growth of the number of real types as the degree increases, in terms of the golden ratio.

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 non-parametric 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.

In 1988, Weispfenning published a seminal paper introducing a substitution technique for quantifier elimination in the linear theories of ordered and valued fields. The original focus was on complexity bounds including the important result that the decision problem for Tarski Algebra is bounded from below by a double exponential function. Soon after, Weispfenning's group began to implement substitution techniques in software in order to study their potential applicability to real world problems. Today virtual substitution has become an established computational tool, which greatly complements cylindrical algebraic decomposition. There are powerful implementations and applications with a current focus on satisfiability modulo theory solving and qualitative analysis of biological networks.

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 mitogen-activated 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 11-dimensional 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 first-order logic with equality, which strictly generalizes two already well-known ones---the Bernays--Schönfinkel--Ramsey (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 non-elementary upper bound on the computing time required for deciding satisfiability in the new fragment. For the subfragment of prenex sentences with the quantifier prefix ∃*∀*∃* the satisfiability problem is shown to be complete for NEXPTIME. Finally, we discuss how automated reasoning procedures can take advantage of our results.

We describe a new incomplete but terminating heuristic 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 800,000 monomials in up to 10 variables with degrees up to 12. Our method has failed due to its incompleteness in only 10 percent of the cases.

We present the application of real quantifier elimination to formal verification and synthesis of continuous and switched dynamical systems. Through a series of case studies, we show how first-order formulas over the reals arise when formally analyzing models of complex control systems. Existing off-the-shelf quantifier elimination procedures are not successful in eliminating quantifiers from many of our benchmarks. We therefore automatically combine three established software components: virtual subtitution based quantifier elimination in Reduce/Redlog, cylindrical algebraic decomposition implemented in Qepcad, and the simplifier Slfq implemented on top of Qepcad. We use this combination to successfully analyze various models of systems including adaptive cruise control in automobiles, adaptive flight control system, and the classical inverted pendulum problem studied in control theory.

We generalize successful algorithmic ideas for quantified satisfiability solving to the parametric case where there are parameters in the input problem. The output is then not necessarily a truth value but more generally a propositional formula in the parameters of the input. Since one can naturally embed propositional logic into first-order logic over Boolean algebras, our work amounts from a model-theoretic point of view to a quantifier elimination procedure for initial Boolean algebras. Our work is completely and efficiently implemented in the logic package Redlog contained in the open source computer algebra system Reduce. We describe this implementation and discuss computation examples pointing at possible applications of our work to configuration problems in the automotive industry.

We introduce an efficient algorithm for determining a suitable projection order for performing cylindrical algebraic decomposition. Our algorithm is motivated by a statistical analysis of comprehensive test set computations. This analysis introduces several measures on both the projection sets and the entire computation, which turn out to be highly correlated. The statistical data also shows that the orders generated by our algorithm are significantly close to optimal.

This paper provides a starting point for generic quantifier elimination by partial cylindrical algebraic decomposition pcad. On input of a first-order formula over the reals generic pcad outputs a theory and a quantifier-free formula. The theory is a set of negated equations in the free variables of the input formula. The quantifier-free formula is equivalent to the input for all parameter values satisfying the theory. For obtaining this generic elimination procedure, we derive a generic projection operator from the standard Collins--Hong projection operator. Our operator particularly addresses formulas with many parameters thus filling a gap in the applicability of pcad. It restricts decomposition to a reasonable subset of the entire space. The above-mentioned theory describes this subset. The approach is compatible with other improvements in the framework of pcad. It turns out that the theory contains assumptions that are easily interpretable and that are most often non-degeneracy conditions. The applicability of our generic elimination procedure significantly extends that of the corresponding regular procedure. Our procedure is implemented in the computer logic system redlog.

We automatically check for the feasibility of arbitrary boolean combinations of linear parametric p-adic constraints using a quantier elimination method. This can be done uniformly for all p. We focus on the necessary simplication methods. Our method is implemented within the computer algebra system reduce. We illustrate the applicability of this implementation to non-trivial problems including the solution of systems of linear congruences over the integers. 1 Introduction It is well-known that linear parametric constraint solving over the reals has numerous important applications in science and engineering. The same holds for corresponding integer and mixed real-integer problems. In this article we consider analogue problems over p-adic numbers instead of real numbers. This also has important though less obvious applications, mainly in class eld theory and Diophantine analysis [Dub92]. One can, for instance, weaken the problem of nding integer solutions to a Diophantine ...

Special-purpose quanti er elimination procedures for problems of low degree using virtual substitution of test terms have recently turned out to be applicable to a variety of non-trivial non-academic problems.We study parallel algorithms based on these methods for several parallelization environments: a Cray YMP4/T3D, a workstation cluster, and a multi-processor Sparc.Our implementations show remarkable though sublinear speed-ups in all these environments.

Computer algebra systems typically drop some degenerate cases when evaluating expressions, e.g., z/z becomes ldropping the case z = O.We claim that it is feasible in practice to compute also the degenerate cases yielding guarded expressions.We work over real closed fields but our ideas about handling guarded expression can be easily transferred to other situations.Using formulas as guards provides a powerful tool for heuristically reducing the combinatorial explosion of cases: equivalent, redundant, tautological, and contradictive cases can be detected by simplification and quantifier elimination.Our approach simplifies the expressions on the basis of simplification knowledge on the logical side.The met hod described in this paper is implemented in the REDUCEpackage GUARDIAN,which is freely available on the WWW.