Mathematics Mechanization

数学机械化

Price: $65.00


Qty. 

Author: Wu Wenjun
Language: English
ISBN/ISSN: 7030066863
Published on: 2000-01
Hardcover

The present book is actually a collection of essays by the author since 1977 centered around the subject which has been baptized mathematics mechanization.The subject tries to deal with mathematics in a constructive and algorithmic manner so that the reasonings become mechanical, automated,and as much as possible to be intelligence-lacking, with the result of lessening the painstaking heavy brainlabor.
The desire of getting mathematics mechanized or more generally of getting all kinds of reasonings automated, may be traced back to G. W. Leibniz (1646--1716). However, the real founding of mathematics mechanization, or more generally automated reasoning, should be, in the author's opinion, attributed to D.Hilbert (1862--1943). The great merit of Hilbert on mathematics mechanization seems to be long time overshadowed by his great success on his existence proof of finite basis theorem and his works on mathematics axiomatization, as well as his controversies with L. Kronecker (1823--1891) , who may be considered as one of the banner-holders of mathematics mechanization. In spite of these, Hilbert is well-deserved to be the real founder of mathematics mechanization, as reflected by his other kinds of great achievements or influences, for which some examples are listed below:
Example 1 In Hilbert's famous speech on mathematical problems in 1900,Problem 10 asks for an automated method of diophantine equations-solving.Though the Problem has been solved in the negative in 1970 by Matijasevic, the positive aspects of the negative solution have been shown to be able to bear extremely important consequences to modern pure mathematics. See, e. g. , the paper of M. Davis, et al in Proc. Symp. in Pure Math. , vol. 28, (1976).
Example 2 In Hilbert's classic Grundlagen der Geometric in 1899, there is some obscure passage, which, when reinterpreted, is equivalent to an automated method of proving a whole class of geometry theorems of some special type. The well-known theorem of Tarski in 1950 and the latter developments of the author on mechanical geometry theorem-proving are nothing else but continuation of this method of Hilbert in the narrow realm of elementary geometry. For this reason the author has baptized the above result of Hilbert, formulated as Theorem 62 in latter editions of Grundlagen, Hilbert' s Mechanization Theorem.
Example 3 Hilbert's program about consistency of mathematics implies a program of automated proving of all theorems in mathematics by a universal method. The discovery of Goedel has declared the collapse of Hilbert's program as being too ambitious to be realizable. Nonetheless Hilbert's efforts have given rise to a new discipline mathematical logic and show a new way of proving theorems or solving problems class by class under the name of decidability of which Hilbert's Mechanization Theorem furnishes a simple but extremely deep and instructive example. It opens a new way of dealing with mathematics: mechanization of mathematics.
Besides these we may note that there are papers of Hilbert with theorems proved in a constructive and algorithmic manner. As an example, we may cite the proof of the theorem concerning what we call nowadays Hilbert function of an ideal. We may even note that the proof of his finite basis theorem is achieved in forming the finite basis in a somewhat consructive and algorithmic manner.
The present book may be considered as a primary development of mathematics mechanization along the line of thought of Hilbert.
The whole book is divided into three parts. Part I concerns historical developments of mathematics mechanization, with emphasis on the developments in ancient China. This is quite natural. In fact, in contrast to the modern development of pure mathematics in accordance to the Euclidean axiomatic pattern of ancient Greece, the ancient mathematics of China is highly constructive, algorithmic and computational in character, with most of the results expressed in the form of algorithms. Even in geometry, the ancient Chinese mathematicians paid little attention to geometry theorem-proving. On the contrary, they devoted themselves rather on geometry problem-solving which leads naturally to the solving of polynomial equations. Accordingly, the problem of polynomial equations-solving occupies a central position throughout thousands of years of development of mathematics in ancient China. In the present book we follow closely the tradition of our ancient mathematics in focusing on polynomial equations-solving with getry theorem-proving and geometry problem-solving as its two main applications. This attitude of treatment is well-reflected in the subtitles of the present book.
Part II, which contains the three chapters 3, 4, and 5 , bears the title of Principles and Methods. It aims at the description of the underlying Principle of polynomial equations-solving, with polynomial coefficients in fields restricted to the case of characteristic 0. Based on the general Principle, we show how general Methods of solving such arbitrary polynomial systems may be found. In order to achieve this we shall use the naive notion of zero-sets of polynomial sets in forsaking the usual notions of ideals. An analysis of the zero-set of a polynomial set , under the guidelines of the Principle gives rise to the fundamental notion of characteristic set (abbr. char-set) and the further Principles under the names: Well-Ordering Principle, Zero-Decomposition Theorems, and Variety-Decomposition Theorem. These Principles form the basis of actual polynomial equations-solving.
It is to be noted that the underlying Principle of polynomial equations-solving had its origin in ancient Chinese mathematics, notably in the classic Jade Mirror of Four Elements in the year +1303 of Zhu Szijie. Of course, there are incompleteness and deficiencies in Zhu's work, but uncontestedly it shows the right way of solving arbitrary systems of polynomial equations. To complete the way indicated in Zhu's work we have relied upon the important works of J. F. Ritt as exhibited in his two classics on the algebraic studies of differential equations. Ritt's theory and method are highly constructive , algorithmic , and computational in character which rely in turn heavily on the early works of Van der Waerden on algebraic geometry. In contrast to the later developments of modern algebraic geometry, the early works of Van der Waerden on algebraic geometry is essentially constructive ,algorithmic ,and in the main computational. It is based on the very useful notions of generic point and specialization ,which have unfortunately disappeared in modern algebraic geometry. As a concrete application of Van der Waerden's treatment, we show in Sect. 3 of Chap. 5,how to define the important notions of Chern classes and Chern numbers of algebraic varieties with arbitrary singularities,based on the notion of generic points. Though there are diverse alternative definitions for getting such extended notions of Chern classes but not of Chern numbers,our treatment has the peculiarity of being computational,giving for example the remarkable Miyaoka-Yau inequality and its extensions by mere simple computations. We refer this to Sect. 3 of Chap. 5. A further application of this notion of generic pointis is given in Sect. 4 of Chap. 8 in Part III.
Usually polynomial equations are to be solved in the complex field. However,to solve in real field is obvriously of utmost importance. An example is furnished by optimization problems for which only real solutions are to be considered. The general method given in Chap. 3, which permits to give,theoretically speaking, a complete answer to the problem of polynomial equations-solving in the complex case , furnishes however merely a very incomplete answer with only partial success in the real case. In Sect. 5 of Chap. 5, we point out that, for the important optimization problems ,the polynomial case is quite different from the general differential case. In fact, we show that, in the polynomial case of optimization problems,there is a finite set of real values , for which the optimal value, supposed existing,is just the optimal value of this finite set. Our method permits also to give partial success for problems involving inequalities. However , the method is far from being satisfactory and much has to be done in the realm of problems in the real field.
Part III ,containing chapters 6,7, and 8, bears the title of Applications and Examples. Chap. 6 concerns applications to polynomial equations-solving. Remark that,though our principles and methods developed in Part II theoretically furnish complete solutions of arbitrary polynomial equations over fields of characteristic 0,the computational complexity is so high that, in actual computations one meets often unsurmountable complications to be able to carry out the computations up to the end. It seems that the only issue is to find some hybrid method of combining our symbolic computations with the usual numerical computations. We give such a hybrid method in Sect. 2 of Chap. 6 with a sound theoretical basis. The author believes that the method will actually permit us to settle the question for all kinds of problems arising from practical applications but experiments are yet to be done.
Chap. 7 of Part III deals with geometry theorem-proving which is treated as applications of our general principles and methods of polynomial equations-solving.Chap. 8 of Part III deals with diverse problems which, in apparence having nothing to do with polynomial equations , are reduced to some form of polynomial equations-solving and then treated by our general methods.
As a preliminary step toward mathematics mechanization,the present book has to be restricted to the polynomial case for equations-solving , and mainly to elementary geometries for theorem-proving and problem-solving. Only some indications about possible developments in differential geometry and differential equations are slightly touched in the last section, Sect. 5 of Chap. 8. We shall leave the studies of mathematics mechanization in the differential case and in other domains of mathematics in latter occasions.
The author would like to take this oppotunity to express his deep gratitudes to the State Science and Technology Commission, the National Natural Science Foundation of China , and the Chinese Academy of Sciences. Without their financial supports and encouragements mathematics mechanization is impossible to be so prosperous in China , today , and also tomorrow.
The author would like also to express his deep gratitudes to his friends and colleagues, especially those in Mathematics Mechanization Research Center (MMRC) of Institute of Systems Science, CAS, who have contributed so much to the development of mathematics mechanization, and to the writing of the present book. As they are so numerous and most of their names are scattered throughout the whole book , the author would like to apologize for not mentioning their names here in the Preface.PREFACE
The present book is actually a collection of essays by the author since 1977 centered around the subject which has been baptized mathematics mechanization.The subject tries to deal with mathematics in a constructive and algorithmic manner so that the reasonings become mechanical, automated,and as much as possible to be intelligence-lacking, with the result of lessening the painstaking heavy brainlabor.
The desire of getting mathematics mechanized or more generally of getting all kinds of reasonings automated, may be traced back to G. W. Leibniz (1646--1716). However, the real founding of mathematics mechanization, or more generally automated reasoning, should be, in the author's opinion, attributed to D.Hilbert (1862--1943). The great merit of Hilbert on mathematics mechanization seems to be long time overshadowed by his great success on his existence proof of finite basis theorem and his works on mathematics axiomatization, as well as his controversies with L. Kronecker (1823--1891) , who may be considered as one of the banner-holders of mathematics mechanization. In spite of these, Hilbert is well-deserved to be the real founder of mathematics mechanization, as reflected by his other kinds of great achievements or influences, for which some examples are listed below:
Example 1 In Hilbert's famous speech on mathematical problems in 1900,Problem 10 asks for an automated method of diophantine equations-solving.Though the Problem has been solved in the negative in 1970 by Matijasevic, the positive aspects of the negative solution have been shown to be able to bear extremely important consequences to modern pure mathematics. See, e. g. , the paper of M. Davis, et al in Proc. Symp. in Pure Math. , vol. 28, (1976).
Example 2 In Hilbert's classic Grundlagen der Geometric in 1899, there is some obscure passage, which, when reinterpreted, is equivalent to an automated method of proving a whole class of geometry theorems of some special type. The well-known theorem of Tarski in 1950 and the latter developments of the author on mechanical geometry theorem-proving are nothing else but continuation of this method of Hilbert in the narrow realm of elementary geometry. For this reason the author has baptized the above result of Hilbert, formulated as Theorem 62 in latter editions of Grundlagen, Hilbert' s Mechanization Theorem.
Example 3 Hilbert's program about consistency of mathematics implies a program of automated proving of all theorems in mathematics by a universal method. The discovery of Goedel has declared the collapse of Hilbert's program as being too ambitious to be realizable. Nonetheless Hilbert's efforts have given rise to a new discipline mathematical logic and show a new way of proving theorems or solving problems class by class under the name of decidability of which Hilbert's Mechanization Theorem furnishes a simple but extremely deep and instructive example. It opens a new way of dealing with mathematics: mechanization of mathematics.
Besides these we may note that there are papers of Hilbert with theorems proved in a constructive and algorithmic manner. As an example, we may cite the proof of the theorem concerning what we call nowadays Hilbert function of an ideal. We may even note that the proof of his finite basis theorem is achieved in forming the finite basis in a somewhat consructive and algorithmic manner.
The present book may be considered as a primary development of mathematics mechanization along the line of thought of Hilbert.
The whole book is divided into three parts. Part I concerns historical developments of mathematics mechanization, with emphasis on the developments in ancient China. This is quite natural. In fact, in contrast to the modern development of pure mathematics in accordance to the Euclidean axiomatic pattern of ancient Greece, the ancient mathematics of China is highly constructive, algorithmic and computational in character, with most of the results expressed in the form of algorithms. Even in geometry, the ancient Chinese mathematicians paid little attention to geometry theorem-proving. On the contrary, they devoted themselves rather on geometry problem-solving which leads naturally to the solving of polynomial equations. Accordingly, the problem of polynomial equations-solving occupies a central position throughout thousands of years of development of mathematics in ancient China. In the present book we follow closely the tradition of our ancient mathematics in focusing on polynomial equations-solving with getry theorem-proving and geometry problem-solving as its two main applications. This attitude of treatment is well-reflected in the subtitles of the present book.
Part II, which contains the three chapters 3, 4, and 5 , bears the title of Principles and Methods. It aims at the description of the underlying Principle of polynomial equations-solving, with polynomial coefficients in fields restricted to the case of characteristic 0. Based on the general Principle, we show how general Methods of solving such arbitrary polynomial systems may be found. In order to achieve this we shall use the naive notion of zero-sets of polynomial sets in forsaking the usual notions of ideals. An analysis of the zero-set of a polynomial set , under the guidelines of the Principle gives rise to the fundamental notion of characteristic set (abbr. char-set) and the further Principles under the names: Well-Ordering Principle, Zero-Decomposition Theorems, and Variety-Decomposition Theorem. These Principles form the basis of actual polynomial equations-solving.
It is to be noted that the underlying Principle of polynomial equations-solving had its origin in ancient Chinese mathematics, notably in the classic Jade Mirror of Four Elements in the year +1303 of Zhu Szijie. Of course, there are incompleteness and deficiencies in Zhu's work, but uncontestedly it shows the right way of solving arbitrary systems of polynomial equations. To complete the way indicated in Zhu's work we have relied upon the important works of J. F. Ritt as exhibited in his two classics on the algebraic studies of differential equations. Ritt's theory and method are highly constructive , algorithmic , and computational in character which rely in turn heavily on the early works of Van der Waerden on algebraic geometry. In contrast to the later developments of modern algebraic geometry, the early works of Van der Waerden on algebraic geometry is essentially constructive ,algorithmic ,and in the main computational. It is based on the very useful notions of generic point and specialization ,which have unfortunately disappeared in modern algebraic geometry. As a concrete application of Van der Waerden's treatment, we show in Sect. 3 of Chap. 5,how to define the important notions of Chern classes and Chern numbers of algebraic varieties with arbitrary singularities,based on the notion of generic points. Though there are diverse alternative definitions for getting such extended notions of Chern classes but not of Chern numbers,our treatment has the peculiarity of being computational,giving for example the remarkable Miyaoka-Yau inequality and its extensions by mere simple computations. We refer this to Sect. 3 of Chap. 5. A further application of this notion of generic pointis is given in Sect. 4 of Chap. 8 in Part III.
Usually polynomial equations are to be solved in the complex field. However,to solve in real field is obvriously of utmost importance. An example is furnished by optimization problems for which only real solutions are to be considered. The general method given in Chap. 3, which permits to give,theoretically speaking, a complete answer to the problem of polynomial equations-solving in the complex case , furnishes however merely a very incomplete answer with only partial success in the real case. In Sect. 5 of Chap. 5, we point out that, for the important optimization problems ,the polynomial case is quite different from the general differential case. In fact, we show that, in the polynomial case of optimization problems,there is a finite set of real values , for which the optimal value, supposed existing,is just the optimal value of this finite set. Our method permits also to give partial success for problems involving inequalities. However , the method is far from being satisfactory and much has to be done in the realm of problems in the real field.
Part III ,containing chapters 6,7, and 8, bears the title of Applications and Examples. Chap. 6 concerns applications to polynomial equations-solving. Remark that,though our principles and methods developed in Part II theoretically furnish complete solutions of arbitrary polynomial equations over fields of characteristic 0,the computational complexity is so high that, in actual computations one meets often unsurmountable complications to be able to carry out the computations up to the end. It seems that the only issue is to find some hybrid method of combining our symbolic computations with the usual numerical computations. We give such a hybrid method in Sect. 2 of Chap. 6 with a sound theoretical basis. The author believes that the method will actually permit us to settle the question for all kinds of problems arising from practical applications but experiments are yet to be done.
Chap. 7 of Part III deals with geometry theorem-proving which is treated as applications of our general principles and methods of polynomial equations-solving.Chap. 8 of Part III deals with diverse problems which, in apparence having nothing to do with polynomial equations , are reduced to some form of polynomial equations-solving and then treated by our general methods.
As a preliminary step toward mathematics mechanization,the present book has to be restricted to the polynomial case for equations-solving , and mainly to elementary geometries for theorem-proving and problem-solving. Only some indications about possible developments in differential geometry and differential equations are slightly touched in the last section, Sect. 5 of Chap. 8. We shall leave the studies of mathematics mechanization in the differential case and in other domains of mathematics in latter occasions.
The author would like to take this oppotunity to express his deep gratitudes to the State Science and Technology Commission, the National Natural Science Foundation of China , and the Chinese Academy of Sciences. Without their financial supports and encouragements mathematics mechanization is impossible to be so prosperous in China , today , and also tomorrow.
The author would like also to express his deep gratitudes to his friends and colleagues, especially those in Mathematics Mechanization Research Center (MMRC) of Institute of Systems Science, CAS, who have contributed so much to the development of mathematics mechanization, and to the writing of the present book. As they are so numerous and most of their names are scattered throughout the whole book , the author would like to apologize for not mentioning their names here in the Preface.

