Chou S.-C. - Mechanical geometry theorem proving
||Mechanical geometry theorem proving
||Growing specialization and diversification have brought a host of monographs and textbooks on increasingly specialized topics. However, the "tree" of knowledge of mathematics and related fields does not grow only by putting forth new branches. It also happens, quite often in fact, that branches which were thought to be completely disparate are suddenly seen to be related.
Further, the kind and level of sophistication of mathematics applied in various sciences has changed drastically in recent years: measure theory is used (non-trivially) in regional and theoretical economics; algebraic geometry interacts with physics; the Minkowsky lemma, coding theory and the structure of water meet one another in packing and covering theory; quantum fields, crystal defects and mathematical programming profit from homotopy theory; Lie algebras are relevant to filtering; and prediction and electrical engineering can use Stein spaces. And in addition to this there are such new emerging subdisciplines as "experimental mathematics", "CFD", "completely integrable systems", "chaos, synergetics and large-scale order", which are almost impossible to fit into the existing classification schemes. They draw upon widely different sections of mathematics. This programme, Mathematics and Its Applications, is devoted to new emerging (sub)disciplines and to such (new) interrelations as exempla gratia:
- a central concept which plays an important .role in several different mathematical and/or scientific specialized areas;
- new applications of the results and ideas from one area of scientific endeavour into another;
- influences which the results, problems and concepts of one field of enquiry have and have had on the development of another.
The Mathematics and Its Applications programme tries to make available a careful selection of books which fit the philosophy outlined above. With such books, which are stimulating rather than definitive, intriguing rather than encyclopaedic, we hope to contribute something towards better communication among the practitioners in diversified fields.
This is a book about automatic theorem proving. I have no difficulty in picturing sceptical smiles on the faces of many colleagues upon hearing this phrase. Indeed, if the phrase is taken in the sense of replacing most of the activities of the modern professional mathematician by computer programs, if might suffice to look into a mirror. But then there would still be a limit of uneasiness. Frankly, I have no idea how far most of our reasoning can be automated. Certainly much of what we do is based on sweat and routine and not on continuous creative sparks. The only way to see how far one can go is to try it. And certainly Chou's (theorem) prover will astonish many.
I see a great future and great usefulness of such provers and symbolic calculation expert systems in near and more distant future mathematics. After all, the 'talents' of computers and humans are vastly different and should be used for reinforcement rather than competition. This 'reinforcement idea', by the way, seems to be gaining headway in such areas as decision-support systems and NP-hard optimization problems.