 | Xia B. Automated inequality proving and discovering / B.Xia, L.Yang. - Singapore; Hackensack, London: World Scientific, 2016. - xii, 332 p.: ill. - ISBN 978-981-4759-11-3
Шифр: (И/В16-X58) 02
|
Preface ......................................................... v
1 Basics of Elimination Method ............................... 1
1.1 Pseudo-division ............................................ 1
1.2 Resultants ................................................. 5
1.3 Subresultants .............................................. 8
1.3.1 The Habicht Theorem ................................ 10
1.3.2 Subresultant Chain Theorem ......................... 14
1.3.3 Subresultant Polynomial Remainder Sequence ......... 18
2 Zero Decomposition of Polynomial System ................... 25
2.1 Notations ................................................. 25
2.2 Wu's Zero Decomposition ................................... 26
2.3 Relatively Simplicial Decomposition (RSD) ................. 29
2.3.1 Regular Chain ...................................... 29
2.3.2 RSD ................................................ 32
2.4 Weakly RSD ................................................ 37
2.4.1 Concepts and Definitions ........................... 37
2.4.2 Algorithm WRSD ..................................... 40
2.4.3 Correctness of Algorithm WRSD ...................... 41
2.5 Generic Regular Decomposition ............................. 47
2.6 Zero Decomposition Keeping Multiplicity ................... 50
2.6.1 Multiplicity ....................................... 52
2.6.2 Zero Decomposition Keeping Multiplicity ............ 54
3 Triangularization of Semi-Algebraic System ................ 57
3.1 Triangular SAS ............................................ 58
3.2 Triangular Decomposition of SASs .......................... 60
3.2.1 Generic Zero-Dimensional Case ...................... 61
3.2.2 Positive Dimensional Case .......................... 66
4 Real Root Counting ........................................ 77
4.1 Classical Results ......................................... 77
4.2 Discrimination Systems for Polynomials .................... 83
4.3 Proof of Discrimination Theorem ........................... 92
4.4 Properties of Discrimination Matrix ....................... 97
5 Real Root Isolation ...................................... 109
5.1 Real Root Isolation for Polynomials ...................... 109
5.2 Real Root Isolation for Constant Semi-Algebraic Systems .. 112
5.2.1 Interval Arithmetic ............................... 113
5.2.2 Algorithm ......................................... 114
5.2.3 Examples .......................................... 119
5.3 Real Root Counting for Constant Semi-Algebraic Systems ... 121
5.4 Termination of Linear Programs ........................... 125
6 Real Root Classification ................................. 133
6.1 Border Polynomial and Discrimination Polynomial .......... 134
6.2 Generic Zero-Dimensional Case ............................ 135
6.2.1 Regular Zero-Dimensional TSA ...................... 135
6.2.2 Generic Zero-Dimensional SAS ...................... 139
6.2.3 Algorithm ......................................... 140
6.3 Positive Dimensional and Over-Determined Cases ........... 144
6.4 DISCOVERER ............................................... 148
6.5 Automated Discovering of Geometric Inequalities .......... 152
6.6 Algebraic Analysis of Biological Systems ................. 163
6.7 Program Verification Through SASs Solving ................ 169
6.7.1 Non-linear Ranking Function Discovering ........... 170
6.7.2 Reachability Computation .......................... 173
7 Open Weak CAD ............................................ 181
7.1 Quantifier Elimination and Cylindrical Algebraic
Decomposition ............................................ 182
7.2 Open CAD ................................................. 186
7.3 Projection Operator Np ................................... 190
7.3.1 An Illustrative Example ........................... 190
7.3.2 Notations ......................................... 192
7.3.3 Algorithm DPS ..................................... 193
7.3.4 The Correctness of Algorithm DPS .................. 196
7.3.5 Examples of Proving Polynomial Inequalities ....... 202
7.3.6 Polynomial Optimization via Np .................... 204
7.4 Open Weak CAD ............................................ 211
7.4.1 Concepts .......................................... 212
7.4.2 Projection Operator Hp ............................ 214
7.4.3 Computing Open Sample ............................. 224
7.4.4 Combining Hp and Np ............................... 226
7.4.5 Examples .......................................... 229
8 Dimension-Decreasing Algorithm ........................... 233
8.1 Inequalities with Radicals ............................... 233
8.2 Dimension-Decreasing Algorithm ........................... 235
8.2.1 Concepts .......................................... 235
8.2.2 Algorithm ......................................... 239
8.3 Inequalities on Triangles ................................ 240
8.4 BOTTEMA .................................................. 242
8.4.1 Inequality Proving with BOTTEMA ................... 244
8.4.2 Non-linear Optimization with BOTTEMA .............. 246
9 SOS Decomposition ........................................ 251
9.1 Preliminary .............................................. 253
9.2 Convex Cover Polynomial .................................. 257
9.3 Split Polynomial ......................................... 261
9.4 Algorithm ................................................ 264
9.5 Experiments .............................................. 269
10 Successive Difference Substitution ....................... 271
10.1 Basic Idea .......................................... 271
10.1.1 An Example ........................................ 271
10.1.2 Difference Substitution ........................... 273
10.1.3 Successive Difference Substitution ................ 278
10.2 Weighted Successive Difference Substitution ......... 283
10.2.1 Concepts .......................................... 283
10.2.2 Geometric Meaning ................................. 284
10.2.3 Termination ....................................... 287
10.3 Examples ................................................. 290
10.4 Polya's Theorem .......................................... 293
11 Proving Inequalities Beyond the Tarski Model ............. 297
11.1 Symmetric Forms of Degrees Less Than Five ................ 298
11.1.1 Problem ........................................... 298
11.1.2 Algorithm ......................................... 301
11.1.3 Examples and Discussion ........................... 306
11.2.4 Class of Symmetric Forms of Any Degrees ........... 307
11.2.1 Problem ........................................... 307
11.2.2 Algorithm ......................................... 309
11.2.3 Examples .......................................... 312
Bibliography .................................................. 315
Index ......................................................... 327
|
|