Part Ⅰ Historical Developments
Chapter Ⅰ Polynomial Equations-Solving in Ancient Times, Mainly in Ancient China
1.1 A Brief Description of History of Ancient China and Mathematics Classics in Ancient China
1.2 Polynomial Equations-Solving in Ancient China
1.3 Polynomial Equations-Solving in Ancient Times beyond China and the Program of Descartes
Chapter Ⅱ Historical Development of Geometry Theorem-Proving and Geometry Problem-Solving in Ancient Times
2.1 Geometry Theorem-Proving from Euclid to Hilbert
2.2 Geometry Theorem-Proving in the Computer Age
2.3 Geometry Problem-Solving and Geometry Theorem-Proving in Ancient China
Part Ⅱ Principles and Methods
Chapter Ⅲ Algebraic Varieies as Zero-Sets and Characteristic-Set Method
3.1 At fine and Projective Space Extended Points and Specialization
3.2 Algebraic Varieties and Zero Sets
3.3 Polsets and Ascending Sets. Partial Ordering
3.4 Characteristic Set of a Polset and the Well-Ordering Principle
3.5 Zero-Decomposition Theorems
3.6 Variety-Decomposition Theorems
Chapter Ⅳ Some Topics in Computer Algebra
4.1 Tuples of Integers
4.2 Well-Arranged Basis of a Polynomial Ideal
4.3 Well-Behaved Basis of a Polynomial Ideal
4.4 Properties of Well-Behaved Basis and its Relationship with Groebner Basis
4.5 Factorization and GCD of Multivariate Polynomials over Arbitrary Extension Fields
Chapter Ⅴ Some Topics in Computational Algebraic Geometry
5.1 Some Important Characters of Algebraic Varieties Complex and Real Varieties
5.2 Algebraic Correspondence and Chow Form
5.3 Chern Classes and Chern Numbers of an Irreducible Algebraic Variety with Arbitrary Singularities
5.4 A Projection Theorem on Quasi-Varieties
5.5 Extremal Properties of Real Polynomials
Part Ⅲ Applications and Examples
Chapter Ⅵ Appiications to Polynomial Equations-Solving
6.1 Basic Principles of Polynomial Equations-Solving; The Char-Set Method
6.2 A Hybrid Method of Polynomial Equations-Solving
6.3 Solving of Problems in Enumerative Geometry
6.4 Central Configurations in Planet Motions and Vortex Motions
6.5 Solving of Inverse Kinematic Equations in Robotics
Chapter Ⅶ Applications to Geometry Theorem-Proving
7.1 Basic Principles of Mechanical Geometry Theorem-Proving
7.2 Mechanical Proving of Geometry Theorems of Hilbertian Type
7.3 Mechanical Proving of Geometry Theorems Involving Equalities Alone
7.4 Mechanical Proving of Geometry Theorems Involving Inequalities
Chapter Ⅷ Diverse Applications
8.1 Applications to Automated Discovering of Unknown Relations and Automated Determination of Geometry Loci
8.2 Applications to Problems involving Inequalities,Optimization Problems, and NonLinear Programming
8.3 Applications to 4-Bar Linkage Design
8.4 Applications to Surface-Fitting Problem in CAGD
8.5 Some Miscellaneous Complements and Extensions?
Bibliography



Sorry we ran out!

Fill out this form and we will let you know when it comes back in stock

Copyright © 2024 China Scientific Books.