SUMMARY: Biological processes are often modeled by ordinary differential equations with unknown parameters. The unknown parameters are usually estimated from experimental data. In some cases, due to the structure of the model, this estimation problem does not have a unique solution even in the case of continuous noise-free data. It is therefore desirable to check the uniqueness a priori before carrying out actual experiments. We present a new software SIAN (Structural Identifiability ANalyser) that does this. Our software can tackle problems that could not be tackled by previously developed packages. AVAILABILITY AND IMPLEMENTATION: SIAN is open-source software written in Maple and is available at https://github.com/pogudingleb/SIAN. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

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.

We report on on-going efforts to apply real quantifier elimination to the synthesis of optimal numerical algorithms. In particular, we describe a case study on the square root problem: given a real number x and an error bound ε, find a real interval such that it contains [EQUATION] and its width is less than or equal to ε.

We study a variant of the real quantifier elimination problem (QE). The variant problem requires the input to satisfy a certain extra condition, and allows the ouput to be almost equivalent to the input. In a sense, we are strengthening the pre-condition and weakening the post-condition of the standard QE problem.

Composition is an operation of replacing variables in a polynomial with other polynomials. The main question of this paper is: When does composition commute with Groebner basis computation (possibly under different term orderings)? We prove that this happens if the leading terms of the composition polynomials form "permuted powering". This is a sequel to another paper where we dealt with a more restricted question (that required same term ordering).

An algorithm is given for constructing a quantifier free formula (a boolean expression of polynomial equations and inequalities) equivalent to a given formula of the form: (% c R)[azzz + alz + a. = O A F], where F is a quantifier free formula in Z1, . . . .z~, z, and az, al, ao are polynomials in z 1, . . . .Xr with real coefficients such that the system {az = O, al = O, a. = O} has no solution in Rr.Formulas of this form frequently occur in the context of constraint logic programming over the real numbers.The output formulas are made of resultants and two variants, which we call trace and slope resultants.Both of these variant resultants can be expressed as determinants of certain matrices.Problem In this section, we give an exact statement of the problem which will be tackled in the next section.First we introduce a few definitions in order to facilitate the subsequent discussions.Definition 1 (Atomic formula) An atomic formula in xl,..., XT is one of the forms: A = O, A # O, A >0, A <0, A ~O, and A ~O, where A is a polynomial in Il@l,.... z].].

An algorithm is given for eliminating the quantifier from a formula: (∃x ∈ R)[a2x2 + a1x + a0 = 0 ∧ F], where F is a quantifier free formula in x1,…,xr, x, and a2, a1, a0 are polynomials in x1, …, xr with real coefficients such that the system {a2=0, a1=0, a0=0} has no solution in R;r. The output formulas are made of resultants and their variants, which we call slope resultants. The slope resultants can be, like the resultants, expressed as determinants of certain matrices. If we allow the determinant symbol in the output, the computing time of the algorithm is linear in the length of the input. If not, the computing time is dominated by N(n2r+1l+n2rl2) where N is the number of polynomials in the input formula, r is the number of variables, n is the maximum of the degrees for every variable, and l is the maximum of the integer coefficient bit lengths. Experiments with implementation suggest that the algorithm is sufficiently efficient to be useful in practice.

Article Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination Share on Author: Hoon Hong View Profile Authors Info & Claims ISSAC '92: Papers from the international symposium on Symbolic and algebraic computationAugust 1992 Pages 177–188https://doi.org/10.1145/143242.143306Online:01 August 1992Publication History 38citation2,977DownloadsMetricsTotal Citations38Total Downloads2,977Last 12 Months5Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

The Cylindrical Algebraic Decomposition (CAD) method of Collins [5] decomposes r-dimensional Euclidean space into regions over which a given set of polynomials have constant signs. An important component of the CAD method is the projection operation: given a set A of r-variate polynomials, the projection operation produces a set P of (r - 1)-variate polynomials such that a CAD of r-dimensional space for A can be constructed from a CAD of (r-1)-dimensional space for P. In this paper, we present an improvement to the projection operation. By generalizing a lemma on which the proof of the original projection operation is based, we are able to find another projection operation which produces a smaller number of polynomials. Let m be the number of polynomials contained in A, and let n be a bound for the degree of each polynomial in A in the projection variable. The number of polynomials produced by the original projection operation is dominated by m2n3 whereas the number of polynomials produced by our projection operation is dominated by m2n2.