Automated Inequality Proving And Discovering

Bican Xia, Lu Yang

• Publisher: WSPC
• Year: 2016
• ISBN:
  9789814759137
• Topic: Mathematics
• Subtopic: Discrete Mathematics
• Index: Mathematics

This is the first book that focuses on practical algorithms for polynomial inequality proving and discovering. It is a summary of the work by the authors and their collaborators on automated inequality proving and discovering in recent years. Besides brief introduction to some classical results and related work in corresponding chapters, the book mainly focuses on the algorithms initiated by the authors and their collaborators, such as real root counting, real root classification, improved CAD projection, dimension-decreasing algorithm, difference substitution, and so on. All the algorithms were rigorously proved and the implementations are demonstrated by lots of examples in various backgrounds such as algebra, geometry, biological science, and computer science.

Contents:

• Preface
• Basics of Elimination Method
• Zero Decomposition of Polynomial System
• Triangularization of Semi-Algebraic System
• Real Root Counting
• Real Root Isolation
• Real Root Classification
• Open Weak CAD
• Dimension-Decreasing Algorithm
• SOS Decomposition
• Successive Difference Substitution
• Proving Inequalities Beyond the Tarski Model

Readership: Researchers and graduate students in computational real algebraic geometry, optimization and artificial intelligence.

Chapter 1

Basics of Elimination Method

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, R is a domain and univariate polynomials are in R[x]. The degree of f ∈ R[x] is denoted by deg(f, x) or deg(f).

1.1Pseudo-division

If K is a field, the Euclidean division in the Euclidean domain K[x] is well-known. For two polynomials f and g ≠ 0 in K[x], there exist q, r ∈ K[x] such that f = qg + r and deg(r, x) < deg(g, x). The polynomials q and r are called respectively the quotient and remainder of f divided by g and denoted by quo(f, g) and rem(f, g), respectively.

If R is a domain, the concept of division in R[x] is generalized to the so-called pseudo-division, for the element in R is not invertible in general.

Suppose

are polynomials in R[x] with m ≥ l. Construct a matrix as follows.

where all the other entries are zero except those of the coefficients of f and g. The ith column of M can be viewed as indexed by x^m−i+1. That is to say,

If R is a field or, at least, b_l is invertible, perform Gaussian elimination on M to get the following matrix

Then, the last row of the matrix is the remainder, i.e. r =

_i=0^l−1 r_ixⁱ is the remainder of f divided by g, denoted as r = rem(f, g).

If b_l is not invertible, we apply fraction-free Gaussian elimination on M as follows: First, multiply the last row by b_l and minus the product of the first row by a_m. Suppose the ith step (1 ≤ i < m − l + 1) is completed and the ith entry of the last row is c_i, multiply the last row by b_l and minus the product of the ith row by c_i. After m − l + 1 such transforma...