Automated Inequality Proving and Discovering

The following sections are included:

• Preface
• Contents

Pseudo-division and resultant are two basic tools used by many elimination methods and are also frequently used in many algorithms in this book. So, we begin with an introduction to some related concepts and results.

If not specified in this chapter, ℛ is a domain and univariate polynomials are in ℛ[x]. The degree of f ∈ ℛ[x] is denoted by deg(f, x) or deg(f).

The following sections are included:

• Notations
• Wu's Zero Decomposition
• Relatively Simplicial Decomposition (RSD)
  • Regular Chain
  • RSD
• Weakly RSD
  • Concepts and Definitions
  • Algorithm WRSD
  • Correctness of Algorithm WRSD
• Generic Regular Decomposition
• Zero Decomposition Keeping Multiplicity
  • Multiplicity
  • Zero Decomposition Keeping Multiplicity

The following system

Automated inequality proving and discovering rely on the methods and tools of computational real algebra and computational real algebraic geometry. From this chapter on, we start to discuss the problems related to the real solutions of polynomials, polynomial systems and semi-algebraic systems. In this chapter, after a quick review of some classical results on real root counting for polynomials, we introduce our contribution along this direction.

A univariate polynomial has only finitely many real roots. If a constant polynomial system or semi-algebraic system is given in this chapter, it is assumed to have only finitely many real solutions, too. Suppose a univariate polynomial (polynomial system / semi-algebraic system) has k distinct real solutions, roughly speaking, real root isolation means computing k disjoint regions to isolate all the distinct real solutions, with only one solution in each region.

Real root isolation for univariate polynomials (polynomial systems / semi-algebraic systems) with integer coefficients plays a significant role in many algorithms concerning computational real algebra and real algebraic geometry. In this chapter, we first introduce well-known algorithms for isolating real roots of polynomials. Then we present our contribution to real root isolation for constant semi-algebraic systems (SAS) based on triangularization of SAS (see Chapter 3) and interval arithmetic. Finally, we introduce our work on real root isolation for polynomial systems based on a combination of homotopy continuation method and interval arithmetic.

In this chapter, we discuss the so-called real root classification problem of parametric SAS in the form of (3.1), i.e. S : [P,G₁,G₂,H],

Open CAD (see Definition 7.8) can be applied to many problems involving only non-strict polynomial inequalities. Combined with “hierarchical strategy”, it is also applied to the real root classification problem (see Chapter 6). In this chapter, we consider the following three problems and introduce two new projection operators which may produce fewer sample points than the usual open CAD and thus lead to faster algorithms and tools for solving the three problems…

To prove an algebraic inequality with radicals, a common method is to introduce new variables for the radicals and transform the inequality to a polynomial inequality with some equational constraints. However, the new variables increase the dimension (number of variables) of the problem and thus often cause the problem intractable in practice. In this chapter, we introduce an algorithm, called dimension-decreasing algorithm, which can deal with radical inequalities efficiently and keep the dimension unchange.

Let us begin with an example. Prove that

Successive difference substitution was first introduced in [Yang (2005, 2006)] as a heuristic algorithm for proving nonnegativity of polynomials when all the variables are nonnegative. The method is incomplete but very efficient for many examples and can solve some large examples which cannot be solved by other tools. The method has been developed into a complete algorithm with some interesting connections to other methods by a series of work, see for example [Yao (2009); Yang and Yao (2009); Yao (2010); Xu and Yao (2011, 2012); Hou and Shao (2011)]. Based on these references, we introduce in this chapter basic concepts, ideas and recent advances of the method.

Propositions of elementary algebra and geometry (Tarski's model) are decidable by Tarski's work. For any given proposition inside Tarski's model, all the functions involved are polynomials in a fixed number of variables. In this chapter, we consider inequality proving problems where the number of variables is a variable or the functions are not polynomials, i.e. propositions beyond the Tarski model.

To have an idea of what we will talk about in this chapter, let us first see two concrete examples below.

The following sections are included:

• Bibliography
• Index